Changes between Version 1 and Version 2 of LanguageSubset

Timestamp:

07/17/13 20:08:54 (13 years ago)

Author:

zirkel

Comment:

--

LanguageSubset

@@ -21 +21 @@
 * if-then-else statements : Same syntax as C.
 * while, for loops
+* { <blockItem>* } : A blockItem can be a variable declaration, function definition, or statement.
 * $assert <expr> : Check that <expr> holds.
 * $assume <expr> : Add <expr> to the path condition.
@@ -44 +45 @@
 The implicit guard of the $choose statement with a default clause
 is "true".
+
+== Declarations ==
+* Variable : Can optionally be specified as an input or output of the program.  Have optional initialization.
+{{{ [$input | $output] <type> v [= <expr>] }}}
+* Typedef : Assign an alternate name to a type.
+{{{ typedef <type> <name> }}}
+* Function : Gives the name, return type, and parameters.  Each function may have 0 or more declarations.
+{{{ <type> f(<type> e1, ..., <type> e_n) }}}
+* Function definition: Gives the name, return type, parameters, and body.  Each function must have exactly one definition.
+{{{ <type> f(<type> e1, ..., <type> e_n) {...} }}}
+
+== Program ==
+
+A program is a sequence of external definitions.  The external definitions are 
+
+* Variable declaration
+* Function declaration
+* Function definition
+* $assume
+
+A program must have a function called main which takes no arguments.  Execution of the program begins in the body of main.