Changes between Version 8 and Version 9 of VerificationWithContracts


Ignore:
Timestamp:
01/22/16 10:24:53 (10 years ago)
Author:
ziqing
Comment:

--

Legend:

Unmodified
Added
Removed
Modified

  • VerificationWithContracts

    v8 v9  
    1414
    1515== Contracts for MPI programs ==
    16 Contracts for MPI programs are contracts stating specific properties of MPI programs. MPI contracts must be introduced by an
     16Contracts 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.
     17
     18
     19
     20
     21MPI contracts must be introduced by an
    1722MPI behavior constructor `\mpi_collective(MPI_Comm, Collective_Kind)` which should be used in a similar way as ACSL `behavior`.