The Eiffel language has many features that support software engineering. One of these is a loop statement that allows programmers to specify loop variants and invariants. We hope Grace may also be used to teach about invariants, so it would be useful to write Eiffel-style loops in Grace:

def letters = "ABCDE" var i : Number := 1 loop { print(letters[i]) i := i+1 } invariant { i < = (letters.size + 1) } until { i > letters.size } variant { letters.size - i + 1 }

1 2 3 4 5 6 7 8 9 10

def letters = "ABCDE" var i : Number := 1   loop {     print(letters[i])     i := i+1   }   invariant { i < = (letters.size + 1) }   until { i > letters.size }   variant { letters.size - i + 1 }

The key here is the loop/invariant/until/variant control structure — which in Grace is just a method that takes Blocks as arguments. Here’s a simple implementation of this method:

method loop (body) invariant (invariant) until (condition) variant (variant) { if (!invariant.apply) then {error "Loop invariant failed before loop" return "ERROR"} var variantValue := variant.apply while {!condition.apply} do { body.apply if (!invariant.apply) then {error "Loop invariant failed in loop" return "ERROR"} def variantValue' = variant.apply if (variantValue' < 0) then {error "Loop variant has gone negative" return "ERROR"} if ((variantValue - variantValue') < 1) then {error "Loop variant decreased by less than one" return "ERROR"} variantValue := variantValue' } }

1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21

method loop (body)        invariant (invariant)        until (condition)        variant (variant) {      if (!invariant.apply) then {error "Loop invariant failed before loop"                                return "ERROR"}    var variantValue := variant.apply    while {!condition.apply} do {        body.apply         if (!invariant.apply) then {error "Loop invariant failed in loop"                                     return "ERROR"}         def variantValue' = variant.apply         if (variantValue' < 0) then {error "Loop variant has gone negative"                                      return "ERROR"}         if ((variantValue - variantValue') < 1)                     then {error "Loop variant decreased by less than one"                           return "ERROR"}         variantValue := variantValue'                      } }

Of course, in a practical Grace system, this method, like other control structures, would be defined in the system or dialect library. The key features that make this possible are not themselves complex: multi-part method names support defining every control structure (syntatically and semantically) as a method request, and then using blocks to pass code into those methods.