Changes between Version 20 and Version 21 of Fundamentals

Timestamp:

05/14/23 21:59:32 (3 years ago)

Author:

siegel

Comment:

--

Fundamentals

@@ -150 +150 @@
 A universally quantified formula has the form
 
-  `$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
-
-  ''type'' ''identifier'' (, ''identifier'')* (`:` ''domain'')?
+  `$forall` `(` ''variable-decls'' (`;` ''variable-decls'' )* (`|` ''restriction'')? `)` ''expr''
+
+where ''variable-decls'' has one of the forms
+
+  ''type'' ''identifier'' (, ''identifier'')*
+
+  ''type'' ''identifier'' `:` ''range''
 
 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.
 
+The syntax for existential quantification is the same, with `$exists` in place of `$forall`.  
+
 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]
-
+int a[3], b[3][2];
+int main() {
+  int n=3, m=2;
+  $assert($forall (int i | 0 <= i && i < n) a[i]==0);
+  $assert($forall (int i: 0..n-1) a[i]==0);
+  $assert($forall (int i: 0..n-1 | i%2==0) a[i]==0);
+  $assert($forall (int i: 0..n-1; int j: 0..m-1) b[i][j]==0);
+  $assert($forall (int i: 0..n-1; int j | 0<=j && j<m) b[i][j]==0);
+  $assert($forall (int i: 0..n-1; int j: 0..m-1 | i<j ) b[i][j]==0);
+  $assert($forall (int i,j | 0<=i && i<n && 0<=j && j<m) b[i][j]==0);
+  $assert($exists (int i | 0<=i && i<n) a[i]==0);
+}
+}}}
 
 * domain literals: An expression of the form `($domain) { r1, ..., rn }` where `r1`, . . . , `rn` are n expressions of type `$range`, is a ''Cartesian domain expression''. It represents the domain of dimension n which is the Cartesian product of the n ranges, i.e., it consists of all n-tuples (x1,...,xn) where x1 ∈ r1, ..., xn ∈ rn. The order on the domain is the dictionary order on tuples. The type of this expression is `$domain(n)`.  When a Cartesian domain expression is used to initialize an object of domain type, the `($domain)` may be omitted. For example: `$domain(3) dom = { 0 .. 3, r2, 10 .. 2 # -2 };`