Changes between Version 24 and Version 25 of ContractReduction


Ignore:
Timestamp:
12/07/15 11:49:02 (10 years ago)
Author:
zmanchun
Comment:

--

Legend:

Unmodified
Added
Removed
Modified

  • ContractReduction

    v24 v25  
    22
    33== ACSL function contract grammar with CIVL-C extension (in bold) ==
    4 
    5 `function-contract ::= requires-clause∗ terminates-clause? decreases-clause?`
    6                                  `simple-clause∗ named-behavior∗ completeness-clause∗`
    7 
    8 `requires-clause ::= requires pred ;`
    9 
    10 `terminates-clause ::= terminates pred ;`
    11 
    12 `decreases-clause  ::= decreases term (for id)? ;`
    13 
    14 `simple-clause ::= assigns-clause | ensures-clause | allocation-clause | abrupt-clause-fn`
    15 
    16 `assigns-clause ::= assigns locations ;`
    17 
    18 `locations ::= location (, location) ∗ | \nothing |` **\everything**
    19 
    20 `location ::= tset`
    21 
    22 `ensures-clause ::= ensures pred ;`
    23 
    24 `named-behavior ::= behavior id : behavior-body`
    25 
    26 `behavior-body ::= assumes-clause∗ requires-clause∗ simple-clause∗`
    27 
    28 `assumes-clause ::= assumes pred ;`
    29 
    30 `completeness-clause ::= complete behaviors (id (, id)∗)? ;`
    31                       `| disjoint behaviors (id (, id)∗)? ;`
     4{{{
     5function-contract ::= requires-clause∗ terminates-clause? decreases-clause?
     6                      simple-clause∗ named-behavior∗ completeness-clause∗
     7requires-clause ::= requires pred ;
     8terminates-clause ::= terminates pred ;
     9decreases-clause  ::= decreases term (for id)? ;
     10simple-clause ::= assigns-clause | ensures-clause
     11                | allocation-clause | abrupt-clause-fn
     12assigns-clause ::= assigns locations ;
     13locations ::= location (, location) ∗ | \nothing |` $everything
     14location ::= tset
     15ensures-clause ::= ensures pred ;
     16named-behavior ::= behavior id : behavior-body
     17behavior-body ::= assumes-clause∗ requires-clause∗ simple-clause∗
     18assumes-clause ::= assumes pred ;
     19completeness-clause ::= complete behaviors (id (, id)∗)? ;
     20                      | disjoint behaviors (id (, id)∗)? ;
     21term ::= \old ( term ) | \result
     22pred ::= \old ( pred )
     23}}}
    3224
    3325{{{
    … …  
    4638}}}
    4739
    48 `term ::= \old ( term ) | \result`
    49 
    50 `pred ::= \old ( pred )`
    51 
    5240
    5341== `$memory` type ==
    … …  
    6351
    6452As in other contract specification language, this contract clause is used to specify a set of existing memory units.    The claim is that if an existing memory unit is not in the set, it will not be modified in the course of the function call.  The syntax is:
    65 `assigns location (, location)*` or `assigns \nothing`
    6653
    67 where `<memory-list>` is a comma-separated list of expressions of type `$memory`.
     54`assigns location (, location)*` or `assigns \nothing` or `assigns $everything`
     55
     56where `location` is a `tset` expressions of type `$memory`.
    6857
    6958Example:
    … …  
    7766This contractual clause specifies part of the dependence relation used in POR.
    7867{{{
    79 $depends {e}
     68$depends event (, event)*
    8069}}}
    81 where `e` is an expression of boolean type.   For each process `p`, the `e` can be evaluated in the context of `p`.   If `e` evaluates to `true`, then `p` must be included in an ample set containing a call to this function.
     70where `event` is a memory event represented as a boolean expression.   For each process `p`, the `event ` can be evaluated in the context of `p`.   If `event ` evaluates to `true`, then `p` must be included in an ample set containing a call to this function.
    8271
    8372The expression `e` hence defines a predicate d(s,p), where s ranges over states, and p over procs.   The requirement is the following: