== Verify programs with Contracts ==

== Different kinds of contracts ==
CIVL generally provides three kinds of contracts:
* Contracts for sequential programs
* Contracts for MPI 
* Contracts for reduction (see [wiki:ContractReduction])
All these contracts in CIVL are developed as extensions on ACSL language.

==  Sequential contracts ==
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] );
}}}