This appendix gives worked solutions or solution sketches for a small set of the exercises marked with an asterisk. They are not the only correct answers. Their purpose is to show a reasonable style of solution in Nex.
Question: should transfer_to(other, amount) require other /= this?
One answer is yes:
Another answer is no:
The better choice depends on the intended interface. If the routine models a real movement of funds between distinct accounts, make it a precondition:
transfer_to(other: Account, amount: Real)
require
positive_amount: amount > 0.0
enough: amount <= balance
different_account: other /= this
do
withdraw(amount)
other.deposit(amount)
end
If the interface is meant to be tolerant and mathematical rather than operational, allowing a no-op is also defensible. The key is to decide deliberately.
For
sort(items: Array[Integer]): Array[Integer]
useful postconditions are:
In prose:
ensure
same_length: result.length = items.length
The order and element-preservation properties are harder to state compactly in the current surface syntax, but they should still be part of the design and of the tests.
An Interval class should satisfy:
class Interval
create
make(a, b: Integer) do
start := a
finish := b
end
feature
start: Integer
finish: Integer
invariant
ordered: start <= finish
end
This invariant changes every mutating routine. Any method that extends, shrinks, or merges intervals must preserve start <= finish. That forces each routine to think about both endpoints together, not independently.
For duplicate removal in a sorted array, a good invariant is:
“The segment from index 0 through write contains the unique elements from the already scanned prefix of the input, in sorted order.”
That invariant explains the whole two-index algorithm:
read scans the inputwrite marks the end of the deduplicated prefixBecause the input is sorted, it is enough to compare each new element with the last kept unique element.
Suppose an earlier routine was:
function first(items: Array[String]): String
require
not_empty: items.length > 0
do
result := items.get(0)
ensure
result_is_first_element: result = items.get(0)
end
The contract reveals what the earlier version left implicit:
A File_Cache design can separate contract and environment like this:
class File_Cache
create
make() do
let initial_cache: Map[String, String] := {"bootstrap": ""}
cache := initial_cache
end
feature
cache: Map[String, String]
load(path: String): String
require
path_not_empty: path.length > 0
do
if cache.contains_key(path) then
result := cache.get(path)
else
raise "file missing"
end
rescue
result := "default contents"
end
end
The path itself is a caller obligation. The missing file is an environmental condition handled by rescue. In a fuller implementation, the routine would attempt a real file read before falling back.
If two files must stay synchronized, the design should avoid partial updates.
One reasonable approach:
The contracts belong on the routine inputs and internal consistency. Exceptions belong on actual file-system failures.
A chapter-26-sized program might be a grade book:
school/Student.nex for one student’s identityschool/Course_Record.nex for one student’s scores in one courseschool/Grade_Book.nex for the collection and summary logicschool/Report_Printer.nex for output formattingEach file has one clear reason to change. That is the main test of a sound file structure.
Take a configuration loader.
Poor design:
Better design:
Config_Source handles file or host accessConfiguration stores parsed settingsThat keeps host-specific code at the edge and preserves a portable center.
Suppose a weak postcondition for without_last(s) only says the result is one character shorter.
Tests should then include:
"a" becomes """cat" becomes "ca""Nex" becomes "Ne"These tests catch implementations that return any string of the right length but not the right prefix.
A small library checkout tracker would naturally use:
BookMemberLoanLibraryContracts would express:
Tests would check the full sequence:
For an inventory list, combine:
Most larger programs are built from a few such patterns layered carefully rather than from entirely new techniques.
The goal of a solutions appendix is not to end thought, but to sharpen it.