Lab · c01.s01.L1

Contract checker

A returned value can keep every line of a four-line contract without being exact.

Question: What may a caller rely on when a procedure returns, and what must the caller never assume?

Contract checkerA row of guesses for the square root of nine climbs from 1.0000 to 5.0000, then settles through 3.4000 and 3.0235 to 3.0001. Beside it, four contract lines are checked in turn: the input is accepted, the square of the estimate lies within the tolerance 0.001, the input is unchanged, and exactness is not promised. A looser tolerance stops earlier. The fourth line never becomes a promise: rely on the tolerance, never on equality.Contract checkerWhat does a program promise you?The contract, four lineswhat you may pass ina whole number n from 2 to 20what comes backan estimate x whose square is within the stated tolerance of nwhat stays the samen is not modifiedwhat is not promisedthat x*x equals n exactlyThe recipe: x_next = (x + n / x) / 2. Stop when |x*x - n| < tolerance.
Re-simulated Re-simulated: the square-root recipe from section 1.1 runs on n = 9 at tolerance 0.001 and stops at 3.0001, with the gap 0.000549. The frames check the four contract lines in turn, show the caller's exactness assumption failing by 0.000549, stop at 3.0235 under tolerance 0.5, and print 2.0000 for n = 4 while the gap is 3.72e-07. The script reruns every control setting; no measured data is used.
Lab controls
9

Left/Down and Right/Up move by 1; Page Up/Down move by 5; Home sets 2; End sets 20

0.001

Left/Right move one option; Home selects 0.5; End selects 0.001

off

Space or Enter toggles; Left sets off, Right sets on

running

Space toggles running and paused

Frame 1 of 14: Four linesA contract is a promise on four lines: what you may pass in, what comes back, what stays the same, and what is not promised. The recipe is the square-root update x_next = (x + n / x) / 2, stopped when |x*x - n| < tolerance. The fourth line is part of the promise, not an apology for it.

Four lines. A contract is a promise on four lines: what you may pass in, what comes back, what stays the same, and what is not promised. The recipe is the square-root update x_next = (x + n / x) / 2, stopped when |x*x - n| < tolerance. The fourth line is part of the promise, not an apology for it.

Keyboard: Space plays or pauses, Left and Right step, Home goes to the first frame, End goes to the last frame.

Text description of this lab

A row of guesses for the square root of nine climbs from 1.0000 to 5.0000, then settles through 3.4000 and 3.0235 to 3.0001. Beside it, four contract lines are checked in turn: the input is accepted, the square of the estimate lies within the tolerance 0.001, the input is unchanged, and exactness is not promised. A looser tolerance stops earlier. The fourth line never becomes a promise: rely on the tolerance, never on equality.

Return to the section that hosts this lab

Caption status: re-simulated. Every lab declares one of published, re-simulated, schematic, synthetic or interpolated.