Previous | Table of Contents | Next |
Eiffel has a remarkably small set of instructions. The basic computational instructions have been seen: creation, assignment, assignment attempt, procedure call, and retry. They are complemented by control structures: conditional, multibranch, and loop, as well as debug and check.
A conditional instruction has the form if...then...elseif...else...end. The elseif... part (of which there may be more than one) and the else... part are optional. After the if comes a boolean expression; after then, elseif and else come zero or more instructions.
A multibranch instruction has the form
inspect exp when v1 then inst1 when v2 then inst2 ... else inst0 end
where the else inst0 part is optional, exp is a character or integer expression, v1, v2, ... are constant values of the corresponding type, all different, and inst0, inst1, inst2, ... are sequences of zero or more instructions. In the integer case, it is often convenient to use unique value for the vi.
The effect of such a multibranch instruction, if the value of exp is one of the vi, is to execute the corresponding insti. If none of the vi matches, the instruction executes inst0, unless there is no else part, in which case it triggers an exception. (This is the desired behavior because the absence of an else part indicates explicitly that the author guarantees that one of the values matches; to ensure that the instruction does nothing in this case, rather than cause an exception, use an else part with an empty inst0. In contrast, the instruction if c then inst end with no else clause does nothing in the absence of an else part because in this case, there is no implied claim that c must hold.)
The loop construct has the form
from initialization until exit invariant inv variant var loop body end
The invariant inv and variant var parts are optional; the others are required. initialization and body are sequences of zero or more instructions; exit and inv are boolean expressions (more precisely, inv is an assertion); var is an integer expression.
The effect is to execute initialization, then, zero or more times until exit is satisfied, to execute body. (If after initialization the value of exit is already true, body is not executed at all.) Note that the syntax of loops always includes an initialization, as most loops require some preparation. If not, just leave initialization empty while including the from because it is a required component.
The assertion inv, if present, expresses a loop invariant (not to be confused with class invariants). For the loop to be correct, initialization must ensure inv, and then every iteration of body executed when exit is false must preserve the invariant, so the effect of the loop is to yield a state in which both inv and exit are true. The loop must terminate after a finite number of iterations, of course; this can be guaranteed by using a loop variant var. It must be an integer expression whose value is non-negative after execution of initialization and decreased by at least one, while remaining non-negative, by any execution of body when exit is false; because a non-negative integer cannot be decreased forever, this ensures termination. The full-assertion-monitoring mode checks these properties of the invariant and variant after initialization and after each loop iteration, triggering an exception if the invariant does not hold or the variant is negative or does not decrease.
An occasionally useful instruction is debug (Debug_key, ...) instructions end where instructions is a sequence of zero or more instructions and the part in parentheses is optional, containing if present one or more strings (debug keys). Compilation options of the environment (specifying explicit debug keys or just yes or no to govern the effect of debug instructions with no keys) make it possible to treat this instruction as executing the instructions or doing nothing at all. The obvious use is for instructions that should be part of the system but executed only in some circumstances; for example, to provide extra debugging information.
The final instruction is connected with design by contract. The instruction check Assertions end, where Assertions is a sequence of zero or more assertions, has no effect unless assertion monitoring is turned on at the check level or higher. In that case, it evaluates all the assertions listed, having no further effect if they are all satisfied; if any one of them does not hold, however, the instruction triggers an exception.
This instruction serves to state properties that are expected to be satisfied at some stages of the computationother than the specific stages, such as routine entry and exit, already covered by the other assertion mechanisms such as preconditions, postconditions, and invariants. A recommended use of check involves calling a routine with a precondition, where the call, for good reason, does not explicitly test for the precondition. Consider a routine of the form
r (ref: SOME_REFERENCE_TYPE) is require not_void: r /= Void do r.some_feature ... end
Previous | Table of Contents | Next |