expr2.bnf 248 Bytes
Newer Older
1 2 3 4 5 6 7 8 9 10 11
\begin{syntax}
  assert ::= "assert" | "assume" | "check"
  \
  to-downto ::= "to" | "downto"
  \
  loop-annot ::= loop-inv? variant?
  \
  loop-inv ::= "invariant" annotation
  \
  variant ::= "variant" "{" term "}" ("with" lqualid)?
\end{syntax}