== 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:
{{{


}}}