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

== MPI extensions on ACSL ==