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
* named behavior:
 * `behavior id : c0; c1; c2; ...`, where `id` is the name of this behavior, `c0, c1, c2, ...` are behavior clauses
 * behavior clause: a clause that can be used in the body of a behavior, and could be one of the following:
  * assumes clause
  * requires clause
  * simple clause
* completeness clause
 * `complete;` or `complete (id0, id1, ...);`: 
 * `disjoint;` or `disjoint (id0, id1, ...);`

== depends clause and actions ==

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