Changes between Version 5 and Version 6 of Function_Contracts


Ignore:
Timestamp:
01/18/16 20:18:14 (10 years ago)
Author:
zmanchun
Comment:

--

Legend:

Unmodified
Added
Removed
Modified

  • Function_Contracts

    v5 v6  
    66{{{
    77contract: requires* terminates? decreases? simple* behavior* completeness* ;
    8 requires: 'Requires' e ';' ;
     8requires: 'requires' e ';' ;
    99...
    1010simple: ensures | assumes | assigns | reads | guards | depends | ... ;
    11 ensures: 'Ensures' e ';' ;
    12 assumes: 'Assumes' e ';' ;
    13 assigns: 'Assigns' e (',' e)* ';' ;
    14 reads: 'Reads' e (',' e)* ';' ;
    15 depends: 'Depends' e (',' e)* ';' ;
     11ensures: 'ensures' e ';' ;
     12assumes: 'assumes' e ';' ;
     13assigns: 'assigns' e (',' e)* ';' ;
     14reads: 'reads' e (',' e)* ';' ;
     15depends: 'depends' e (',' e)* ';' ;
    1616...
    17 behavior: 'Behavior' id ':' behaviorBody ;
     17behavior: 'behavior' id ':' behaviorBody ;
    1818behaviorBody: behaviorClause+;
    1919behaviorClause: assumes | requires | simple ;
    20 completeness: 'Complete' (id (',' id)*)?
    21             | 'Disjoint' (id (',' id)*)?
     20completeness: 'complete' (id (',' id)*)?
     21            | 'disjoint' (id (',' id)*)?
    2222            ;
    2323}}}
    … …  
    2626{{{
    2727fun[atomic] sendRecv(Int cmd, Pointer buf): Integer
    28   Reads deref(buf);
    29   Behavior send:
    30     Depends writes(buf);
    31     Assigns nothing;
    32   Behavior receive:
    33     Depends access(deref(buf));
    34     Assigns deref(buf);
     28  reads deref(buf);
     29  behavior send:
     30    depends writes(buf);
     31    assigns nothing;
     32  behavior receive:
     33    depends access(deref(buf));
     34    assigns deref(buf);
    3535{
    3636  begin choose
    … …  
    4848== contract clauses ==
    4949
    50 * `Requires e;`: precondition, `e` has `Bool` type and should hold at the entry of the function
    51 * `Terminates e;`: `e` has `Bool` type and if `e` holds then the function should terminate eventually
    52 * `Decreases e ;` or `Decreases e for r`;: decreases clause, where `e` is an expression of type `T` and `r` is an relation over `T`
     50* `requires e;`: precondition, `e` has `Bool` type and should hold at the entry of the function
     51* `terminates e;`: `e` has `Bool` type and if `e` holds then the function should terminate eventually
     52* `decreases e ;` or `decreases e for r`;: decreases clause, where `e` is an expression of type `T` and `r` is an relation over `T`
    5353* simple clauses:
    54  * `Ensures e;`: postcondition, `e` has `Bool` type and should hold when the function terminates
    55  * `Assumes e;`: assumption, `e` has `Bool` type
    56  * `Assigns e0, e1, ...;`: side-effects, `e0, e1, ...` have `Mem` type
     54 * `ensures e;`: postcondition, `e` has `Bool` type and should hold when the function terminates
     55 * `assumes e;`: assumption, `e` has `Bool` type
     56 * `assigns e0, e1, ...;`: side-effects, `e0, e1, ...` have `Mem` type
    5757  * absence of `Assigns` clause does NOT mean that the function has no side-effects
    58   * `Assigns nothing`: means that the function has no side-effects
    59  * `Allocates e0, e1, ...;`: memory units allocated by the function, `e0, e1, ...` have `Mem` type
    60  * `Frees e0, e1, ...;`: memory units deallocated by the function, `e0, e1, ...` have `Mem` type
    61  * `Guards e;`: guard of the function, where `e` has `Bool` type
    62  * `Reads e0, e1, ...;`: memory access, where `e0, e1, ...` have `Mem` type
    63   * similar to `Assigns`
     58  * `assigns nothing`: means that the function has no side-effects
     59 * `allocates e0, e1, ...;`: memory units allocated by the function, `e0, e1, ...` have `Mem` type
     60 * `frees e0, e1, ...;`: memory units deallocated by the function, `e0, e1, ...` have `Mem` type
     61 * `guards e;`: guard of the function, where `e` has `Bool` type
     62 * `reads e0, e1, ...;`: memory access, where `e0, e1, ...` have `Mem` type
     63  * similar to `assigns`
    6464  * absence of `Reads` clause does NOT mean that the function does NOT read anything
    65   * `Reads nothing`: means that the function does NOT read the memory
    66  * `Depends e0, e1, ...;`: dependency relation, where `e0, e1, ...` have `Mem` type
    67  * Note: `Guards`, `Depends` and `Reads` are CIVL extension for ACSL
     65  * `reads nothing`: means that the function does NOT read the memory
     66 * `depends e0, e1, ...;`: dependency relation, where `e0, e1, ...` have `Mem` type
     67 * Note: `guards`, `depends` and `reads` are CIVL extension for ACSL
    6868* named behavior:
    69  * `Behavior id : c0; c1; c2; ...`, where `id` is the name of this behavior, `c0, c1, c2, ...` are behavior clauses
     69 * `behavior id : c0; c1; c2; ...`, where `id` is the name of this behavior, `c0, c1, c2, ...` are behavior clauses
    7070 * behavior clause: a clause that can be used in the body of a behavior, and could be one of the following:
    7171  * assumes clause
    … …  
    7373  * simple clause
    7474* completeness clause
    75  * `Complete;` or `Complete (id0, id1, ...);`:
    76  * `Disjoint;` or `Disjoint (id0, id1, ...);`
     75 * `complete;` or `complete (id0, id1, ...);`:
     76 * `disjoint;` or `disjoint (id0, id1, ...);`
    7777
    7878== depends clause and actions ==