# Symbolic forms of loops

by Alexander Kogtenkov (modified: 2024 Mar 26)

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:

Loop syntax
Syntax form
iteration symbolic
`across s as c all f (c.item) end` `∀c: s ¦ f (c)`
`across s as c some f (c.item) end` `∃ c: s ¦ f (c)`
`across s as c loop g (c.item); h (c.item) end` `⟳ c: s ¦ g (c); h (c) ⟲`