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