Changes between Version 9 and Version 10 of ContractReduction


Ignore:
Timestamp:
07/02/14 15:52:05 (12 years ago)
Author:
zmanchun
Comment:

--

Legend:

Unmodified
Added
Removed
Modified

  • ContractReduction

    v9 v10  
    11== Contract Reduction Language  ==
     2
     3== `$depend` clause ==
    24
    35The following contractual clause may appear in a function contract in the same places that `$ensures` or `$requires` clauses can appear:
    … …  
    1921
    2022
    21 DEFAULT (when the `$depend` expression is absent): if no `$ample` expression is present, then the library enabler needs to calculate the ample set.
     23* Things to be decided:
     24   - what shall DEFAULT (when the `$depend` expression is absent) do?
     25   - how to specify the case when we need the library enabler to decide the ample set?
     26   - what keyword to use to specify functions to execute as one step, `$atomic`, `_Atomic`, etc.
    2227
    23 Examples:
     28===  Examples ===
     29
    2430- The following means that any process that can reach the memory unit of `comm` should be in the ample set if the current process (`$self`) is to be chosen in the ample set.
    2531{{{