Changes between Version 10 and Version 11 of VerificationWithContracts


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

--

Legend:

Unmodified
Added
Removed
Modified

  • VerificationWithContracts

    v10 v11  
    88All these contracts in CIVL are developed as extensions on ACSL language.
    99
    10 == Contracts for sequential programs ==
    11 Contracts for sequential programs are based on the theory of Hoare Logic. Contracts only state sequential properties on either
     10==  Sequential contracts ==
     11Sequential contracts are based on the theory of Hoare Logic. Contracts only state sequential properties on either
    1212the pre-state or post-state of the given procedure. All sequential contract constructors are inherited from ACLS, CIVL will start
    1313from supporting part of them.
    1414
    15 == 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.
     15== MPI contracts ==
     16MPI 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.
    1717
    18 == MPI extensions on ACSL ==
     18== Notations of MPI contracts ==