\begin{syntax}
spec ::= requires | ensures | returns | raises ;
| reads | writes | variant
\
requires ::= "requires" "{" formula "}"
\
ensures ::= "ensures" "{" formula "}"
\
returns ::= "returns" "{" "|"? formula-case ("|" formula-case)* "}"
\
reads ::= "reads" "{" term ( "," term )* "}"
\
writes ::= "writes" "{" term ( "," term )* "}"
\
raises ::= "raises" "{" "|"? raises-case ("|" raises-case)* "}" ;
| "raises" "{" uqualid ("," uqualid)* "}"
\
raises-case ::= uqualid pattern? "->" formula
\
variant ::= "variant" "{" one-variant ("," one-variant)+ "}"
\
one-variant ::= term ("with" variant-rel)?
\
variant-rel ::= lqualid
\
invariant ::= "invariant" "{" formula "}" ;
\
assertion ::= ("assert" | "assume" | "check") "{" formula "}" ;
| "absurd"
\end{syntax}