== Verify Programs with Contracts ==

The CIVL contract system is based on ACSL (http://frama-c.com/acsl.html), and it contains four categories:

* Contracts for sequential programs
* Contracts for MPI 
* Contracts for state space reduction (see [wiki:ContractReduction])
* Loop invariants

Note that the first three are also called function contracts, while the last is called loop contract.

Additional primitives that extend ACSL include:
* contract primitives for MPI
 * MPI collective contract
 * remote expressions
* contract primitives for dependency relation
  * `depends` clause: specify the dependency relation of the function, usually used for partial order reduction (POR) or other analysis
  * `\calls(fun, arg0, arg1, ...)`: a set of actions that invokes the function with the specified arguments
  * `\noact`: empty set of actions 
  * `\anyact`: any action sets 
  * set of memory actions: `\read(mu-list)`, `\write(mu-list)`
  * action set operations: `+` union, `-` complement, `&` intersect
  * `reads` clause: specify memory locations read by the function, the syntax of which is similar to `assigns` clause
* malicious primitives
  * wildcard term: `...`
 * additional parameter for `allocates` clause: specify the scope of the heap for allocation; if absent then the root scope is used
 * extension for range with steps: `lo .. hi # step`

The contract grammar could be found bellow:

{{{
function-contract ::= requires-clause∗ terminates-clause? decreases-clause? guards-clause?
                      simple-clause∗  named-behavior∗ completeness-clause∗ 
requires-clause ::= requires pred ;
terminates-clause ::= terminates pred ;
decreases-clause  ::= decreases term (for id)? ;
guards-clause ::= guards pred ;
simple-clause ::= assigns-clause | ensures-clause 
                | allocation-clause | abrupt-clause-fn
                | reads-clause | depends-clause
assigns-clause ::= assigns tsets ;
tsets ::= location (, location) ∗
ensures-clause ::= ensures pred ;
allocation-clause ::= allocates tsets (, scope)? ; | frees tsets ;
reads-clause ::= reads tsets;
depends-clause := depends event (, event)*;
named-behavior ::= behavior id : behavior-body
behavior-body ::= assumes-clause∗ requires-clause∗ simple-clause∗
assumes-clause ::= assumes pred ;
completeness-clause ::= complete behaviors (id (, id)∗)? ;
                      | disjoint behaviors (id (, id)∗)? ;
term ::= \old ( term ) | \result | \nothing | ...
pred ::= \old ( pred )
}}}

{{{
tset ::= \empty
       | tset -> id 
       | tset . id * tset
       | & tset
       | tset [ tset ]
       | term? .. term?
       | \union ( tset (, tset)∗ )
       | \inter ( tset (, tset)∗ )
       | tset + tset
       | ( tset )
       | { tset | binders (; pred)? }
       | { term } term
}}}

{{{
literal ::= \true | \false | integer | real | string | character
}}}

{{{
bin-op ::= + | - | * | / | % | << | >>
         | == | != | <= | >= | > | <
         | && | || | ^^
         | & | | | --> | <--> | ^
}}}

{{{
unary-op ::= + | - | ! | ~ | * | & 
}}}

{{{
term ::= literal | id | unary-op term | term bin-op term | term [ term ]
       | { term \with [ term ] = term } 
       | term . id
       | {term \with.id =term }
       | term -> id
       | ( type-expr ) term
       | id ( term (, term)∗ )
       | (term)
       | term ? term : term
       | \let id = term ; term sizeof ( term )
       | sizeof ( C-type-name )
       | id : term 
       | string : term
}}}


==  Contracts for Sequential Programs ==
Sequential contracts are based on the theory of Hoare Logic. Contracts only state sequential properties on either 
the pre-state or post-state of the given procedure. All sequential contract constructors are inherited from ACLS, CIVL will start 
from supporting part of them.

== MPI contracts ==
MPI contracts are contracts stating specific properties of MPI programs. Since there is much difference between sequential and concurrent programs, checking and reasoning MPI programs requires a unique system. Obviously the two states (pre- and post-) system is not suitable for concurrent programs. 

== Notations of MPI contracts ==
`MPI-Collective-Block` 
{{{
Collective-signature ::= "\mpi_collective(MPI_Comm, COLLECTIVE_KIND)";
Collective-body ::= (ACSL-clause)* ;
Collective-block ::= Collective-signature : Collective-body;
}}}

`MPI-Empty-In` && `MPI-Empty-Out`  expressions
{{{

}}}

== Pointers & Alias ==
Pointers can be asserted as valid pointers via using ACSL constructor `\valid`. ACSL allows programmers specify a set of valid
pointers which requires CIVL to be able to represent a `set`.

CIVL has a typing rule: {{{  pointer PLUS CIVL_Range ==> An array of pointers  }}}. Other sets of different types may have the similar typing rule.

For CIVL, coping with a `\valid` expression is tricky. For `\valid` expressions appear in assurances, one can implement the evaluation semantics
on a specific state. However, `\valid` appears in requirements brings problems, it heavily affects how CIVL constructs an initial state.

For example:
{{{
/*@ requires (\valid(p) || !\valid(p) ) && \valid(q);
*/
foo(int * p, int * q);
}}}
The construction of an initial state seems to be irrelevant to if the pointer p is valid or not, but when CIVL recursively analyzes the requirement
predicate, it's hard to know if it's relevant or not. Thus my rough solution is :
  1. Making `\valid` expressions uninterpreted functions;
  2. Pointer "p" should be valid initially only if {{{ requirement => valid_of_p }}};
  3. Vice versa, pointer "p" should be undefined initially only if {{{ requirement => !valid_of_p }}};
  4. Otherwise, it's a non-deterministic choice.

Considering pointer alias, I'm planning such an approach:
  First, there is an outer scope outside of the source function which is going to be verified. It can be used to represent a set of all visible 
  scopes from the source function. Thus, for each pointer argument, creating a unique unconstraint array element in the outer scope. 
{{{
$input int X[2];  // one for each pointer

/*@ requires \valid(p) && \valid(q);
*/
foo(int *p, int *q);
}}}
For this example, considering aliasing, the context can be 
{{{
( ( \valid(p) && \valid(q) ) => \valid(p) ) => (exists i, 0 <= i < 2 such that *p == X[i] );
}}}