Changes between Version 13 and Version 14 of PIL

Timestamp:

10/05/24 16:53:06 (19 months ago)

Author:

siegel

Comment:

--

PIL

@@ -155 +155 @@
 
 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`
+- `t1 == t2`
+ * the two tuples have the same type 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] = expr` : sets component `i` of tuple `t` to `expr`
+- `t.(i) = expr` : sets component `i` of tuple `t` to `expr`
 
 == Sets
@@ -167 +171 @@
 Side-effect free expressions:
 - `s1 == s2`
-- `($set<T>)$empty`   // empty set of type T
+ * the two sets have the same type and contain the same elements
+- `($set<T>)$empty`
+ * empty set of type T
 
 Logic functions:
 - `$pure $logic $bool $set_contains($set<T> s, T x);`
- * is `x` an element of `s`?
+ * is x an element of s?
 - `$pure $logic $set<T> $set_with($set<T> s, T x);`
- * `s` U {`x`}
+ * s U {x}
 - `$pure $logic $set<T> $set_without($set<T> s, T x);`
- * `s` - {`x`}
+ * s - {x}
 - `$pure $logic $set<T> $set_union($set<T> s1, $set<T> s2);`
- * `s1` U `s2` 
+ * s1 U s2 
 - `$pure $logic $set<T> $set_difference($set<T> s1, $set<T> s2);`
- * `s1`-`s2` 
+ * s1-s2 
 - `$pure $logic $set_intersection($set<T> s1, $set<T> s2);`
- * `s1`  \cap `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`?
+ * returns the set of elements of s as an array in some deterministic order
+- `$pure $logic $bool $set_subset($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);`
- * { `f`(`x`) | `x` in `s`}
+ * { f(x) | x in s}
 - `$pure logic $set<T> $set_comprehension($set<T>, $fun<T,$bool> p);`
- * { `x` in `s` | `p`(`x`) }
+ * { x in s | p(x) }
 
 Mutating procedures:
@@ -202 +208 @@
 Expressions:
 - `a1 == a2`
+ * the two arrays have the same type and length and corresponding elements are equal
 - `a[i]`
+ * the `i`-th element of `a`
+- `a[i:=x]`
+ * the sequence which is the same as `a`, exception in position `i`, where it has value `x`
 - `(T[]){ expr1, ... }`
 
@@ -209 +219 @@
 - `$pure $logic T[] $seq_uniform($int n, T val);`
 - `$pure $logic $int $length(T[] a);` // length of a
-- `$pure $logic T[] $seq_write(T[] a, int i, T x);`  // a[i:=x]
 - `$pure $logic T[] $seq_subseq(T[] a, int i, int n);`  // a[i..i+n-1]
 - `$pure $logic T[] $seq_without(T[] a, int i);` // a with position i removed
@@ -229 +238 @@
 ==  Maps
 
-Non-mutating expressions:
+Side-effect-free expressions:
 - `m1 == m2`
 - `($map<K,V>)$empty`
-- `$logic V $map_get($map<K,V> K key);`
-- `$logic $bool $map_containsKey($map<K,V> map, K key);`
-- `$logic $bool $map_containsValue($map<K,V> map, V val);`
-- `$logic $map<K,V> $map_with($map<K,V> map, K key, V val);`
-- `$logic $map<K,V> $map_without($map<K,V> map, K key);`
-- `$logic $set<K> $map_keys($map<K,V> map);`
-- `$logic $set<$tuple<K,V>> $map_entries($map<K,V> map);`
+
+Logic functions:
+- `$pure $logic V $map_get($map<K,V> K key);`
+- `$pure $logic $bool $map_containsKey($map<K,V> map, K key);`
+- `$pure $logic $bool $map_containsValue($map<K,V> map, V val);`
+- `$pure $logic $map<K,V> $map_with($map<K,V> map, K key, V val);`
+- `$pure $logic $map<K,V> $map_without($map<K,V> map, K key);`
+- `$pure $logic $set<K> $map_keys($map<K,V> map);`
+- `$pure $logic $set<$tuple<K,V>> $map_entries($map<K,V> map);`
 
 Mutating procedures:
@@ -246 +257 @@
 - `void $map_addAll($map<K,V> * this, $map<K,V> that);`
 
-
 == Heaps
 
 There is a single heap for dynamic allocation.  The following built-in procedures are provided:
 
-- `T* $new<T>()`: creates an object `A` of type `T` in heap and returns `&A`.
-- `T* $alloc<T>(int n)`: creates an array `A` of length `n` of `T` in heap and returns `&A[0]`.
-- `void $free<T>(T* p)`: frees the object referred to by `p`, the pointer returned by an earlier call to `$new` or `$alloc`.
+- `T* $new<T>()`
+ * creates an object `A` of type `T` in heap and returns `&A`.
+- `T* $alloc<T>(int n)`
+ * creates an array `A` of length `n` of `T` in heap and returns `&A[0]`.
+- `void $free<T>(T* p)`
+ * frees the object referred to by `p`, the pointer returned by an earlier call to `$new` or `$alloc`.
 
 
@@ -261 +274 @@
 * can there be nondeterministic expressions, i.e., expressions that evaluate to a set of values instead of one value?
 * how to implement C's malloc?
+* what to return when something is wrong, e.g., $map_get$ when the specified key is not in the map (default value of type?)
 
 Ideas on malloc: