\begin{syntax}
  C-compound-statement ::= "{" declaration* statement* assertion+ "}"
        \
  C-statement ::= assertion statement \
  assertion-kind ::= "assert" | "check" \
  assertion ::= "/*@" assertion-kind pred ";" "*/" ;
  | { "/*@" "for" id ("," id)* ":" assertion-kind pred ";" "*/" } ;
\end{syntax}