Changes between Version 144 and Version 145 of IR

Timestamp:

05/11/16 14:02:44 (10 years ago)

Author:

zmanchun

Comment:

--

IR

@@ -433 +433 @@
 
 Function modifiers that may be placed in the brackets after `fun`:
-* `pure` : the value returned by the function is a deterministic function of the inputs (so cannot depend on the state in any way), and furthermore the function has no side-effects.  So this is just like a mathematical function.  (This is intended to be used for system functions, but can it also be used for non-system functions?)
+* `state_f` : the value returned by the function is a deterministic function of the inputs (so cannot depend on the state in any way), and furthermore the function has no side-effects.  So this is just like a mathematical function.  (This is intended to be used for system functions, but can it also be used for non-system functions?)
 * `abstract`: an uninterpreted pure function.  The result of a function call on such a function is a symbolic expression "`f(arg1, ...)`".   There is no definition for such a function, not even a system definition.
 * `atomic`: function definition is atomic, and it never blocks.  A function call to such a function occurs in a single atomic transition.  It is slightly different than a function in which the entire body is atomic, because in the latter case the call and return happen as two separate transitions.