Changes between Version 24 and Version 25 of Fundamentals

Timestamp:

05/15/23 23:09:54 (3 years ago)

Author:

siegel

Comment:

--

Fundamentals

@@ -203 +203 @@
 
 
-* `$here`
-* `$root`
-* `$pow(double, double)` 
-* range literals: An expression of the form `lo .. hi` where `lo` and `hi` are integer expressions, represents the range consisting of the integers `lo`, `lo` + 1, ..., `hi` (in that order).  An expression of the form `lo .. hi # step`, where `lo`, `hi`, and `step` are integer expressions is interpreted as follows. If `step` is positive, it represents the range consisting of `lo`, `lo` + `step`, `lo` + 2 ∗ `step`, …, up to and possibly including `hi`. To be precise, the infinite sequence is intersected with the set of integers less than or equal to `hi`.  If `step` is negative, the expression represents the range consisting of `hi`, `hi` + `step`, `hi` + 2 ∗ `step`, . . ., down to and possibly including `lo`. Precisely, the infinite sequence is intersected with the set of integers greater than or equal to `lo`.
-* `$scopeof`
-* scope relational expressions:
+=== `$here`
+Expression of type `$scope`, evaluating to the dynamic scope in which the evaluation takes place.
+
+=== `$root`
+Constant of type `$scope`, the root dynamic scope.
+
+=== Range literals
+
+An expression of the form `lo .. hi` where `lo` and `hi` are integer expressions, represents the range consisting of the integers `lo`, `lo` + 1, ..., `hi` (in that order).
+An expression of the form `lo .. hi # step`, where `lo`, `hi`, and `step` are integer expressions is interpreted as follows.
+If `step` is positive, it represents the range consisting of `lo`, `lo` + `step`, `lo` + 2 ∗ `step`, …, up to and possibly including `hi`.
+To be precise, the infinite sequence is intersected with the set of integers less than or equal to `hi`.
+If `step` is negative, the expression represents the range consisting of `hi`, `hi` + `step`, `hi` + 2 ∗ `step`, . . ., down to and possibly including `lo`.
+Precisely, the infinite sequence is intersected with the set of integers greater than or equal to `lo`.
+
+=== `$scopeof`
+
+Given any left-hand-side expression ''expr'', the expression `$scopeof(`''expr''`)` evaluates to the dynamic scope containing the object specified by ''expr''.
+The following example illustrates the semantics of the `$scopeof` operator. All of the assertions hold:
+{{{
+{
+  $scope s1 = $here;
+  int x;
+  double a[10];
+  {
+    $scope s2 = $here;
+    int *p = &x;
+    double *q = &a[4];
+    assert($scopeof(x)==s1);
+    assert($scopeof(p)==s2);
+    assert($scopeof(*p)==s1);
+    assert($scopeof(a)==s1);
+    assert($scopeof(a[5])==s1);
+    assert($scopeof(q)==s2);
+    assert($scopeof(*q)==s1);
+  }
+}
+}}}
+
+=== Scope relational expressions
+
+Let `s1` and `s2` be expressions of type `$scope`. The following are all CIVL-C expressions of boolean type:
+
+* `s1 == s2`. Holds iff `s1` and `s2` refer to the same dynamic scope.
+* `s1 != s2`. Holds iff `s1` and `s2` refer to different dynamic scopes.
+* `s1 <= s2`. Holds iff `s1` is equal to or a descendant of `s2`, i.e., `s1` is equal to or contained in `s2`.
+* `s1 < s2`. Holds iff `s1` is a strict descendant of `s2`, i.e., `s1` is contained in `s2` and is not equal to `s2`.
+* `s1 > s2`. Equivalent to `s2 < s1`.
+* `s1 >= s2`. Equivalent to `s2 <= s1`.
+
+Each of these expressions is erroneous if `s1` or `s2` is undefined.  This error is reported by the model checker.
 
 
@@ -241 +286 @@
 * `$yield()`
 
+== Functions and macros
+
+=== `$pow(double, double)` 
 
 == Contract Annotations