Changes between Version 23 and Version 24 of Fundamentals


Ignore:
Timestamp:
05/15/23 08:01:20 (3 years ago)
Author:
siegel
Comment:

--

Legend:

Unmodified
Added
Removed
Modified

  • Fundamentals

    v23 v24  
    144144=== Boolean expressions
    145145
    146 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.
    147 
    148 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).
     146CIVL-C provides the boolean constants`$true` and `$false`, which are simply defined as 1 and 0, respectively.
     147CIVL-C is, after all, an extension of C.
     148A program may also include the standard C library header file `stdbool.h`, which defines `true` and `false` in the exact same way.
     149
     150In addition to the standard logical operators `&&`, `||`, and `!`, CIVL-C provides `=>` (implies).
     151`p => q` is equivalent to `!(p) || q` (and has the same short-circuit semantics).
    149152
    150153A universally quantified formula has the form
    … …  
    154157where ''variable-decls'' has one of the forms
    155158
    156   ''type'' ''identifier'' (, ''identifier'')*
     159  ''type'' ''identifier'' (`,` ''identifier'')*
    157160
    158161  ''type'' ''identifier'' `:` ''range''
    159162
    160 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.
     163where ''type'' is a type name (e.g., `int` or `double`), ''identifier'' is the name of the bound variable,
     164''restriction'' is a formula (boolean expression) which expresses some restriction on the values that the bound variable can take,
     165''range'' is an expression of `$range` type, and ''expr'' is a formula.
     166The universally quantified formula holds iff for all values assignable to the bound variable for which the restriction holds, the formula expr holds.
    161167
    162168The syntax for existential quantification is the same, with `$exists` in place of `$forall`.