Changes between Version 80 and Version 81 of IR


Ignore:
Timestamp:
11/28/15 11:10:07 (10 years ago)
Author:
siegel
Comment:

--

Legend:

Unmodified
Added
Removed
Modified

  • IR

    v80 v81  
    11
    22The CIVL-IR language.  A program in this language is also known as a "CIVL model".
    3 
    4 Questions:
    5 * fix notation for contracts
    6 * can labels, whens, chooses be optional?   See proposed statement grammar below.
    7 * quotes around variables in declarations?  Could be awkward but might simplify parsing.
    8 * quotes around function names in definitions, prototypes?  Could be awkward.
    9 * is there ever a need for a function prototype?  Could variable decl notation be used instead? NO, variable decls are different, those are state variables.
    10 * 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.
    11 
    12 Proposed statement grammar:
    13 {{{
    14 statement: (ID ':')? (simpleStmt | chooseStmt)
    15 
    16 simpleStmt:
    17   (guardedStmt | primitiveStmt) ('goto' ID ';')?
    18 
    19 guardedStmt:
    20   'when' expr 'do' primitiveStmt
    21 
    22 chooseStmt:  'begin choose' simpleStmt+ 'end choose'
    23 }}}
    24 
    25 If goto is missing, default is the next location.
    26 If guard missing, deafult is true.
    27 
    283
    294Properties of the language:
    … …  
    4520* 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.
    4621
     22== Grammar ==
     23
     24This is not the complete grammar, but the high-level overview.
     25
     26{{{
     27program: block ;
     28block: typedef* vardecl* fundef* statement+ ;
     29statement: (ID ':')? (simpleStmt | chooseStmt | blockStmt) ;
     30simpleStmt: (guardedStmt | primitiveStmt) ('goto' ID)? ;
     31guardedStmt: 'when' expr 'do' primitiveStmt ;
     32chooseStmt: 'begin choose' simpleStmt+ 'end choose' ;
     33blockStmt: '{' block '}' ;
     34typedef: 'type' ID '=' typeName ';' ;
     35vardecl: 'var' varopts? ID ':' typeName ';' ;
     36varopts: '[' varopt+ ']' ;
     37varopt: 'input' | 'output' ;
     38fundef:  'fun' funopts? ...
     39}}}
     40
     41Notes:
     42* If goto is missing, default is the next location.
     43* If guard missing, deafult is true.
     44
    4745
    4846Example:
    4947{{{
    50 def f(u:Integer, a:Array[Real]): Integer {
     48fun f(u:Integer, a:Array[Real]): Integer {
    5149  x: Real;
    5250  y: Real;
    … …  
    5452 
    5553L1 :
     54  begin choose
    5655    when g1 do stmt1; goto L2;
    5756    when g2 do stmt2; goto L3;
     57  end choose
    5858
    5959  { // begin new scope
    6060   x: Real;
    6161L2 :
    62       when g3 do stmt3; goto L4;
     62      stmt3; goto L4;
    6363      ...
    6464  } // end new scope
    … …  
    6868}}}
    6969
    70 Example:
     70Example: the C code
    7171{{{
    7272{
    … …  
    7575}
    7676}}}
    77 translates to:
     77could be represented as
    7878{{{
    7979{
    … …  
    9494==  Types ==
    9595
    96 The types are:
     96The types (and their type names) are:
    9797
    9898* `Bool` : boolean type, values are `true` and `false`
    … …  
    400400pointer, ...
    401401Should these be called part of the language, or not?
     402
     403== Questions ==
     404
     405* fix notation for contracts
     406* can labels, whens, chooses be optional?   See proposed statement grammar below.
     407* quotes around variables in declarations?  Could be awkward but might simplify parsing.
     408* quotes around function names in definitions, prototypes?  Could be awkward.
     409* is there ever a need for a function prototype?  Could variable decl notation be used instead? NO, variable decls are different, those are state variables.
     410* 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.
     411
     412