Changes between Version 19 and Version 20 of Fundamentals

Timestamp:

05/14/23 19:54:03 (3 years ago)

Author:

siegel

Comment:

--

Fundamentals

@@ -150 +150 @@
 A universally quantified formula has the form
 
-  `$forall` `(` ''variable-declarations'' (`;` ''variable-declarations'' )* `|` ''restriction'' `)` ''expr''
+  `$forall` `(` ''variable-declarations'' (`;` ''variable-declarations'' )* (`|` ''restriction'')? `)` ''expr''
 
 where ''variable-declarations'' declares a list of variables of a given type with an optional domain, and has the form
@@ -157 +157 @@
 
 where ''type'' is a type name (e.g., `int` or `double`), ''identifier'' is the name of the bound variable. Moreover, ''restriction'' is a boolean expression which expresses some restriction on the values that the bound variable can take, and ''expr'' is a formula. The universally quantified formula holds iff for all values assignable to the bound variable for which the restriction holds, the formula expr holds.
+
+Examples:
+{{{
+$forall (int i | 0 <= i && i < n) a[i]==0
+$forall (int i: 0..n-1) a[i]==0
+$forall (int i,j | 0<=i && i<n && 0<=j && j<m) b[i][j]==0
+$forall (int i: 0..n-1; int j: 0..m-1) b[i][j]==0
+$forall (int i,j: ($domain){0..n-1, 0..m-1}) b[i][j]==0
+}}}
+
+[Note: the last form is not yet implemented]