Тогда надо как в Eiffel, чтобы инварианты, предусловия и постусловия были в синтаксис языка встроены:
## Код:
```
Loops

Loop ::=
      [Iteration]
      [Initialization]
      [Invariant]
      [Exit_condition]
      Loop_body
      [Variant]
      end

Iteration ::= across Expression as Identifier

Initialization ::= from Compound

Exit_condition ::= until Boolean_expression

Loop_body ::=
      loop Compound |
      all Boolean_expression |
      some Boolean_expression
```
