multi-lines spec comments /*@ ... */
axioms, with syntax //@ assume ...;
assignments operators ++ -- += etc. for array elements