 | 1.5 Finite maps |
| 
| 1 Changes to RSL |
| 
| 1.7 Test cases |
|
| 1.6 Extra meanings for ∈, ∉, and hd |
1.6 Extra meanings for ∈, ∉, and hd
The infix operators ∈ and ∉ can now be applied to lists
and maps as well as sets. The meanings correspond to the following
definitions for arbitrary types T and U:
|
| | | | | | | | | | | | |
| value |
| ∈ : T × Tω → Bool |
| t ∈ l ≡ t ∈ elems l, |
| |
| ∉ : T × Tω → Bool |
| t ∉ l ≡ t ∉ elems l, |
| |
| ∈ : T × (T -~m-> U) → Bool |
| t ∈ m ≡ t ∈ dom m, |
| |
| ∉ : T × (T -~m-> U) → Bool |
| t ∉ m ≡ t ∉ dom m
|
The point of adding these meanings is that the RSL is shorter, and
that it is easier to translate the RSL into more efficient code, as
there is no need to generate a set from the list or map before
applying ∈ or ∉.
The prefix operator hd can now be applied to (non-empty) sets and
maps. The meaning of hd in these two cases is as if hd were
defined as follows for arbitrary types T and U:
|
| | | | | | | | | | | | |
| value |
| hd : T-infset -~-> T |
| hd : (T -~m-> U) -~-> T |
| axiom |
| ∀ s : T-infset • s ≠ {} ⇒ hd s ∈ s |
| ∀ m : T -~m-> U • m ≠ [] ⇒ hd m ∈ m
|
The operator hd can therefore be used to select an arbitrary member of a
non-empty set or of the domain of a non-empty map. This allows many
examples of quantified and comprehended expressions to be written in
ways that allows them to be translated. The choice of hd for
this operator may seem a little strange, but using an existing
operator avoids adding another keyword.
Chris George, April 17, 2008
| 1.6 Extra meanings for ∈, ∉, and hd |
| 1.5 Finite maps |
| |
| 1 Changes to RSL |
| |
| 1.7 Test cases |
|