Changes between Version 50 and Version 51 of Language


Ignore:
Timestamp:
05/23/23 09:35:32 (3 years ago)
Author:
Alex Wilton
Comment:

Some formatting and typo fixes. Also reworked the section on quantified expressions a little bit.

Legend:

Unmodified
Added
Removed
Modified

  • Language

    v50 v51  
    3333
    3434An object of this type is a reference to a dynamic scope.
    35 Several constants, expressions, and functions dealing with the $scope type are also provided.
     35Several constants, expressions, and functions dealing with the `$scope` type are also provided.
    3636The `$scope` type is like any other object type.
    3737It may be used as the element type of an array, a field in a structure or union, and so on.
    … …  
    9999$abstract int f(int x);
    100100}}}
    101 An abstract function must have a non-void return type and take at least one parameter.
     101An abstract function must have a non-`void` return type and take at least one parameter.
    102102An invocation of an abstract function is an expression and can be used anywhere an expression is allowed.
    103103The interpretation is an "uninterpreted function".
    … …  
    129129
    130130A system function may have a guard, which is specified in the function contract using a `$executes_when` clause.
    131 Unless constrained by its contract or other qualifiers, a system function may modify the stay in an arbitrary way.
     131Unless constrained by its contract or other qualifiers, a system function may modify the state in an arbitrary way.
    132132
    133133=== Pure functions: `$pure` #pure
    … …  
    150150=== Boolean expressions, `=>`, `$forall`, `$exists` #boolean-expressions
    151151
    152 CIVL-C provides the boolean constants`$true` and `$false`, which are simply defined as 1 and 0, respectively.
     152CIVL-C provides the boolean constants `$true` and `$false`, which are simply defined as 1 and 0, respectively.
    153153CIVL-C is, after all, an extension of C.
    154154A program may also include the standard C library header file `stdbool.h`, which defines `true` and `false` in the exact same way.
    … …  
    161161  `$forall` `(` ''variable-decls'' (`;` ''variable-decls'' )* (`|` ''restriction'')? `)` ''expr''
    162162
    163 where ''variable-decls'' has one of the forms
    164 
    165   ''type'' ''identifier'' (`,` ''identifier'')*
    166 
    167   ''type'' ''identifier'' `:` ''range''
    168 
    169 where ''type'' is a type name (e.g., `int` or `double`), ''identifier'' is the name of the bound variable,
    170 ''restriction'' is a formula (boolean expression) which expresses some restriction on the values that the bound variable can take,
    171 ''range'' is an expression of `$range` type, and ''expr'' is a formula.
    172 The universally quantified formula holds iff for all values assignable to the bound variable for which the restriction holds, the formula expr holds.
    173 
    174 The syntax for existential quantification is the same, with `$exists` in place of `$forall`. 
     163where
     164* ''variable-decls'' has one of the forms
     165  * ''type'' ''identifier'' (`,` ''identifier'')*
     166  * `int` ''identifier'' `:` ''range''
     167* ''type'' is a type name (e.g., `int` or `double`),
     168* ''identifier'' is the name of a bound variable,
     169* ''range'' is an expression of `$range` type,
     170* ''restriction'' is a formula (boolean expression) which expresses some restriction on the values that the bound variable can take, and
     171* ''expr'' is a formula.
     172The syntax for existential quantification is the same, with `$exists` in place of `$forall`.
     173
     174We will call any assignment of values to the bound variables of a quantified expression a "candidate assignment" if it satisfies ''restriction'' and each bound variable with an associated ''range'' is given a value contained in this ''range''. The universally quantified formula holds iff ''expr'' holds under all candidate assignments. Similarly, the existentially quantified formula holds iff there exists a candidate assignment for which ''expr'' holds.
    175175
    176176Examples:
    … …  
    222222=== Range literals: ''a''`..`''b'' and ''a''`..`''b''`#`''c'' #range-literals
    223223
    224 A range literal has form
     224A range literal has the form
    225225  ''expr'' `..` ''expr'' ( `#` ''expr'' )?
    226226The two or three sub-expressions (the third is optional) have integer type and the type of the entire expression is `$range`.
    … …  
    361361The default clause is optional.
    362362
    363 The guards of the statements are evaluated and among those that are true, one is chosen nondeterministically and executed.
     363The guards of the statements are evaluated and among those that are true, one is chosen non-deterministically and executed.
    364364If none are true and the default clause is present, it is chosen.
    365365The default clause will only be selected if all guards are false.
    … …  
    397397Control iterates over the values of the domain, assigning the integer variables the components of the current tuple in the domain at the start of each iteration.
    398398The scope of the variables extends to the end of ''S''.
    399 The iterations takes place in the order specified by the domain, e.g., dictionary order for a Caretesian domain.
     399The iterations takes place in the order specified by the domain, e.g., dictionary order for a Cartesian domain.
    400400Note that if a range expression can be used as ''dom'' here, it will be automatically converted to a one-dimensional domain.
    401401For example,