Changes between Version 123 and Version 124 of IR

Timestamp:

12/09/15 22:07:04 (10 years ago)

Author:

siegel

Comment:

--

IR

@@ -416 +416 @@
 
 Function modifiers that may be placed in the brackets after `fun`:
-* `pure` : the function has no side effects, but may be nondeterministic
- * **DO WE NEED TWO SEPARATE MODIFIERS?  One that says no side-effects, one that says deterministic?  For example, `choose_int` has no side-effects, but is not deterministic.  And a non-deterministic function can NOT be used as an expression.
-* `abstract`: an uninterpreted function.  The result of a function call on such a function is a symbolic expression "`f(arg1, ...)`".
+* `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?)
+* `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.
  * Since every system function is atomic, this option is only useful for non-system functions.
@@ -430 +429 @@
 * A system function will have no body.  It may have any number (including 0) of contract clauses.
 * If the system function is called anywhere in the program, it must be defined by providing Java code in an Enabler and Executor.  Failure to do so will result in an exception.
-* A system function may modify only memory it can reach.  This includes allocating new data on heaps it can reach.   This modifiable memory can be further limit by the contract.
+* A system function may modify only memory it can reach.  This includes allocating new data on heaps it can reach.   This modifiable memory can be further limited by the contract.
 * A system function may have a guard, which is another function taking the same types of inputs, but returning `Bool`.