Dynamic Semantics

The dynamic semantics describes what a program does when it runs, once it has passed the checks of Chapter 4: the value each expression produces, the changes each statement makes, and the ways evaluation can end. The static semantics kept track only of the types of values. Here the values themselves are the subject.

5.1Values and Objects

A value is what an expression produces. The values of Nex are:

• scalars: integers (including the fixed-width integers Byte, Integer16 and Integer32), reals, characters, booleans and strings. Each is an immutable value of the corresponding scalar class.
• the null reference, nil.
• references to objects held in the store (Section 5.2): instances of user classes, arrays, maps, sets, tasks and channels.
• closures, the values of anonymous and named functions. A closure pairs a parameter list and a body with the bindings in force where the function was defined.

An object is a mutable record held in the store. It has three parts:

• its class, which is used for dynamic dispatch (Section 5.4), by match, and by convert;
• the fields its class declares directly, each with its current value;
• for each parent named in its class’s inherit clause, a reference to a further object of that parent’s class, called a nested object, which is built in the same way.

An object therefore has the same shape as its class’s inheritance. A field that the class only inherits is not among the object’s own fields. It is held in the nested object of the ancestor that declares it, and is reached by following parent references from the object down to that nested object (Section 4.9).

Nested objects are never shared. If two parents of a class have a common ancestor, each parent’s nested object has its own nested object for that ancestor, with its own copy of every field the ancestor declares (Section 4.9, Repeated inheritance and shared ancestors). A write to one copy is never seen through the other.

class Counter
  create make() do count := 0 end
feature
  count: Integer
  bump() do count := count + 1 end
end

class Left
  inherit Counter
  create make() do Counter.make() end
feature
  bump_left() do bump() end
  left_count(): Integer do result := count end
end

class Right
  inherit Counter
  create make() do Counter.make() end
feature
  right_count(): Integer do result := count end
end

class Both
  inherit Left, Right
  create make() do Left.make() Right.make() end
end

let b := create Both.make()
b.bump_left()
b.bump_left()
print(b.left_count())
print(b.right_count())

Both inherits Counter twice, once through Left and once through Right, so its objects hold two count fields (Figure 5.1). bump_left increments the copy in Left’s nested object, and right_count reads the copy in Right’s. The program prints 2 and then 0.

Because inheritance is acyclic (Section 4.9), the nesting always ends, and because no nested object is shared, an object and its nested objects form a tree. They all belong to the one object made by create: they are allocated together (Section 5.5), and none of them can be reached on its own from outside that object.

Scalars and nil are not objects, and are not held in the store. Two scalar values are identical exactly when they are equal, which is why == and = agree on them (Section 5.3).

5.2The Dynamic Environment

Expressions are evaluated, and statements executed, against two things.

• The bindings map each name in scope to a value. A variable, parameter or field is bound to the value it currently holds. Within a method or constructor, the bindings also give the current object, which is the value of this. Within a routine that has a return type, they also give the variable result.
• The store holds every object. A reference points to an object in the store, and changing an object means changing the store. An assignment to a field changes only the object that holds the field directly. For an inherited field, that is the nested object of the ancestor that declares it (Section 5.1).

How evaluation ends

Evaluating an expression ends in one of three ways. It completes normally, producing a value; it raises an exception (Section 5.7); or it never ends (Section 5.9). Executing a statement ends in the same three ways, except that a statement that completes normally produces no value.

The following rules hold throughout this chapter. Each section states only where it departs from them.

• Order. Apart from tasks (Chapter 6), evaluation is sequential and deterministic, and proceeds from left to right: the operands of an operator, the receiver and then the arguments of a call, and the statements of a block, each in the order written.
• Exceptions. If evaluating part of an expression or statement raises an exception, the whole expression or statement raises the same exception, and its remaining parts are not evaluated. Only a rescue clause stops this (Section 5.7).
• No undoing. Changes made to the store before an exception is raised remain in place. Raising an exception does not restore objects that the abandoned evaluation had already changed.

5.3Evaluation of Expressions

Constants, variables, and the current object

A constant produces its value and changes nothing. A variable produces the value it is bound to. A name refers to its nearest enclosing binding (Section 5.8, on scope).

this produces the current object. Inside the body of a method or constructor, member access through this — a field read this.f, a call this.m(…), and likewise a bare field name or bare call — refers to the part of the object that belongs to the class whose text contains the body (Section 5.4). Used as a value (stored, passed, returned or compared), this is the whole object, so a heir’s overrides apply to calls made on it.

super and the name of an ancestor produce something different, because each inherited part of an object is a nested object of its own (Section 5.1). On its own, super produces the current object’s nested object for its direct parent: a different reference, one level down. The name of an ancestor P produces the nested object for P, which may be several levels down if P is not a direct parent (Section 4.9).

Member access through super or P, as in super.f or P.f, therefore needs no rule of its own: the field is read from that nested object as it would be from any other. Calls through super or P are described in Section 5.4.

All these nested objects belong to one object. They are allocated together (Section 5.5) and never reachable on their own from outside it. So there is still only one object, even though this and super are different references.

Operators

An arithmetic or comparison operator evaluates its left operand, then its right operand, and then applies the operation that the operands’ class defines for it.

let a: Integer := 7
let b: Real := 2.0
print(a + b)

The operands have different numeric classes. The Integer is accepted where a Real is wanted, the sum is computed as a Real, and the value printed is 9.0. This widening is the language’s only implicit numeric conversion (Section 4.3).

let b: Byte := 200u8
print(b + b)

An operand of a fixed-width type is first replaced by the Integer with the same value, and the operation is carried out on Integer operands, so the sum is the Integer 400. The result of an arithmetic operation is never a fixed-width value, and it cannot overflow the narrow type. The range of Byte, Integer16 or Integer32 is checked only where a value is converted back into one (§B.3).

Arithmetic on Integer operands is checked. If the exact result of an operation lies outside the 64-bit range, the operation raises Arithmetic_Overflow. Integer division or remainder with a divisor of zero raises Division_by_Zero (§B.3).

Arithmetic on Real operands never raises an exception. Division by zero yields the IEEE 754 value positive infinity, negative infinity or NaN, as §B.3 records. This difference between integer and real division by zero is deliberate, and holds on every back end.

Equality comes in two kinds. Value equality, =, compares contents: two collections are equal when their elements are equal, and two objects are equal according to the equals method of their class, which a user class may override. Identity equality, ==, compares references: two objects are identical exactly when they are the same object. On scalars the two kinds agree. The operands of the equality operators are not converted the way arithmetic operands are. Their types must be related by conformance (Section 4.4), so comparing the Byte 65u8 with the Integer 65 is a compile-time error, not a comparison that yields false.

An arithmetic operator can also be bound to a method by an alias clause (Section 3.4). The operator is then the call: once both operands are evaluated, a - b is evaluated as the call a.minus(b) by the steps of Section 5.4. The class of the left operand’s object selects the method, the method’s contract is checked, and its rescue clause handles a failure in its body. An operator is never a way around a method’s contract.

let owed: Money := create Money.make(100, "USD")
let paid: Money := create Money.make(30, "EUR")
print(owed - paid)      -- Precondition violation: same_currency

Short-circuit and and or

The operators and and or do not always evaluate their right operand. In a and b, a is evaluated first. If it is false, the result is false and b is not evaluated; otherwise the result is the value of b. In a or b, if a is true, the result is true and b is not evaluated; otherwise the result is the value of b.

This holds on every back end and is part of the language, not an optimisation. A guard such as n /= 0 and total / n > 2 therefore never evaluates the division when n is 0, and cannot raise Division_by_Zero.

Member access and the safe access

An access e.f evaluates e and reads the field f of the object it refers to. If the static type of e declares f itself, the field is one of the object’s own. Otherwise it is held in the nested object of the ancestor that declares it, reached by following parent references from the object (Section 4.9). The static type of e is a class type, never an optional one (Section 4.4), so e never produces nil.

The safe access e?.f may be applied to an optional receiver. If e produces nil, the safe access produces nil. Otherwise it reads the field as e.f does. This is why the static type of a safe access is optional (Section 4.4).

5.4Calls and Dynamic Dispatch

A call names a routine and supplies its arguments. This section describes how a call on a receiver, e.m(e1, …, en), is evaluated. Calls of free functions, calls that name an ancestor, and calls through super differ from it only in the ways noted at the end of the section.

The steps of a call

A call e.m(e1, …, en) is evaluated in the following steps. Figure 5.2 shows the same steps, with every way a call can end.

1. The receiver e is evaluated. Its static type is a class type, never an optional one (Sections 4.1 and 4.4), so the result is a reference to an object, never nil.
2. The arguments are evaluated from left to right.
3. A method is selected: the method named m with n parameters that the object’s class declares or inherits. It is the class of the object that counts, not the static type of e. This is dynamic dispatch, and it is how an overriding method in a subclass takes effect. Because the number of arguments takes part in the selection, this step also resolves overloading by arity (Section 4.4).
4. If the method has a postcondition, the values its old expressions will need are recorded (Section 5.6). Then a new set of bindings is made for the method’s body. Each parameter is bound to the value of its argument, and this is bound to the object the method belongs to (see Which object this names, below).
5. If the call is qualified (see below), the class invariant is checked (Section 5.6).
6. The method’s precondition is checked.
7. The body is run.
8. The method’s postcondition is checked.
9. If the call is qualified, the class invariant is checked again.
10. The call completes, and its value is the final value of result. A method that declares no return type yields the void value instead.

If any of these steps raises an exception, the call raises the same exception and the remaining steps are skipped. An exception in step 1 or step 2 therefore means that no method is entered, and an argument after the one that raised is never evaluated. A failed check in step 5, 6, 8 or 9 raises a contract violation.

A call is qualified when it is written with a receiver expression, as e.m(e1, …, en) is. This includes a call on this, such as this.m(), and an operator bound to a method by an alias clause, since a - b is the call a.minus(b) (Section 3.4). A call written without a receiver is unqualified: a bare call m(…), a call that names an ancestor, and a call through super. Unqualified calls skip steps 5 and 9, so a method may call other methods of its own class while the invariant is temporarily broken.

Step 7 works differently when the method has a rescue clause. If the body raises an exception, the clause is run with exception bound to it, and how the clause finishes decides what happens next.

• If the clause executes retry, the call goes back to the start of step 7 and runs the body again. Neither the invariant nor the precondition is checked again, and the old values recorded in step 4 are kept.
• If the clause completes normally, the call continues at step 8, as if the body had completed. The value of the call is still the final value of result, which the clause may have set.
• If the clause raises an exception, the call raises it.

A rescue clause handles only exceptions raised by the body. A failed invariant, precondition or postcondition is not caught by the method’s own rescue clause; it passes to the caller.

A call that raises an exception does not undo anything. Assignments the body made to fields before the exception remain in place.

Dynamic dispatch: an example

class Shape
  create make() do end
feature
  area(): Real do result := 0.0 end
end

class Square
  inherit Shape
  create make(s: Real) do side := s end
feature
  side: Real
  area(): Real do result := side * side end
end

let sh: Shape := create Square.make(3.0)
print(sh.area())

The variable sh has static type Shape, but the object it refers to is a Square. Step 3 selects the method by the class of the object, so Square’s area runs and the value printed is 9.0, not 0.0.

What the body can see

The bindings made in step 4 extend the bindings in force where the method was defined, not those of the caller. The body can therefore see the fields of its object and its own parameters, but none of the caller’s local variables.

Which object this names

For a call on any receiver other than the current object, if the object’s own class declares or overrides m, this is the receiver itself. If instead the class inherits m, the body is text written in the ancestor that declares it, and this always names the class its text belongs to (Section 5.3). In that case this is that ancestor’s nested object within the receiver (Section 5.1), found the same way an inherited field is found (Section 4.9): along the first path.

Calls on the current object

A bare call m(…) or a call this.m(…) is a call on the current object o, made by text that may belong to one of o’s ancestors. Let A be the class whose text contains the call, and p the path from the class of o to the part of o that this text is running on (empty when it is o’s own class’s text). Step 3 then selects the method as follows.

• Among the classes along p, from the class of o down to, but not including, A, the outermost one that itself declares m (an override, not merely an inherited method) supplies it, and this is bound to that class’s part of o. An override in a subclass therefore takes effect in the code it inherits.
• If none of them declares m, the call stays on p: the method is the one A declares or inherits, and this is bound within the part of o that belongs to A, to the nested object of the class that declares it. A method of a shared ancestor (Section 4.9) called this way acts on the copy of its fields along p, never on another path’s copy.
• If that method is deferred, the method is selected from the class of o, as for a call on any other receiver.

In the example of Section 5.1, suppose Right also had a method bump_right() do bump() end. Then b.bump_right() increments the copy of count in Right’s nested object: neither Both nor Right declares bump, so it runs on the Counter nested in Right. Had Both overridden bump, its override would run instead, for bump_left and bump_right alike.

Free functions and closures

A call of a free function, m(e1, …, en), follows the same steps without a receiver. Step 1 is skipped, step 3 selects the function by name alone (free functions cannot be overloaded), no this is bound, and there is no invariant to check. A bare call written inside a class is a call on this if the current class has a method of that name, and a free-function call otherwise (Section 4.4). A bare call on this is unqualified, so it checks no invariant. Applying a closure is evaluated likewise, with the bindings the closure captured taking the place of the bindings of a routine’s definition.

Calling a named ancestor, and calling through super

Within a class, a call may name one of the current class’s ancestors in place of a receiver: Shape.describe(), written inside a subclass of Shape, for example. A call P.m(e1, …, en) of this kind acts on the current object, and differs from an ordinary call in the following steps.

• Step 1. There is no receiver expression to evaluate.
• Step 3. The method is selected from P: the method named m with n parameters that P declares or inherits. The class of the current object plays no part, so there is no dynamic dispatch.
• Step 4. this is bound to P’s nested object within the current object, the same object that evaluating P on its own yields (Section 5.3). If P only inherits m, this is bound further in, to the nested object of the ancestor that declares it. Either way, a field read inside the body of m refers to that ancestor’s own copy of the field, not to the current object’s outer one.
• Steps 5 and 9. The call is unqualified, so the class invariant is not checked.

A call through super, super.m(e1, …, en), is the same call with P supplied implicitly: it is the one class that the class containing the call inherits. A class that inherits more than one class, or none, cannot use super (Section 4.4). It must name the intended ancestor instead, as Flyable.fly() does.

class Shape
  create make(c: String) do colour := c end
feature
  colour: String
  describe(): String do result := colour end
end

class Square
  inherit Shape
  create make(c: String, s: Real) do
  super.make(c)
  side := s
  end
feature
  side: Real
  describe(): String do result := super.describe + ", side " + side.to_string end
end

let sq := create Square.make("blue", 3.0)
print(sq.describe())

Square.make first delegates to Shape.make to set colour (Section 5.5), then sets side itself. Square’s describe calls super.describe, which selects Shape’s describe, not Square’s own (which would only call itself again), and appends to its result. The program prints "blue, side 3.0".

The class that super stands for is fixed by the class whose text contains it, not by the class of the current object. This keeps it correct under further inheritance. Suppose a class Cube inherits Square without overriding describe. Then cube.describe() runs Square’s describe by ordinary dynamic dispatch, and its super.describe still reaches Shape, the ancestor its author meant, however far below Square the actual object’s class is.

The named ancestor may also be an imported host interface or class (Section 3.6), when the current class extends it under the conditions of Section 4.9. Step 3 then selects the host’s own implementation of m rather than a Nex method. As in the ordinary case, the method is fixed by the named class, so if the current class overrides m itself, a call through super still reaches the host’s implementation and never recurses back into the override. A member that the current class does not define itself needs no such care: an ordinary call o.m(…) reaches the host’s implementation, because no Nex override competes with it.

5.5Object Creation and Constructors

A creation create A.k(e1, …, en) makes a new object of class A and runs its constructor k. It is evaluated in the following steps.

1. A new object of class A is allocated, together with its nested objects: one for each parent named in A’s inherit clause, each with nested objects of its own, all the way down (Section 5.1). Every field of every one of these objects is given its initial value: nil for an optional field, and the zero value of its type for a scalar field. A non-optional reference field has no initial value. The attachment rule of Section 4.9 guarantees that some constructor assigns it before creation completes.
2. The arguments are evaluated from left to right.
3. The constructor k is entered. this is bound to the new object, and each parameter to the value of its argument.
4. The constructor’s precondition is checked.
5. The constructor’s body is run. A rescue clause on the constructor handles an exception raised by the body as a method’s does (Section 5.4).
6. The constructor’s postcondition is checked.
7. The class invariant, including the invariants A inherits, is checked on the new object (Section 5.6). This is the only invariant check a creation makes: there is none on entry to the constructor.
8. The creation completes, and its value is a reference to the new object.

class Account
  create make(b: Real) do balance := b end
feature
  balance: Real
invariant
  non_negative: balance >= 0.0
end

let acct := create Account.make(100.0)
print(acct.balance)

The constructor make sets balance, then step 7 checks the invariant non_negative on the new object before the creation yields it. The value printed is 100.0. Had the constructor left balance negative, step 7 would raise a contract violation instead of returning an inconsistent object.

A constructor may assign the once fields of its class. After the constructor returns, those fields keep their values for the life of the object (Section 4.5 enforces this statically). When a create names no constructor, steps 2 to 6 are skipped: the object keeps the initial values of its fields, and only the invariant is checked.

Delegating to a named or superclass constructor

A constructor may call another constructor on the object already being created, instead of creating a new one. Most often this is the parent’s constructor, called to set the fields the parent declares before the subclass’s constructor sets the rest. The call names the class, P.k(e1, …, en), or uses super.k(e1, …, en), where P is the one class that the enclosing class inherits (Section 4.4). P must declare k itself; a constructor that P only inherits does not qualify (Section 4.4).

Such a call allocates nothing. P’s nested object already exists, made in step 1 of the outermost create. The call evaluates its arguments, binds this to that nested object and each parameter to its argument, checks k’s precondition, runs its body, and checks its postcondition. It checks no invariant.

Because this is P’s nested object, a field that k assigns is set in that nested object, which is where the field is held (Section 5.1). The body of k sees this as the class its own text belongs to, as every routine body does (Section 5.3).

The invariant is checked once, by the outermost create, when its constructor returns (step 7). By then every constructor it delegated to has run, each on the nested object it was meant to initialise. In the Square example of Section 5.4, this is why super.make(c) is safe to run before side is set: no invariant is checked until Square.make itself returns, with both fields in place.

When a class extends a concrete host class rather than a Nex class (Section 4.9), delegation reaches the host’s own constructor, and the constructor is written new. new is reserved for this purpose when P is a host class, and is an ordinary identifier everywhere else. Delegation to a host constructor differs from delegation to a Nex constructor in two ways.

• The call must be the first statement of the delegating constructor. The host platform’s object model requires the superclass’s construction to finish before anything else touches the object. Delegation among Nex constructors has no such requirement, since every field already has its initial value.
• The host constructor is selected by the number of arguments alone, since a host constructor’s parameters are not given Nex types (Section 4.9).

If the delegating constructor contains no such call, a call with no arguments is supplied implicitly. The host class must then provide a constructor that takes no arguments, as the Host superclass construction condition of Section 4.9 requires.

5.6Contract Checking

Contracts are checked while the program runs. To check an assertion is to evaluate its expression. If the value is true, evaluation continues. If it is false, a contract violation is raised: an instance of the Contract_Violation class for that kind of assertion (Appendix B.7), whose label is the assertion’s label and whose message names it — or, for a bare assert, which has no label, names its source line — so that the report can say which condition failed. When a clause contains several assertions, they are checked in the order written, and the first that is false is the one reported.

A contract violation is reported differently from other exceptions, but it is caught by a rescue clause in the same way (Section 5.7).

Routine contracts

A routine’s contract is checked at fixed points in the steps of a call (Section 5.4 and Figure 5.2).

• On entry, if the routine has a postcondition, the values its old expressions will need are recorded: for each field that an old expression reads, the value the field holds at that moment. This happens before the invariant and the precondition are checked.
• The precondition is checked after the parameters are bound and before the body runs. A failed precondition is the caller’s fault.
• The postcondition is checked when the body completes normally, or when the routine’s rescue clause completes without retry. At that point result holds the value the call will return, and each old expression has the value recorded on entry. A failed postcondition is the routine’s fault.
• The class invariant is checked twice in a qualified call (Section 5.4): on entry, before the precondition, and on exit, after the postcondition. The invariant checked is the receiver’s, which includes the invariants its class inherits (see Inherited contracts, below). An unqualified call checks no invariant. Inside a method, the invariant may therefore be broken for a while, even across calls to other methods of the same class, provided it holds again when the qualified call returns. Creating an object checks the invariant once, when the constructor returns (Section 5.5). While an invariant is being checked, the calls its assertions make check no invariant themselves, so an assertion may call the object’s queries, even qualified (this.q).

A routine’s own rescue clause does not catch a failure of its invariant, precondition or postcondition. That contract violation passes to the caller (Section 5.4).

class Account
  create make() do balance := 0.0 end
feature
  balance: Real
  withdraw(amount: Real)
  require
    enough: amount <= balance
  do
    balance := balance - amount
  end
end

let acct := create Account.make()
acct.withdraw(50.0)

The precondition enough is checked on entry to withdraw, after amount is bound. The balance is 0.0, so the assertion is false, and the call raises a contract violation that names the failing condition: Precondition violation: enough. A failed precondition is the caller’s fault, and the label is what lets the report point to the cause.

Inherited contracts

A method that overrides an inherited one also inherits its contract, and a class inherits the invariants of its ancestors. The checks of a call use the effective contract of the method selected in step 3. It combines the contracts of every version of that method, that is, every method with the same name and number of parameters in the method’s class and in its ancestors.

• Precondition. The effective precondition holds if the precondition of any version that states one holds. A version’s precondition holds when all of its assertions are true. A first declaration, a version that overrides nothing, with no require clause admits every call, so if any first declaration has none, the effective precondition always holds. Any other version with no require clause contributes nothing: a method that overrides without stating a precondition keeps the one it inherits. An overriding method can therefore weaken what its callers must establish, but never strengthen it (Section 4.9, Attainable preconditions).
• Postcondition. The effective postcondition holds only if the postconditions of all versions hold. The ancestors’ assertions are checked first, then the method’s own. An overriding method can therefore add to what it guarantees, but never take anything away.
• Invariant. A class’s effective invariant holds only if its own invariant and the invariants of all its ancestors hold. The ancestors’ assertions are checked first. An ancestor reached through more than one parent is checked once.

A deferred method is a version like any other. It never runs, but its contract is part of the effective contract of every implementation. Each version’s assertions are evaluated with that version’s parameters bound to the call’s arguments, by position, so an inherited assertion reads the arguments it was written against even when the selected method names its parameters differently.

When the effective precondition combines more than one version and fails, no single assertion is to blame, so the violation names the combined precondition rather than one assertion’s label.

class Base
  create make() do end
feature
  f(x: Integer)
  require
    small: x < 10
  do
  end
end

class Heir
  inherit Base
  create make() do end
feature
  f(x: Integer)
  require
    even: x % 2 = 0
  do
    print(x)
  end
end

let h: Base := create Heir.make()
h.f(3)
h.f(12)
h.f(13)

The effective precondition of Heir’s f is small or even. The call h.f(3) satisfies small and h.f(12) satisfies even, so both run. The call h.f(13) satisfies neither, and raises a precondition violation.

A contract stated on a deferred method binds every implementation:

deferred class Shape
feature
  scale(x: Integer): Integer
  require
    positive: x > 0
  deferred
  ensure
    bigger: result > x
  end
end

class Doubler
  inherit Shape
  create make() do end
feature
  scale(n: Integer): Integer
  do
    result := n * 2
  end
end

let s: Shape := create Doubler.make()
print(s.scale(3))
print(s.scale(0))

Doubler’s scale states no precondition and is not a first declaration, so its effective precondition is positive, read with n for x; its effective postcondition is bigger. The first call prints 6. The second raises Precondition violation: positive.

The assert statement

Routine contracts are checked at a routine’s boundaries, and loop invariants over the span of a loop. The assert statement checks a condition at a chosen point inside a body. Executing assert checks each of its assertions in the order written. If one is false, a contract violation is raised and the statement does not complete. If all are true, the statement completes and changes nothing. The named form supplies the label to report. The bare form has none, and the report gives the line instead:

assert non_empty: items.length > 0   -- Assertion violation: non_empty
assert i < n                          -- Assertion violation (line 42)

A failed assert raises the same kind of contract violation as a failed require or ensure, and a rescue clause catches it on the same terms. The only difference is the clause it came from.

Refinement types

The predicate of a refinement type is checked in the same way. The static semantics marks every place where a value of the base type flows into a binding, parameter, field or return whose type is the refinement type, and every convert to it (Section 4.3). At each such place, the predicate’s variable is bound to the value and the predicate is evaluated.

If the predicate is true, the value passes through unchanged. There is no wrapper, since a refinement type is represented by its base type. If the predicate is false, a contract violation is raised, as for a failed require.

The one exception is convert, whose purpose is to test rather than to assert. A failed refinement predicate there makes the convert yield false instead of raising.

5.7Exceptions: raise, rescue, retry

An exception is raised either by a raise statement or by the language itself. It ends each enclosing expression and statement in turn, as Section 5.2 describes, until a rescue clause handles it. A routine’s own rescue clause is described with the steps of a call (Section 5.4). This section describes raise and the scoped block.

The statement raise e evaluates e and raises its value. Any value may be raised: raise "transient" raises a string, and raise 42 an integer. The language raises built-in exceptions in the same way for a nil dereference, a failed contract (Section 5.6), arithmetic overflow and integer division by zero (Section 5.3), a failed runtime argument check, a conversion method given a value it cannot convert (Conversion_Error, Appendix B.7), and a match that no clause matches (Section 5.8). A failed convert raises nothing: it yields false (Section 4.5). Such an exception is an object of one of the classes of Appendix B.7, chosen by the kind of failure, so a handler can tell failures apart with convert or match rather than by reading a message. A value raised with raise is not wrapped: the handler receives exactly that value.

A scoped block do b1 rescue b2 end is executed in the following steps.

1. The block b1 is executed. If it completes normally, the rescue part is ignored and the scoped block completes normally.
2. If b1 raises an exception, the handler b2 is executed, with exception bound to the raised value. The local variables of b1 are not in scope in b2. What happens next depends on how b2 ends.
   • If b2 executes retry, the rest of b2 is abandoned and the scoped block starts again at step 1, running b1 from its first statement against the store as it now is.
   • If b2 completes normally, the scoped block completes normally, and execution continues after it.
   • If b2 raises an exception, the scoped block raises it.

class Worker
  create make() do attempts := 0 end
feature
  attempts: Integer
  run()
  do
    do
      attempts := attempts + 1
      if attempts < 3 then
        raise "transient"
      end
      print(attempts)
    rescue
      if attempts < 3 then
        retry
      end
    end
  end
end

let w := create Worker.make()
w.run()

The first two attempts raise. Each time, the handler runs and executes retry, which runs the block again from the top. On the third attempt no exception is raised, and 3 is printed. retry may appear only inside a rescue block (Section 2.9); anywhere else it is a compile-time error.

5.8Statements and Control Flow

Local declaration, assignment, and scope

The statement let x := e evaluates e and introduces a new variable x in the current scope, bound to the value. If an enclosing scope already has a variable x, the new one shadows it until the end of the current scope.

The assignment x := e evaluates e and binds the nearest enclosing variable x to the value. An assignment to a field, f := e or this.f := e, changes the field in the store, in the object that holds it (Section 5.2). Only the class that declares a field may assign it (Section 4.5).

A scoped block do…end opens a new scope. A let inside the block shadows any outer variable of the same name. When the block ends, the variables it declared disappear and the outer ones are visible again. Assignments the block made to variables of enclosing scopes remain.

let y := 1
do
  let y := 2
  print(y)
end
print(y)
do
  y := 3
end
print(y)

The program prints 2, 1 and 3. The first block declares its own y, which disappears when the block ends. The second assigns the outer y.

Conditionals

The statement if c1 then s1 elseif c2 then s2 … else s end evaluates its conditions in order and executes the branch of the first condition that is true. If none is true, it executes the else branch, or nothing if there is none.

The conditional expression when c then a else b end evaluates c, then evaluates only the chosen expression, a if c is true and b otherwise. Its value is the value of the chosen expression.

Loops

A loop from init until c do body end, which may also carry an invariant and a variant, is executed in the following steps.

1. A new scope is opened for the loop, and the from block is executed in it. Variables it declares are visible in the rest of the loop, but not after it.
2. If the loop has an invariant, it is checked.
3. The condition c is evaluated. If it is true, the loop completes normally.
4. If the loop has a variant, it is evaluated. Its value must not be negative and, from the second iteration on, must be less than its value in the previous iteration. Otherwise a contract violation is raised.
5. The body is executed in a new scope that lasts for this iteration only. A let in the body does not survive to the next iteration, but assignments to variables outside the body do.
6. The loop continues at step 2.

The invariant is therefore checked after the from block and after every execution of the body. The variant is what guarantees the loop ends: an integer that decreases on every iteration and never goes below zero cannot decrease for ever.

let sum: Integer := 0
from let i := 1 until i > 5 do
  sum := sum + i
  i := i + 1
end
print(sum)

The from block declares i. The body runs while i > 5 is false, adding i to sum on each iteration. When i reaches 6 the loop ends, and 15 is printed.

The counted loop repeat n do body end and the cursor loop across e as x do body end are derived forms, translated in Appendix C. The first becomes a loop over a counter. The second becomes a loop driven by the start, item, next and at_end methods of the Cursor class (Appendix B).

Any of the three loops may end with a rescue clause, written before its closing end. It guards the body, not the loop as a whole. If an execution of the body raises an exception, the clause runs with exception bound to it, and how the clause finishes decides what happens next. If it executes retry, the body runs again from its first statement, for the same iteration: the from block, the condition, and the counter or cursor of repeat and across are not touched. If it completes normally, the loop ends, as though its condition had become true. If it raises, the loop raises the same exception. The clause is a derived form: the body becomes a scoped block do body rescue handler end (Section 5.7), and a fresh flag that the handler sets is added to the loop’s condition with or.

Dispatch statements

The case statement evaluates its subject once, then compares the value with the constants of each clause in turn, by value equality. It executes the first clause that has an equal constant. If no clause matches, it executes the else clause, or does nothing if there is none.

The match statement evaluates its subject once, then tries its clauses in order. A clause matches when the class of the subject’s object conforms to the class the clause names and any field patterns it has match the object’s fields (Section 2.8). The clause’s variables are then bound, and its guard, if any, is evaluated; if the guard is false, the next clause is tried. The statement executes the first clause that matches with a true guard. If no clause matches, it executes the else clause; if there is none, it raises an exception. On a sealed class, the static check of Section 4.5 ensures that some clause always matches.

The host block

The statement with "name" do body end, where the string names a host facility, is the one construct whose behaviour depends on the platform beneath the implementation.

If the implementation recognises the facility, the body is executed with name resolution extended to it: a class name or call in the body that resolves to no Nex entity may resolve to an entity of the host. If the implementation does not recognise the facility, the whole block is skipped. The body is not executed, and no error arises. A program can therefore carry host-specific passages that run only where their host is present.

The JVM implementation recognises the facility "java". Within the block, imported Java classes may be instantiated, and their methods called with the ordinary call syntax. A call whose receiver is a Nex value is still dispatched by the rules of Section 5.4. Unlike the scoped block do…end, the host block does not open a scope: a let inside it declares a variable in the enclosing scope, which remains visible after the block.

A class’s inherit clause is a declaration, elaborated with the rest of the static world (Section 3.1), not a statement that is executed. A class that implements a host interface or extends a host class (Sections 4.9, 5.4 and 5.5) is therefore not itself written inside a host block. Only the direct construction and use of a host object needs one.

Implementations may also differ in which host capabilities they support. A conforming implementation must recognise every host facility it claims to. But inheriting a host interface and inheriting a host class are separate capabilities, and an implementation may support one without the other, reporting a compile-time error for the one it lacks rather than approximating it.

5.9Termination

As Section 5.2 describes, evaluation ends in one of three ways: it completes normally, it raises an exception, or it never ends. A loop whose condition never becomes true, or a recursion with no base case, never ends. This Definition makes no claim that evaluation ends; it says only what the outcome is when it does.

The remaining statement, spawn, starts a concurrent evaluation, and is the subject of Chapter 6.