Changes between Version 11 and Version 12 of PIL

Timestamp:

10/05/24 15:15:08 (21 months ago)

Author:

siegel

Comment:

--

PIL

@@ -153 +153 @@
 == Tuples
 
-Non-mutating expressions:
-- `t1 == t2`
-- `t.i`
-- `($tuple<T1,...>){ x1, ... }`
-- `$pure $logic $tuple<T1,...> $tuple_write($tuple<T1,...> t, $int i, Ti x);`
+Expressions: these are all side-effect-free, assuming `expr1`, ... are side-effect-free.
+- `t1 == t2` : the two tuples have the same number of components and corresponding components are equal
+- `t.i` : the value of component `i` (a constant integer) of tuple `t`
+- `($tuple<T1,...>){ expr1, ... }` : the literal tuple with the given list of components.
+- `t[i : expr1]` : the tuple which is the same as `t`, except for component `i` (a constant integer), which has value `expr1`
 
 Mutating expressions:
-- `t.i = x`
+- `t[i] = expr` : sets component `i` of tuple `t` to `expr`
 
 == Sets
 
-Non-mutating expressions:
+Side-effect free expressions:
 - `s1 == s2`
 - `($set<T>)$empty`   // empty set of type T
-- `$pure $logic _Bool $set_in(T x, $set<T> s);`  // is x an element of s?
-- `$pure $logic $set<T> $set_with($set<T> s, T x);` // s U {x}
-- `$pure $logic $set<T> $set_without($set<T> s, T x);` // s - {x}
-- `$pure $logic $set<T> $set_union($set<T> s1, $set<T> s2);` // s1 U s2 
-- `$pure $logic $set<T> $set_difference($set<T> s1, $set<T> s2);` // s1-s2 
-- `$pure $logic $set_intersection($set<T> s1, $set<T> s2);` // s1 \cap s2
-- `$pure $logic T[] $set_elements($set<T> s);`
-- `$pure $logic _Bool $set_isSubsetOf($set<T> s1, $set<T> s2);`
-- `$pure $logic $set<U> $set_map($set<T> s, $fun<T,U> f);`
+
+Logic functions:
+- `$pure $logic _Bool $set_contains($set<T> s, T x);` :  // is x an element of s?
+- `$pure $logic $set<T> $set_with($set<T> s, T x);` : // s U {x}
+- `$pure $logic $set<T> $set_without($set<T> s, T x);` : // s - {x}
+- `$pure $logic $set<T> $set_union($set<T> s1, $set<T> s2);` : // s1 U s2 
+- `$pure $logic $set<T> $set_difference($set<T> s1, $set<T> s2);` : // s1-s2 
+- `$pure $logic $set_intersection($set<T> s1, $set<T> s2);` : // s1 \cap s2
+- `$pure $logic T[] $set_elements($set<T> s);` : // returns the set of elements of `s` as an array in some deterministic order
+- `$pure $logic _Bool $set_isSubsetOf($set<T> s1, $set<T> s2);` : is `s1` a subset of `s2`?
+- `$pure $logic $set<U> $set_map($set<T> s, $fun<T,U> f);` : the set { f(x) | x in s}
+- `$pure logic $set<T> $set_comprehension($set<T>, $fun<T,_Bool> p);` : the set { x in s | p(x) }
 
 Mutating procedures: