loops.tex 873 Bytes
Newer Older
1
\begin{syntax}
Julien Signoles's avatar
Julien Signoles committed
2
  statement ::= "/*@" loop-annot "*/" ;
Julien Signoles's avatar
Julien Signoles committed
3
  "while" "(" C-expression ")" C-statement ;
Julien Signoles's avatar
Julien Signoles committed
4
  | "/*@" loop-annot "*/" ;
5
    "for";
Julien Signoles's avatar
Julien Signoles committed
6
  "(" C-expression ";" C-expression ";" C-expression ")";
7
  statement ;
Julien Signoles's avatar
Julien Signoles committed
8
  | "/*@" loop-annot "*/" ;
Julien Signoles's avatar
Julien Signoles committed
9 10
  "do" C-statement ;
  "while" "(" C-expression ")" ";"
11
  \
Julien Signoles's avatar
Julien Signoles committed
12
  loop-annot ::= loop-clause* ;
13 14 15
  { loop-behavior* } ;
  { loop-variant? }
  \
Julien Signoles's avatar
Julien Signoles committed
16
  loop-clause ::= loop-invariant ;
17 18
                | { loop-assigns }
  \
19
  [ loop-invariant ] ::= { clause-kind? } [ "loop" "invariant" pred ";" ] ;
20 21 22 23
  \
  { loop-assigns } ::= { "loop" "assigns" locations ";" } ;
  \
  { loop-behavior } ::= { "for" id ("," id)* ":" } ;
24
  { loop-clause* } ; \hspace{-35mm} annotation for behavior $id$
25 26
  \
  { loop-variant } ::= { "loop" "variant" term ";" } ;
27
  | { "loop" "variant" term "for" id ";" } ;  \hspace{-35mm} variant for relation $id$
28
\end{syntax}