assertions.tex 311 Bytes
Newer Older
1
\begin{syntax}
Julien Signoles's avatar
Julien Signoles committed
2
  C-compound-statement ::= "{" declaration* statement* assertion+ "}"
3
        \
Julien Signoles's avatar
Julien Signoles committed
4
  C-statement ::= assertion statement \
5
6
7
  assertion-kind ::= "assert" | "check" \
  assertion ::= "/*@" assertion-kind pred ";" "*/" ;
  | { "/*@" "for" id ("," id)* ":" assertion-kind pred ";" "*/" } ;
8
\end{syntax}