spec.bnf 854 Bytes
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30
\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}