== contract clauses ==

* `requires e;`: precondition, `e` should hold at the entry of the function
* `terminates e;`: 
* `decreases e ;` or `decreases e for r`;: decreases clause, where `e` is an expression of type `T` and `r` is an relation over `T`
* simple clauses:
 * `ensures e;`
 * `assumes e;`
 * `assigns e0, e1, ...;`
 * `allocates e0, e1, ...;`
 * `frees e0, e1, ...;`
 * `guards e;`
 * `reads e0, e1, ...;`
 * `depends e0, e1, ...;`

* action expressions:
 * `read(e)`: `e` has type `Mem`. The function reads the memory units specified by `e`.
 * `write(e)`: `e` has type `Mem`. The function writes the memory units specified by `e`.
 * `call(f, <e1, ...>)`: `f` has type `Function`. The function calls `f` with parameters `e1, ...`.
 * `noaction`: no action
 * `anyaction`: all actions
 * `act_union(ma0, ma1)`: the union of the two memory set actions `ma0` and `ma1`.
 * `act_comp(ma0, ma1)`: action complement (everything not in `ma1`)
 * `act_isect(ma0, ma1)`: action intersection

* depends clause: `depends action0, action1, action2, ... `
 * Example: `depends act_union(act_comp(read(n), call(inc, <x>))), call(dec, <y>))`
 * absence of depends clause: there is no information about the dependency of the function, which means that the analysis needs to figure it out by itself.
* some facts about assigns-or-reads clause
 * absence of `reads`/`assigns` clause: there is no assumption about the read/assign access of the function, i.e., the function could read/assign anything
  * absence of `assigns` clause: similar to the absence of `reads` clause
 * `reads/assigns nothing` doesn’t necessarily means that the function never reads or assigns any variable. The function could still reads/assigns its “local” variables, including function parameters and any variable declared inside the function body. **check it**

* For an independent function which has `depends coaction`, usually we also need to specify `reads nothing`, for the purpose of reachability analysis.
e.g., 
{{{
/* Returns the size of the given bundle b. */
bundle_size(Bundle b): Integer
  depends nothing
  reads b
  ;
}}}

* Example of a function declaration with contracts: 
{{{
fun[atomic] sendRecv(Int cmd, Pointer buf): Integer
  reads deref(buf);
  behavior send:
    depends writes(buf);
    assigns nothing;
  behavior receive:
    depends access(deref(buf));
    assigns deref(buf);
{
  begin choose
  when eq(cmd, 0)
     do CALL send, <buf, ...>; goto L1;
  when eq(cmd, 1)
    do CALL recv, <buf, ...>; goto L1;
  when and(neq(cmd, 0), neq(cmd, 1))
    do NOOP; goto L1;
  end choose
L1:
}
}}}