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 s with Result.)

Doesn't the loop above resemble the mathematical notation mentioned earlier modulo syntax? Yes, it does! Moreover, a 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 s 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 item.
• 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 variant and 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 symbolic forms address the most common cases, making them more concise, and closer to classical mathematical notation. They do not support more elaborate cases; for example, they have no room for loop invariants and variants. For all cases which do not fit into these restrictions, use the full across ... or from ... form.

The table below summarizes correspondence between keyword-based and symbolic forms of loops: