Changes between Version 18 and Version 19 of Fundamentals

Timestamp:

05/14/23 19:27:25 (3 years ago)

Author:

siegel

Comment:

--

Fundamentals

@@ -142 +142 @@
 == Expressions
 
-* `=>` 
+=== Boolean expressions
+
+CIVL-C provides the boolean constants`$true` and `$false`, which are simply defined as 1 and 0, respectively.   CIVL-C is, after all, an extension of C.   A program may also include the standard C library header file `stdbool.h`, which defines `true` and `false` in the exact same way.
+
+In addition to the standard logical operators `&&`, `||`, and `!`, CIVL-C provides `=>` (implies).  `p => q` is equivalent to `!(p) || q` (and has the same short-circuit semantics).
+
+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'')?
+
+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.
+
+
 * 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 };`
 * `$true`