Changes between Version 86 and Version 87 of IR

Timestamp:

11/29/15 10:52:03 (10 years ago)

Author:

siegel

Comment:

--

IR

@@ -48 +48 @@
 {{{
 fun f(u:Integer, a:Array[Real]): Integer {
-  x: Real;
-  y: Real;
-  z: Float[16,23];
+  var x: Real;
+  var y: Real;
+  var z: Float[16,23];
  
 L1 :
@@ -79 +79 @@
 {{{
 {
-  x: Integer;
-  a_t : Dytype[Array[Integer]];
-  a: Array[Integer];
+  var x: Integer;
+  var a_t : Dytype[Array[Integer]];
+  var a: Array[Integer];
 
   ASSIGN "x", mul(3,"y");
@@ -150 +150 @@
 type S=Tuple[<Array[Integer]>];
 
-n: Integer;
-S_d: Dytype[S];
-x1: S;
-x2: S;
+var n: Integer;
+var S_d: Dytype[S];
+var x1: S;
+var x2: S;
 
 ASSIGN "n", 10;
@@ -270 +270 @@
 * `FOR_ENTER dom;` **FIX ME**
 
-== Declarations and Function Definitions ==
-
-Function prototypes are considered to be declarations similar to variable declarations.
+==  Function Definitions ==
+
+The general form of a function definition:
+
+{{{
+fun[options] foo(x:Integer, ...) : Real {
+
+  // contract clauses (optional):
+  requires expr;
+  ensures expr ;
+  mpi_requires expr ;
+  mpi_ensures expr ;
+  assigns expr ;
+  reads expr ;
+  depends actions ;
+
+  // all of the following are missing for a system function...
+
+  // types defns:
+  type T=tuple[<blah, blay>];
+  type U=blah;
+
+  // variable decls:
+  var x : T;
+  var y : U;
+
+  // body:
+  ASSIGN x, 0;
+  ...
+}
+}}}
+
 
 Example of declaration of a system function defined in library Concurrency:
 {{{
-fun[lib="edu.udel.cis.vsl.civl.lib.Concurrency"] f(x: Real, b: Bool): Float[32,33];
+fun[lib="edu.udel.cis.vsl.civl.lib.Concurrency"] f(x: Real, b: Bool): Float[32,33] {}
 }}}
 
@@ -287 +316 @@
 
 System functions:
-* A function declaration which is not abstract and for which no definition is provided is a system function.
+* A function declaration which contains an option `lib=...` is a system function
+* 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 any memory it can reach.  This includes allocating new data on heaps it can reach.
-* A system function may have a guard.
+* 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 have a guard, which is another function taking the same types of inputs, but returning `Bool`.
 
 Example of a declaration of a system function with guard.
 {{{
-g(x:Real):Bool { ... }
-fun[lib="Blah",guard="g"] f(x:Real):Integer;
-}}}
-
-
-== Function Contracts ==
+fun g(x:Real):Bool { ... }
+fun[lib="Blah",guard="g"] f(x:Real):Integer {}
+}}}
+
+
+=== Function Contracts ===
+
+**THIS NEEDS TO BE UPDATED**
 
 * event set expressions:
@@ -396 +428 @@
 
 * fix notation for contracts
-* can labels, whens, chooses be optional?   See proposed statement grammar below.
 * quotes around variables in declarations?  Could be awkward but might simplify parsing.
 * quotes around function names in definitions, prototypes?  Could be awkward.
@@ -402 +433 @@
 * should we leave our parameter names in abstract and system functions?  They are not needed for anything.  THEY ARE NEEDED FOR CONTRACTS, sometimes, and maybe for documentation.    Consider making them optional.
 
-