Changes between Version 16 and Version 17 of PIL

Timestamp:

10/06/24 09:30:04 (19 months ago)

Author:

siegel

Comment:

--

PIL

@@ -35 +35 @@
  * `$int[]* q`: pointer to array of integer
  * `$int*[]($real) f`: function from Real to array of pointer to integer
+- every type has a default value.  The result of evaluating an erroneous expression is the default value of that type.
 - basic types: 
- * `$bool` : the set consisting of `$true` and `$false`
- * `$int`: the set of integers
- * `$real`: the set of Reals
- * `$int<lo,hi>`: set of integers between `lo` and `hi`, inclusive. `lo` and `hi` are constant expressions so are known at compile time.
- * `$uint<hi>`: nonnegative integers less than the constant expression `hi`.  Arithmetic is performed modulo `hi` (like C's unsigned integer types). 
- * `$float<p,emax>`: the set of IEEE binary floating point numbers with precision `p` and emax `emax`.  These are also constant expressions.
-- `T*`: pointer to `T`
-- `struct TAG { T1 f1; ... Tn fn; }`: a C struct
-- `union`: similar
-- `T[]`: sequence of `T`.  Note: there is no "T[n]".  Sequences are first-class values: they can be assigned, returned, passed as arguments, etc.  
-- `R(T1, ..., Tn)`: the type of a procedure which consumes values in `T1`, ..., `Tn` and returns a value in `R`.   This is basically C's function type.
-- `$fun<T1,T2>` :  "logic functions":  deterministic, total, side-effect free functions from `T1` to `T2`.  Note however the function may depend on the state (i.e., the state should be considered a hidden input).   A `$pure` function is a function that does not depend on the state.
-- `$set<T>` : finite set of `T`
-- `$map<T1,T2>` : finite map from `T1` to `T2`.  A map is a set of ordered pairs `(x,y)` with the property that if `(x,y)` and `(x,z)` are in the map, then `y`=`z`.
-- `$tuple<T1,...>` : tuples of specified type.  This is similar to `struct`, but there is no tag and the fields do not have names.
+ * `$bool` : the set consisting of `$true` and `$false`.  Default value: `$false`.
+ * `$int`: the set of integers.  Default value: 0.
+ * `$real`: the set of Reals.  Default value: 0.0.
+ * `$int<max>`: set of integers [-max, max-1]. `max` is a constant positive integer expression so is statically known.  Default value: 0.
+ * `$uint<hi>`: nonnegative integers less than the constant expression `hi`.  Arithmetic is performed modulo `hi` (like C's unsigned integer types).   Default value: 0.
+ * `$float<p,emax>`: the set of IEEE binary floating point numbers with precision `p` and emax `emax`.  These are also constant expressions.  Default value: 0.0.
+- `T*`: pointer to `T`.  Default value: `NULL`.
+- `struct TAG { T1 f1; ... Tn fn; }`: a C struct.  Default value: the struct value in which each field has its default value.
+- `union`: a C union.   Default value: the union value in which the first field has its default value.
+- `T[]`: sequence of `T`.  Note: there is no "T[n]".  Sequences are first-class values: they can be assigned, returned, passed as arguments, etc.  Default value: the sequence of length 0.
+- `R(T1, ..., Tn)`: the type of a procedure which consumes values in `T1`, ..., `Tn` and returns a value in `R`.   This is basically C's function type.  Default value: the procedure which does nothing (has no side-effects) and returns the default value of `R` for any inputs.
+- `$fun<T1,T2>` :  "logic functions":  deterministic, total, side-effect free functions from `T1` to `T2`.  Note however the function may depend on the state (i.e., the state should be considered a hidden input).   A `$pure` function is a function that does not depend on the state.  Default value: the function that returns the default value of `T2` on any input.
+- `$set<T>` : finite set of `T`.  Default value: the empty set.
+- `$map<T1,T2>` : finite map from `T1` to `T2`.  A map is a set of ordered pairs `(x,y)` with the property that if `(x,y)` and `(x,z)` are in the map, then `y`=`z`.  Default value: the empty map.
+- `$tuple<T1,...>` : tuples of specified type.  This is similar to `struct`, but there is no tag and the fields do not have names.  Default value: the tuple in which each component has its default value.
 - Type definitions have the form: `typedef typename ID;`
 
@@ -158 +159 @@
  * 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`
+ * the value of component `i` (an integer constant) of tuple `t`.  Syntax error if `i` is out of range for the tuple type.
 - `($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`
+ * the tuple which is the same as `t`, except for component `i` (an integer constant), which has value `expr1`.  Syntax error if `i` is out of range.
 
 Mutating expressions:
-- `t.(i) = expr` : sets component `i` of tuple `t` to `expr`
+- `t.(i) = expr` : sets component `i` of tuple `t` to `expr`.  Here `i` is an integer constant; it is a syntax error if `i` is out of range.
 
 == Sets
@@ -199 +200 @@
 Mutating procedures:
 - `$bool $set_add($set<T> * this, T x);`
+ * adds `x` to `this`.  Returns `$true` iff `x` was not in `this`, i.e., if the operation results in a change to the set.
 - `$bool $set_remove($set<T> * this, T x);`
+ * removes `x` from `this`.  Returns `$true` iff `x` was in `this`, i.e., if the operation results in a change to the set.
 - `void $set_addAll($set<T> * this, $set<T> that);`
+ * adds all of the elements of `that` to `this`
 - `void $set_removeAll($set<T> * this, $set<T> that);`
+ * removes all of the elements of `that` from `this`
 - `void $set_keepOnly($set<T> * this, $set<T> that);`
+ * removes any elements of `this` which is not in `that` from `this`
 
 ==  Sequences (arrays)
@@ -210 +216 @@
  * the two sequences have the same type and length and corresponding elements are equal
 - `a[i]`
- * the `i`-th element of `a`. Here `a` is an expression of type `T[]` and `i` is an expression of type `$int`.
+ * the `i`-th element of `a`. Here `a` is an expression of type `T[]` and `i` is an expression of type `$int`.  Requires `i` to be in range, i.e., `i` is in [0,n-1], where n is the length of `a`.   (Otherwise the expression is erroneous.)
 - `a[i:=x]`
- * the sequence which is the same as `a`, except in position `i`, where it has value `x`.  Here `a` is an expression of type `T[]`, `i` is an expression of type `$int`, and `x` is an expression of type `T`
+ * the sequence which is the same as `a`, except in position `i`, where it has value `x`.  Here `a` is an expression of type `T[]`, `i` is an expression of type `$int`, and `x` is an expression of type `T`.  Requires `i` to be in range for `a`.
 - `(T[]){ expr1, ... }`
  * the sequence obtained by evaluating the given expressions, each of which has type `T`
@@ -224 +230 @@
  * the length of `a`
 - `$pure $logic T[] $seq_subseq(T[] a, int i, int n);`
- * the sequence of length n,  a[i..i+n-1]
+ * the sequence of length n,  a[i..i+n-1].  Requires that i..i+n-1 are all in range for `a`
 - $pure $logic T[] $seq_with(T[] a, int i, T x);`
- * the sequence obtained from `a` by inserting `x` at position `i` and shifting the subsequent elements up
-- `$pure $logic T[] $seq_without(T[] a, int i);`
+ * the sequence obtained from `a` by inserting `x` at position `i` and shifting the subsequent elements up.  Requires `i` to be in [0,n], where `n` is the length of `a`.
+- `$pure $logic T[] $seq_without(T[] a, int i);`.  Requires `i` to be in [0,n-1], where `n` is the length of `a`.
  * the sequence obtained from `a` by deleting the element in position `i` and shifting subsequent elements down
 - `$pure $logic T[] $seq_concat(T[] a1, T[] a2);`