Symbolic forms of loops
A customer of a cheese maker asks for aged cheeses (denoted below as
s). The age can be different, the type can be different, and there are a dozen of other characteristics to think about. But let's focus solely on age
a. It can be 6 months, 12 months, 24 months or something else. How to document this requirement? A mathematician would write something like ∀c∈s. age(c) ≥ a . The formula reads "for all cheese products c from the requested aged cheeses s the age of the product should be greater than or equal to the specified age a".
Thanks to loop expressions, the same property can be expressed in Eiffel with an iteration form of a loop:
across s as c all age (c.item) >= a end
The boolean expression above states that during iteration over the set of cheeses
s with cursor
c, all elements accessible through
c have the age greater than or equal to
a. (In particular, the expression can be written in the postcondition of the function that returns all cheese products that satisfy the age requirement after replacing
Doesn't the loop above resemble the mathematical notation mentioned earlier modulo syntax? Yes, it does! Moreover, the similar notation is adopted for inclusion in Eiffel. It is not exactly the version used in pure math, but pretty close:
∀ c: s ¦ age (c) >= a
Although the expression looks declarative like the math formula, it is completely operational and executable. It is just a syntax version of the
across loop above.
The other variant of loop expressions, using keyword
some, as in an example requirement to have soft cheese among the set
across s as c some moisture (c.item) = soft end
has the symbolic counterpart as well:
∃ c: s ¦ moisture (c) = soft
A few notes about the notation:
- In the symbolic forms of loops, there is no need to specify explicit access to the element at the cursor position by calling feature
- There is no final keyword
end. Several properties could be specified by using conjunction (or other boolean operators as needed), e.g.
∀ c: s ¦ (age (c) >= a ∧ moisture (c) = semi_hard)
- The delimiter between the range part and the property part is a broken vertical bar
¦(the regular vertical bar
|is used for operators).
- Verification parts of loops, like
invariant, as well as an exit condition are unavailable in symbolic forms.
For consistency, a loop instruction also has a symbolic form:
⟳ c: s ¦ print (c.name) ⟲The instruction above prints all names of cheese from the set
s. It is a shortcut for
across s as c loop print (c.item.name) end
The table below summarizes correspondence between keyword-based and symbolic forms of loops:
| || |
| || |
| || |