== 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;
}}}