Changes between Version 48 and Version 49 of IR2


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

--

Legend:

Unmodified
Added
Removed
Modified

  • IR2

    v48 v49  
    4343    '$input'  /* input variable; only for global decls */
    4444  | '$output'  /* output variable; only for global decls */
    45   | '$abstract'  /* abstract function; only for function decls */
    46   | '$pure'  /* function is a mathematical function of its parameters */
     45  | '$abstract_f'  /* abstract function; only for function decls */
     46  | '$pure_f'  /* function is a mathematical function of its parameters */
    4747  | '$state_f'  /* function is a mathematical function of the state */
    4848  | '$atomic_f'  /* function invocations take place atomically */
    49   | '$system' '<' STRING ',' STRING '>'  /* function is defined in system code elsewhere */
     49  | '$system_f' '<' STRING ',' STRING '>'  /* function is defined in system code elsewhere */
    5050  ;
    5151block: '{' typedef* decl* function-definition* statement* '}' ;
    … …  
    6666
    6767* A declaration declares a variable to have either an object type or a function type.   (An object type is any type that is not a function type.)
    68 * A variable of function type represents either an abstract or a system function.   The declaration of such a variable must use either the qualifier `$abstract` or `$system`.  Moreover, those two qualifiers can only be used in a declaration of function type.
     68* A variable of function type represents either an abstract or a system function.   The declaration of such a variable must use either the qualifier `$abstract_f` or `$system_f`.  Moreover, those two qualifiers can only be used in a declaration of function type.
    6969* An abstract function represents a new uninterpreted pure function.
    70 * A system function has no definition in CIVL-IR, but is instead defined elsewhere (for example, in C or Java code).  Such a function will always be executed atomically.   The first string specifies a path (e.g., Java package) to the library containing the function, the second is the name of the library.    These two Strings should be enough to tell CIVL where to find the system definition of the function.
    71 * `$atomic_f` can only be used in a function definition.  It indicates that a defined function is to behave atomically, i.e., every call to such a function will behave as if the call occurred in an `$atomic` block.    (An abstract or system function must necessarily be atomic.)
    72 * `$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.
    73 * `$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.
    74 * Contract clauses can occur only with system function and defined functions (not with abstract functions, not with variables).
     70* A system function has no definition in the program, but is instead defined elsewhere (for example, in C or Java code).  Such a function will always be executed atomically.   The first string specifies a path (e.g., Java package) to the library containing the function, the second is the name of the library.    These two Strings should be enough to tell CIVL where to find the system definition of the function.
     71* `$atomic_f` can only be used in a function definition.  It indicates that a defined function is to behave atomically, i.e., every call to such a function will be executed as if in atomic region.    (An abstract or system function must necessarily be atomic.)
     72* `$pure_f` can be applied to a system function or defined function only.  (An abstract function is necessarily pure.)  The use of `$pure_f` 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.
     73* `$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_f` function is necessarily a `$state_f`, so at most one of these two qualifiers can occur in a declaration or definition.
     74* Contract clauses can occur only with system functions and defined functions (not with abstract functions, not with variables).
    7575* A program must contain a function definition for a function named `main`.
    7676* `$input` and `$output` can be used only on global variable declarations (not on function definitions, not in block scope).