The contracts specification of CIVL-C is based on ACSL, with additional primitives and constructs for various purposes, such as function guard, function dependency, MPI function behavior, etc.

== overview ==
The grammar for the contract specification of a function is as follows:

{{{
contract: requires* terminates? decreases? simple* behavior* completeness* ;
requires: 'Requires' e ';' ;
...
simple: ensures | assumes | assigns | reads | guards | depends | ... ;
ensures: 'Ensures' e ';' ;
assumes: 'Assumes' e ';' ;
assigns: 'Assigns' e (',' e)* ';' ;
reads: 'Reads' e (',' e)* ';' ;
depends: 'Depends' e (',' e)* ';' ;
...
behavior: 'Behavior' id ':' behaviorBody ;
behaviorBody: behaviorClause+;
behaviorClause: assumes | requires | simple ;
completeness: 'Complete' (id (',' id)*)? 
            | 'Disjoint' (id (',' id)*)? 
            ;
}}}

Example
{{{
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:
}

}}}

== contract clauses ==

* `Requires e;`: precondition, `e` has `Bool` type and should hold at the entry of the function
* `Terminates e;`: `e` has `Bool` type and if `e` holds then the function should terminate eventually
* `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;`: postcondition, `e` has `Bool` type and should hold when the function terminates
 * `Assumes e;`: assumption, `e` has `Bool` type
 * `Assigns e0, e1, ...;`: side-effects, `e0, e1, ...` have `Mem` type
  * absence of `Assigns` clause does NOT mean that the function has no side-effects
  * `Assigns \nothing`: means that the function has no side-effects
 * `Allocates e0, e1, ...;`: memory units allocated by the function, `e0, e1, ...` have `Mem` type
 * `Frees e0, e1, ...;`: memory units deallocated by the function, `e0, e1, ...` have `Mem` type
 * `Guards e;`: guard of the function, where `e` has `Bool` type
 * `Reads e0, e1, ...;`: memory access, where `e0, e1, ...` have `Mem` type
  * similar to `Assigns`
  * absence of `Reads` clause does NOT mean that the function does NOT read anything
  * `Reads \nothing`: means that the function does NOT read the memory
 * `Depends e0, e1, ...;`: dependency relation, where `e0, e1, ...` have `Mem` type
 * Note: `Guards`, `Depends` and `Reads` are CIVL extension for ACSL

* 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:
}
}}}