Changes between Initial Version and Version 1 of LanguageSubset

Timestamp:

07/17/13 19:14:50 (13 years ago)

Author:

zirkel

Comment:

--

LanguageSubset

@@ +1 @@
+== Types ==
+* boolean
+* int
+* double
+* $proc : The process type.
+* $scope : The scope type.
+
+== Expressions ==
+
+* +, - , * , / , %
+* =
+* ==, <=. >=, <, >
+* ++, --
+* $true, $false
+* $self : The process invoking the expression (constant of type $proc).
+* $spawn f(e1, ..., e_n) : Spawn a process executing f on (e1, ..., e_n), return a reference to the process.
+* function calls
+
+== Statements ==
+* Expression statement : Use an expression as a statement (e.g. i++;).
+* if-then-else statements : Same syntax as C.
+* while, for loops
+* $assert <expr> : Check that <expr> holds.
+* $assume <expr> : Add <expr> to the path condition.
+* $wait <expr> : For <expr> of type $proc, block until <expr> terminates.
+* $when (<expr>) S; : Guarded statement.  Block until <expr> is true, then execute S.
+* $choose : A $choose statement has the form 
+{{{
+  $choose {
+  stmt1;
+  stmt2;
+  ...
+  default: stmt
+}
+}}}
+The "default" clause is optional.
+The guards of the statements are evaluated and among those that are
+true, one is chosen nondeterministically and executed.  If none are
+true and the default clause is present, it is chosen.  The default
+clause will only be selected if all guards are false.  If no default
+clause is present and all guards are false, the statement blocks.
+Hence the implicit guard of the $choose statement without a default
+clause is the disjunction of the guards of its sub-statements.
+The implicit guard of the $choose statement with a default clause
+is "true".