Changes between Version 7 and Version 8 of VerificationWithContracts


Ignore:
Timestamp:
01/22/16 10:05:56 (10 years ago)
Author:
ziqing
Comment:

--

Legend:

Unmodified
Added
Removed
Modified

  • VerificationWithContracts

    v7 v8  
    99
    1010== Contracts for sequential programs ==
    11 {{{
    1211Contracts for sequential programs are based on the theory of Hoare Logic. Contracts only state sequential properties on either
    1312the pre-state or post-state of the given procedure. All sequential contract constructors are inherited from ACLS, CIVL will start
    1413from supporting part of them.
    15 }}}
     14
    1615== Contracts for MPI programs ==
    17 {{{
    1816Contracts for MPI programs are contracts stating specific properties of MPI programs. MPI contracts must be introduced by an
    19 MPI behavior constructor `\mpi_collective(MPI_Comm, Collective_Kind)` which should be used in a similar way as ACSL
    20  `guards`
    21 }}}
     17MPI behavior constructor `\mpi_collective(MPI_Comm, Collective_Kind)` which should be used in a similar way as ACSL `behavior`.