| 149 | | * Logical |
| 150 | | * `\true`, `\false` : literal values of type `Bool` |
| 151 | | * `\not(e)` : logical not |
| 152 | | * `\and(e1, e2)`, `\or(e1, e2)`: logical and/or operation |
| 153 | | * `\eq(e1, e2)`, `\neq(e1, e2)`: equality/inequality test |
| 154 | | * `\forall <i1:T1, i2:T2, ...>, e1, e2` : universal quantification. For all i1 in type T1, i2 in type T2, ...: if e1 holds, then e2 holds. The only reason for having two expressions e1 and e2 is possible side-effects (exceptions) in e2 if e1 does not hold. For example, e1 can be x!=0, and e2 can safely divide by 0. |
| 155 | | * `\exists <i1:T1, i2:T2, ...>, e1, e2`: existential quantification. There is some i1 in type T1, i2 in type T2, ..., such that e1 holds and e2 holds. |
| 156 | | * Numeric |
| 157 | | * 123, -123, 3.1415, etc. : values of type `Integer`, `Int`, `Real`, `Float`. **NEED TO BE MORE SPECIFIC** |
| 158 | | * `\add(e1, e2)` : numeric addition. |
| 159 | | * `e1` and `e2` have the same numeric type. Note that there are no "automatic conversions" as there are in C. If the original expressions have different types, explicit casts must be inserted. |
| 160 | | * `\sub(e1, e2)` : subtraction |
| 161 | | * `\mul(e1, e2)` : multiplication |
| 162 | | * `\div(e1, e2)` : division |
| 163 | | * If both are integer types, the result is integer division. Otherwise it is real division. Need to define what happens for negative integers. |
| 164 | | * `\mod(e1, e2)` : integer modulus |
| 165 | | * `\neg(e)` : negative |
| 166 | | * `\lt(e1, e2)`, `\lte(e1, e2)`: less than/less than or equal to |
| 167 | | * Characters and Strings |
| 168 | | * 'a', 'b', ... : Char values. **UNICODE?** |
| 169 | | * `"abc"` : string literals: value of type `Array[Char, n+1]`, where n is the length of the string (the last element is the character `\0`) |
| 170 | | * Ranges and Domains |
| 171 | | * `\range(e1,e2,e3)` : value of type `Range` consisting of the integers e1, e1+e3, e1+2*e3, ... that are less than or equal to e2. |
| 172 | | * `\domain(<r1,...,rn>)` : value of type `Domain[n]`, the ordered Cartesian product of the n ranges (dictionary order) |
| 173 | | * `\hasnext(dom, <i, j, …>)`: an expression of boolean type, testing if the domain `dom` contains any element after `<i, j, ...>` |
| 174 | | * Arrays |
| 175 | | * `\array(T, <e0, ..., en-1>)`: value of type `Array[T, n]`, a literal array |
| 176 | | * `\array(T, n, e)`: value of type `Array[T,n]` in which each of the n elements is `e` |
| 177 | | * `\asub(e1, e2)` : array subscript expression. Note that `e1` must have array type, not pointer type. (This is different from C.) If `e1` has pointer type, use `\deref(\padd(e1, e2))` instead. |
| 178 | | * `\seq_add(a,e)` : array obtained by adding element e to the end of the array. Original array a is not modified. |
| 179 | | * `\seq_append(a1,a2)` : array obtained by concatenating two arrays. Original array not modified. |
| 180 | | * `\seq_remove(a,i)` : array obtained by removing element at position i from a. Original array a not modified. **WHAT HAPPENS TO REFERENCES INTO A** |
| 181 | | * `\bit_and(e1, e2)`, `\bit_or(e1, e2)`, `\bit_xor(e1, e2)`, `\bit_comp(e1)` : bit-wise operations: arguments are arrays of booleans of equal length. |
| 182 | | * Tuples |
| 183 | | * `\tuple(S, <e0, e1, ...>)` : value of tuple type `S` (tuple literal) |
| 184 | | * `\tsel(e1, i)` : tuple selection of component i of e1. i must be a literal natural number. |
| 185 | | * Pointers and Memory |
| 186 | | * `NULL` : value of type `void*` |
| 187 | | * `\deref(e)` : pointer dereference |
| 188 | | * `\addr(e)` : address-of operator |
| 189 | | * `\padd(e1, e2)`: pointer addition. `e1` has pointer type and `e2` has an integer type or range type. If `e2` has integer type the result has pointer type. Otherwise, the result has `Mem` type. |
| 190 | | * `\psub(e1,e2)`: pointer subtraction |
| 191 | | * `\mem_reach(ptr)`, where `ptr` is an expression with a pointer type. This represents the set of all memory units reachable from `ptr`, including the memory unit pointed to by `ptr` itself. |
| 192 | | * `\mem_union(mem1, mem2)`, where `mem1` and `mem2` are expressions of type `Memory`. This is the union of the two memory sets. |
| 193 | | * `\mem_isect(mem1, mem1)` : set intersection |
| 194 | | * `\mem_comp(mem1)` : set complement (everything not in `mem1`) |
| 195 | | * `\mem_slice(a, dom)`, where `a` is an expression of array type and `dom` is an expression of `Domain` type. The dimension of the array must match the dimension of the domain. This represents all memory units which are the cells in the array indexed by a tuple in `dom`. |
| 196 | | * Scopes and Processes |
| 197 | | * `\root`, `\here` : values of type `Scope` |
| 198 | | * `\self`, `\proc_null` : values of type `Proc` |
| 199 | | * Other |
| 200 | | * variables |
| 201 | | * `\sizeof_type(t)` : the size of the dynamic type t; `Integer` type |
| 202 | | * `\sizeof_expr(e)` : the size of the value of expression `e`; `Integer` type |
| 203 | | * `\new(t)` : new (default) value of `Dytype` t |
| 204 | | * `\defined(e)` : is `e` defined? `Bool` type |
| 205 | | * `\cast(e, T)` : casts `e` to a value of the named type |
| 206 | | * need to list all of the legal casts and what they mean exactly |
| 207 | | * cast of integer to array-of-boolean, and vice-versa? |
| 208 | | * **Instead of casts would it be better to have explicit functions for each legal kind of cast?** |
| 209 | | * `\ite(e1, e2, e3)`: if-then-else (conditional) expression, equivalent to `e1?e2:e3` in C. |
| 210 | | * `e0(e1,...,en)` : a function invocation where `e` must evaluate to either an abstract or pure system function |
| | 149 | Logical |
| | 150 | * `\true`, `\false` : literal values of type `Bool` |
| | 151 | * `\not(e)` : logical not |
| | 152 | * `\and(e1, e2)`, `\or(e1, e2)`: logical and/or operation |
| | 153 | * `\eq(e1, e2)`, `\neq(e1, e2)`: equality/inequality test |
| | 154 | * `\forall <i1:T1, i2:T2, ...>, e1, e2` : universal quantification. For all i1 in type T1, i2 in type T2, ...: if e1 holds, then e2 holds. The only reason for having two expressions e1 and e2 is possible side-effects (exceptions) in e2 if e1 does not hold. For example, e1 can be x!=0, and e2 can safely divide by 0. |
| | 155 | * `\exists <i1:T1, i2:T2, ...>, e1, e2`: existential quantification. There is some i1 in type T1, i2 in type T2, ..., such that e1 holds and e2 holds. |
| | 156 | Numeric |
| | 157 | * 123, -123, 3.1415, etc. : values of type `Integer`, `Int`, `Real`, `Float`. **NEED TO BE MORE SPECIFIC** |
| | 158 | * `\add(e1, e2)` : numeric addition. |
| | 159 | * `e1` and `e2` have the same numeric type. Note that there are no "automatic conversions" as there are in C. If the original expressions have different types, explicit casts must be inserted. |
| | 160 | * `\sub(e1, e2)` : subtraction |
| | 161 | * `\mul(e1, e2)` : multiplication |
| | 162 | * `\div(e1, e2)` : division |
| | 163 | * If both are integer types, the result is integer division. Otherwise it is real division. Need to define what happens for negative integers. |
| | 164 | * `\mod(e1, e2)` : integer modulus |
| | 165 | * `\neg(e)` : negative |
| | 166 | * `\lt(e1, e2)`, `\lte(e1, e2)`: less than/less than or equal to |
| | 167 | Characters and Strings |
| | 168 | * 'a', 'b', ... : Char values. **UNICODE?** |
| | 169 | * `"abc"` : string literals: value of type `Array[Char, n+1]`, where n is the length of the string (the last element is the character `\0`) |
| | 170 | Ranges and Domains |
| | 171 | * `\range(e1,e2,e3)` : value of type `Range` consisting of the integers e1, e1+e3, e1+2*e3, ... that are less than or equal to e2. |
| | 172 | * `\domain(<r1,...,rn>)` : value of type `Domain[n]`, the ordered Cartesian product of the n ranges (dictionary order) |
| | 173 | * `\hasnext(dom, <i, j, …>)`: an expression of boolean type, testing if the domain `dom` contains any element after `<i, j, ...>` |
| | 174 | Arrays |
| | 175 | * `\array(T, <e0, ..., en-1>)`: value of type `Array[T, n]`, a literal array |
| | 176 | * `\array(T, n, e)`: value of type `Array[T,n]` in which each of the n elements is `e` |
| | 177 | * `\asub(e1, e2)` : array subscript expression. Note that `e1` must have array type, not pointer type. (This is different from C.) If `e1` has pointer type, use `\deref(\padd(e1, e2))` instead. |
| | 178 | * `\seq_add(a,e)` : array obtained by adding element e to the end of the array. Original array a is not modified. |
| | 179 | * `\seq_append(a1,a2)` : array obtained by concatenating two arrays. Original array not modified. |
| | 180 | * `\seq_remove(a,i)` : array obtained by removing element at position i from a. Original array a not modified. **WHAT HAPPENS TO REFERENCES INTO A** |
| | 181 | * `\bit_and(e1, e2)`, `\bit_or(e1, e2)`, `\bit_xor(e1, e2)`, `\bit_comp(e1)` : bit-wise operations: arguments are arrays of booleans of equal length. |
| | 182 | Tuples |
| | 183 | * `\tuple(S, <e0, e1, ...>)` : value of tuple type `S` (tuple literal) |
| | 184 | * `\tsel(e1, i)` : tuple selection of component i of e1. i must be a literal natural number. |
| | 185 | Pointers and Memory |
| | 186 | * `NULL` : value of type `void*` |
| | 187 | * `\deref(e)` : pointer dereference |
| | 188 | * `\addr(e)` : address-of operator |
| | 189 | * `\padd(e1, e2)`: pointer addition. `e1` has pointer type and `e2` has an integer type or range type. If `e2` has integer type the result has pointer type. Otherwise, the result has `Mem` type. |
| | 190 | * `\psub(e1,e2)`: pointer subtraction |
| | 191 | * `\mem_reach(ptr)`, where `ptr` is an expression with a pointer type. This represents the set of all memory units reachable from `ptr`, including the memory unit pointed to by `ptr` itself. |
| | 192 | * `\mem_union(mem1, mem2)`, where `mem1` and `mem2` are expressions of type `Memory`. This is the union of the two memory sets. |
| | 193 | * `\mem_isect(mem1, mem1)` : set intersection |
| | 194 | * `\mem_comp(mem1)` : set complement (everything not in `mem1`) |
| | 195 | * `\mem_slice(a, dom)`, where `a` is an expression of array type and `dom` is an expression of `Domain` type. The dimension of the array must match the dimension of the domain. This represents all memory units which are the cells in the array indexed by a tuple in `dom`. |
| | 196 | Scopes and Processes |
| | 197 | * `\root`, `\here` : values of type `Scope` |
| | 198 | * `\self`, `\proc_null` : values of type `Proc` |
| | 199 | Other |
| | 200 | * variables |
| | 201 | * `\sizeof_type(t)` : the size of the dynamic type t; `Integer` type |
| | 202 | * `\sizeof_expr(e)` : the size of the value of expression `e`; `Integer` type |
| | 203 | * `\new(t)` : new (default) value of `Dytype` t |
| | 204 | * `\defined(e)` : is `e` defined? `Bool` type |
| | 205 | * `\cast(e, T)` : casts `e` to a value of the named type |
| | 206 | * need to list all of the legal casts and what they mean exactly |
| | 207 | * cast of integer to array-of-boolean, and vice-versa? |
| | 208 | * **Instead of casts would it be better to have explicit functions for each legal kind of cast?** |
| | 209 | * `\ite(e1, e2, e3)`: if-then-else (conditional) expression, equivalent to `e1?e2:e3` in C. |
| | 210 | * `e0(e1,...,en)` : a function invocation where `e` must evaluate to either an abstract or pure system function |
