Changes between Version 95 and Version 96 of IR

Timestamp:

11/30/15 09:15:28 (10 years ago)

Author:

siegel

Comment:

--

IR

@@ -7 +7 @@
 * a CIVL-IR program represents a guarded-transition system explicitly
 * as in CIVL-C, there are functions, scopes, and functions can be defined in any scope
-* all blocks (including a function body) consist of the following elements, in this order:
+* all blocks (including a function definition) consist of the following elements, in this order:
+ * a sequence of contract clauses (for function definitions only)
  * a sequence of type definitions
- * a sequence of variable declarations with no initializers
+ * a sequence of variable declarations (with no initializers)
  * a sequence of function definitions
- * a sequence of labeled statements.   Each clause in the labeled statement is a `when` statement with some guard and a primitive statement, followed by a `goto` statement
+ * a body, which encodes a program graph. 
 * an array is declared without any length expression.  When it is initialized it can specify length.
 * curly braces are used only to indicate scopes, as in `{ // new scope ... }`
@@ -19 +20 @@
 * unlike C, there is no "array-pointer pun".   If an array `a` needs to be converted to a pointer, you must use addr(asub(a, 0))`.
 * there are no automatic conversions.  All conversions must be by explicit casts or other functions.   Operations such as numeric addition (`add`) require that both operands have the exact same type.
+* in general, symbols can be used before they are defined, as long as they are in scope.  For example, a function `f` can call `g`, even if `g` is defined after `f` in the same scope.  There is no need for a "prototype".  Similarly, a type definition can refer to a type defined later, or can refer to itself in its own definition.
 
 == Grammar ==
@@ -26 +28 @@
 {{{
 program: block ;
-block: typedef* vardecl* fundef* statement+ ;
-statement: blockStmt | basicStmt ;
+blockitems: typedef* vardecl* fundef* statement* ;
+statement: '{' blockitems '}' | basicStmt ;
 basicStmt:  (ID ':')? (simpleStmt | chooseStmt) ;
 simpleStmt: (guardedStmt | primitiveStmt) ('goto' ID)? ;
 guardedStmt: 'when' expr 'do' primitiveStmt ;
 chooseStmt: 'begin choose' simpleStmt+ 'end choose' ;
-blockStmt: '{' block '}' ;
 typedef: 'type' ID '=' typeName ';' ;
 vardecl: 'var' varopts? ID ':' typeName ';' ;
 varopts: '[' varopt+ ']' ;
 varopt: 'input' | 'output' ;
-fundef:  'fun' funopts? ...
+fundef:  'fun' funopts? ID '(' paramlist ')' ':' typeName '{' conclause* blockitems '}' ;
+funopts: '[' funopt+ ']' ;
+conclause : 'assigns' expr ';' 
+                 | 'requires' expr ';'
+                 | 'ensures' expr ';'
+                 ...
+                 ;
 }}}