| Version 3 (modified by , 10 years ago) ( diff ) |
|---|
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.
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.
Note:
See TracWiki
for help on using the wiki.
