Changes between Version 47 and Version 48 of IR2


Ignore:
Timestamp:
04/28/21 20:42:30 (5 years ago)
Author:
siegel
Comment:

--

Legend:

Unmodified
Added
Removed
Modified

  • IR2

    v47 v48  
    3838  | 'typedef' type-specifier declarator ';'
    3939  ;
    40 decl: qualifier* type-specifier declarator guard-clause? contract-clause* ';' ;
     40decl: qualifier* type-specifier declarator contract-clause* ';' ;
    4141function-definition: qualifier* type-specifier declarator contract-clause* block ;
    4242qualifier:
    … …  
    4949  | '$system' '<' STRING ',' STRING '>'  /* function is defined in system code elsewhere */
    5050  ;
    51 guard-clause: '$when' '(' ID ')' ;
    5251block: '{' typedef* decl* function-definition* statement* '}' ;
    5352statement: block | simpleStmt | chooseStmt ;
    … …  
    5958expression-list: expr (',' expr)* ;
    6059gotoStmt: 'goto' ID ;
    61 contract-clause :
    62     '$assigns' expr ';'
    63   | '$requires' expr ';'
    64   | '$ensures' expr ';'
    65    ...
    6660INT: ... /* integer constant */
    6761ID: ... /* identifier */
    … …  
    7872* `$pure` can be applied to a system function or defined function only.  (An abstract function is necessarily pure.)  The use of `$pure` indicates that the function has no side-effects, and the value returned in a mathematical function of the arguments.    If the function is not actually pure, the behavior is undefined.
    7973* `$state_f` can be applied to a system function or defined function only.   It declares that the function has no side-effects, and the value returned is a mathematical function of the state in which the call occurred; i.e., the value returned may depend on the arguments in the call, the values of global variables, or any other component of the state.  But, if called twice from the same state, it will always return the same value.   If the function does not actually have this property, the behavior is undefined.   Any `$pure` function is necessarily a `$state_f`, so at most one of these two qualifiers can occur in a declaration or definition.
    80 * A guard clause can occur only in the declaration of a system function.  The identifier is the name of the function that will be used as the guard in all calls to the system function.  The guard function must have the same input signature as the system function, but must return `$bool`.    Any call to the system function will block unless the guard function returns `$true` on the arguments used in the call.   The execution of the system function and the return of "true" from the guard function will occur atomically, i.e., no state change will occur between the return of true and the call of the system function.   The guard function must be a `$state_f` function; in particular, it must be side-effect free.  The guard function may be a system function or a defined function; it cannot be abstract.   If omitted, the guard is understood to be "true", i.e., a call to the system function will never block.
    8174* Contract clauses can occur only with system function and defined functions (not with abstract functions, not with variables).
    8275* A program must contain a function definition for a function named `main`.
    8376* `$input` and `$output` can be used only on global variable declarations (not on function definitions, not in block scope).
    8477* The `expr` in a guard must have type `$bool`.
    85 * The expressions in a dependency clause must have pointer type.   This declares that the following transition depends only on the objects pointed to. 
    8678
    8779{{{
    … …  
    9385   $assume($defined(a, 0, 10)); // ?
    9486}}}
     87
     88== Contracts ==
     89
     90{{{
     91contract-clause:
     92    '$assigns' '(' expression-list? ')'   /* frame condition */
     93  | '$requires' '(' expr ')'  /* precondition */
     94  | '$ensures' '(' expr ')'  /* postcondition */
     95  | '$depends_on' '(' expression-list? ')'  /* dependency specification */
     96  | '$when '(' ID ')'  /* guard clause */
     97  ;
     98}}}
     99
     100=== Notes ===
     101
     102* A guard clause can occur only in the declaration of a system function.  The identifier is the name of the function that will be used as the guard in all calls to the system function.  The guard function must have the same input signature as the system function, but must return `$bool`.    Any call to the system function will block unless the guard function returns `$true` on the arguments used in the call.   The execution of the system function and the return of "true" from the guard function will occur atomically, i.e., no state change will occur between the return of true and the call of the system function.   The guard function must be a `$state_f` function; in particular, it must be side-effect free.  The guard function may be a system function or a defined function; it cannot be abstract.   If omitted, the guard is understood to be "true", i.e., a call to the system function will never block.
     103* The expressions in a dependency clause must have pointer type.   This declares that the following transition depends only on the objects pointed to. 
     104
    95105
    96106== Types ==