# Symbolic forms of loops

- Tags:
- loop
- Unicode
- symbolic loop

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:

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) ⟲` |