Changes between Version 42 and Version 43 of IR2

Timestamp:

04/28/21 17:53:22 (5 years ago)

Author:

siegel

Comment:

--

IR2

@@ -28 +28 @@
 1. a type for $state ? 
 1. How do you model `malloc` when the element type is not known?  (Create a type `$byte`?)
-1. How do you specify the guard of a system function (this should be the name of another function)
 1. How do you iterate over a domain?
 
@@ -41 +40 @@
   | 'typedef' type-specifier declarator ';'
   ;
-decl: qualifier* type-specifier declarator contract-clause* ';' ;
+decl: qualifier* type-specifier declarator guard-clause? contract-clause* ';' ;
 function-definition: qualifier* type-specifier declarator contract-clause* block ;
 qualifier:
@@ -52 +51 @@
   | '$system' '<' STRING ',' STRING '>'  /* function is defined in system code elsewhere */
   ;
+guard-clause: '$when' '(' ID ')' ;
 block: '{' typedef* decl* function-definition* statement* '}' ;
 statement: block | simpleStmt | chooseStmt ;
@@ -78 +78 @@
 * `$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.
 * `$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. 
+* 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.
+* Contract clauses can occur only with system function and defined functions (not with abstract functions, not with variables).
 * A program must contain a function definition for a function named `main`.
 * `$input` and `$output` can be used only on global variable declarations (not on function definitions, not in block scope).