Changes between Version 35 and Version 36 of Language

Timestamp:

05/21/23 09:57:38 (3 years ago)

Author:

siegel

Comment:

--

Language

@@ -258 +258 @@
 === Scope relational expressions #scope-expressions
 
-Let `s1` and `s2` be expressions of [#scope-type 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` is equivalent to `s2 < s1`.
-* `s1 >= s2` is equivalent to `s2 <= s1`.
-
-Each of these expressions is erroneous if `s1` or `s2` is undefined.
+Let ''s,,1,,'' and ''s,,2,,'' be expressions of [#scope-type type $scope]. The following are all CIVL-C expressions of boolean type:
+
+* ''s,,1,,''`==`''s,,2,,'' holds iff ''s,,1,,'' and ''s,,2,,'' refer to the same dynamic scope.
+* ''s,,1,,''`!=`''s,,2,,'' holds iff ''s,,1,,'' and ''s,,2,,'' refer to different dynamic scopes.
+* ''s,,1,,''`<=`''s,,2,,'' holds iff ''s,,1,,'' is equal to or a descendant of ''s,,2,,'', i.e., ''s,,1,,'' is equal to or contained in ''s,,2,,''.
+* ''s,,1,,''`<`''s,,2,,'' holds iff ''s,,1,,'' is a strict descendant of ''s,,2,,'', i.e., ''s,,1,,'' is contained in ''s,,2,,'' and is not equal to ''s,,2,,''.
+* ''s,,1,,''`>`''s,,2,,'' is equivalent to ''s,,2,,''`<`''s,,1,,''.
+* ''s,,1,,''`>=`''s,,2,,'' is equivalent to ''s,,2,,''`<=`''s,,1,,''.
+
+Each of these expressions is erroneous if ''s,,1,,'' or ''s,,2,,'' is undefined.
 This error is reported by the model checker.