== 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.

== Contracts for sequential programs ==
{{{
Contracts for sequential programs 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.
}}}
== Contracts for MPI programs ==
{{{
Contracts for MPI programs are contracts stating specific properties of MPI programs. MPI contracts must be introduced by an MPI behavior constructor. To be consistent with
}}}