Changes between Version 9 and Version 10 of VerificationWithContracts


Ignore:
Timestamp:
01/22/16 10:27:23 (10 years ago)
Author:
ziqing
Comment:

--

Legend:

Unmodified
Added
Removed
Modified

  • VerificationWithContracts

    v9 v10  
    1414
    1515== Contracts for MPI programs ==
    16 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.
     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. 
    1717
    18 
    19 
    20 
    21 MPI contracts must be introduced by an
    22 MPI behavior constructor `\mpi_collective(MPI_Comm, Collective_Kind)` which should be used in a similar way as ACSL `behavior`.
     18== MPI extensions on ACSL ==