Changes between Version 38 and Version 39 of ContractReduction


Ignore:
Timestamp:
12/11/15 13:35:05 (10 years ago)
Author:
zmanchun
Comment:

--

Legend:

Unmodified
Added
Removed
Modified

  • ContractReduction

    v38 v39  
    11== Contract Reduction Language  ==
    22
    3 == ACSL function contract grammar with CIVL-C extension (starting with `$`) ==
     3== ACSL function contract grammar with CIVL-C extension ==
    44The CIVL-C function contract extends ACSL function contract with the following elements:
    55* `guards` clause: specify the guard of a function, i.e., the specified predicate should hold in order to enable the execution of the function body
    … …  
    88 * `\noact`: empty set of actions
    99 * `\anyact`: any actions
     10 * memory actions: `\read(mu-list)`, `\write(mu-list)`
     11 * action operations: `+`, `-`, `&`
    1012* `reads` clause: specify memory locations read by the function, the syntax of which is similar to `assigns` clause
    1113* additional parameter for `allocates` clause: specify the scope of the heap for allocation; if absent then the root scope `$root` is used
    … …  
    7981This contractual clause specifies part of the dependence relation used in POR.
    8082{{{
    81 depends event (, event)*
    82 }}}
    83 where `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.
     83depends action (, action)*
     84}}}
     85where `action` is an action represented as a boolean expression.   For each process `p`, the `action ` can be evaluated in the context of `p`.   If `action ` evaluates to `true`, then `p` must be included in an ample set containing a call to this function.
    8486
    8587The grammar of `event` is defined as follows:
    … …  
    9092 | \write(MemorySetExpression)
    9193 | \calls(FunctionCallExpression)
    92  | \nothing
    93  | \everything
     94 | \noact
     95 | \anyact
    9496 | ‘(’ EventSetExpression ‘)’
    9597 | EventSetExpression + EventSetExpression
    … …  
    195197
    196198{{{
    197 guard bool-expr
     199guards bool-expr
    198200}}}
    199201
    … …  
    227229/*@ requires barrier != \null;
    228230  @ guards true;
    229   @ depends \nothing;
     231  @ depends \noact;
    230232  @ assigns barrier;//barrier has pointer type, and is converted into $memory type automatically
    231233  @ */
    … …  
    284286{{{
    285287/* Calls the barrier associated with this local barrier object.*/
    286 /*@ depends \nothing;
     288/*@ depends \noact;
    287289  @ assigns \nothing; // although the barrier records is updated but it gets cleaned up when the method returns
    288290  @*/