Manuel Kauers Hagenberg, December 20, 2002 RISC-Linz

Formal Specification of Abstract Datatypes

Exercise 1: Loose Specifications

1. Design a loose specification with constructors, say sp, for the algebra of sets containing among others the following operations:

∅: → set  the empty set
Insert : set × el → set adds an element to a set
Delete : set × el → set removes an element from a set
∪: set × set → set  set union
∈: el × set → bool  element predicate

Hint: Some of the equations that must hold are, for s: set, n, m: el

Insert(Insert(s, n), n) = Insert(s, n)
Insert(Insert(s, n), m) = Insert(Insert(s, m), n).

Let sp be defined as follows:

loose spec sp

sorts:  bool, el, set
operators:  True : → bool

False : → bool ∅: → set Insert : set × el → set Delete : set × el → set ∪ : set × set → set ∈ : el × set → bool

generated sorts: bool, set
constructors:  True : → bool

False : → bool ∅: → set Insert : set × el → set

variables:  s, s_{1}, s_{2} : set

e, m, n: el

axioms:  False ≠ True

Insert(Insert(s, n), n) = Insert(s, n) Insert(Insert(s, n), m) = Insert(Insert(s, m), n) ∅ ∪ s = s Insert(s_{1}, e) ∪ s_{2} = Insert(s_{1} ∪ s_{2}, e) Delete(∅, e) = ∅ Delete(Insert(s, e), e) = Delete(s, e) Insert(s_{1}, e) ≠ Delete(s_{2}, e) m ≠ n ⇒ Delete(Insert(s, m), n) = Insert(Delete(s, n), m) (e ∈ s) = True ⇔ s = Insert(s, e) (e ∈ s) = False ⇔ s = Delete(s, e)

end spec.

2. Prove that sp is strictly adequate. Hint: The abstract datatype “set” is defined as set := {a : a ≈ S} where S is the sp-algebra for which e.g. holds

S(set) := The set of all el-sets
S(Insert)(s, x) := s ∪ {x}
S(Delete)(s, x) := s \ {x}
S(∪)(s_{1}, s_{2}) := s_{1} ∪ s_{2}
S(∈)(x, s) := \{ \begin{matrix}true & if x ∈ s \\ false & otherwise \end{matrix}

Proof sketch (please elaborate in detail): to show that sp is strictly adequate, it suffices to show that every element of set is an element of M(sp) and vice versa. This amounts to showing that (i) S is a model of the axioms of sp and that (ii) every model A of the axioms of sp is isomorphic to S. To show the second, use induction as demonstrated in class.

Consider the algebra S which is defined as follows:

S(bool) := {true, false}
S(set) := The set of all finite sets with elements of type el
S(el) := An arbitrary set
S(True) := true
S(False) := false
S(∅) := ∅
S(Insert)(s, e) := s ∪ {e}
S(Delete)(s, e) := s \ {e}
S(∪)(s_{1}, s_{2}) := s_{1} ∪ s_{2}
S(∈)(e, s) := \{ \begin{matrix}true & if e ∈ s \\ false & otherwise \end{matrix}

We show that S is a model of sp and that every other model of sp is isomorphic to S.

First, S is a model of sp: We have to check that for all sets, elements and boolean values, all axioms of sp are satisfied. So, consider the axioms of sp.

For the purely equational axioms, i.e. for all but the last two axiom, there is nothing to prove. We simply state the claims and refer to Zermelo Fraenkel or something similar for rigorous proofs of the corresponding properties of sets.

S(False) ≠ S(True)
⇔  false ≠ true
S(Insert(Insert(s, n), n)) = S(Insert(s, n))
⇔ (S(s) ∪ {S(n)}) ∪ {S(n)} = S(s) ∪ {S(n)}
S(Insert(Insert(s, n), m)) = S(Insert(Insert(s, m), n))
⇔ (S(s) ∪ {S(n)}) ∪ {S(m)} = (S(s) ∪ {S(m)}) ∪ {S(m)}

S(∅ ∪ s) = S(s)
⇔  ∅ ∪ S(s) = S(s)
S(Insert(s_{1}, e) ∪ s_{2}) = S(Insert(s_{1} ∪ s_{2}, e))
⇔ (S(s_{1}) ∪ {S(e)}) ∪ S(s_{2}) = (S(s_{1}) ∪ S(s_{2})) ∪ {S(e)}
S(Delete(∅, e)) = S(∅)
⇔  ∅ \ {S(e)} = ∅
S(Delete(Insert(s, e), e)) = S(Delete(s, e))
⇔  (S(s) ∪ {S(e)}) \ {e} = S(s) \ {S(e)}
S(Insert(s_{1}, e)) ≠ S(Delete(s_{2}, e))
⇔  S(s_{1}) ∪ {S(e)} ≠ S(s_{2}) \ {S(e)}

It remains to show that also the last three axiom

m ≠ n ⇒ Delete(Insert(s, m), n) = Insert(Delete(s, n), m)
(e ∈ s) = True ⇔ s = Insert(s, e)
(e ∈ s) = False ⇔ s = Delete(s, e)

As for the first of them, we have to check

S(m) ≠ S(n) ⇒ (S(s) ∪ {S(m)}) \ {S(n)} = (S(s) \ {S(n)}) ∪ {S(m)} .

As for the next one, we have to check

S(e) ∈ S(s) ⇔ S(s) = S(s) ∪ {S(e)} .

As for the last one, we have to check

S(e) ∈ S(s) ⇔ S(s) = S(s) \ {S(e)} .

Summarizing, we have “shown” that S is a model of sp.

It remains to show that each other model A of sp is isomorphic to S. We show this by providing an isomorphism between S and A. Let h: S → A be defined by

h(true) := A(True)
h(false) := A(False)
h(∅) := A(∅)
h({S(a_{1}), …, S(a_{r})}) := A(Insert(… Insert(Insert(∅, a_{1}), a_{2}) …, a_{r})).

For the bool type the isomorphism property is immediate by use of the axiom False ≠ True. In what follows, we therefore restrict ourselves to the set type.

First, we show that h is well defined, injective, and surjective.

• h is well defined, because A is a model of sp by assumption and so it satisfies the axioms of sp. We conclude

A(Insert(… Insert(Insert(∅, a_{1}), a_{2}), …, a_{r}))
= A(Insert(… Insert(Insert(∅, a_{π(1)}), a_{π(2)}), …, a_{π(r)}))

for any permutation π ∈ S_{r}.

• h is surjective. To show: h(S(set)) = A(set). First, it is immediate that h(S(set)) ⊆ A(set): Write

s := {a_{1}, a_{2}, …, a_{r}} ∈ S(set)

as

s = {a_{1}} ∪ {a_{2}} ∪ ⋯ ∪ {a_{r}}.

Then

h(s) = A(Insert(… Insert(Insert(∅, h(a_{1})), h(a_{2})) …, h(a_{r}))) ∈ A(set).

As for the other inclusion, it suffices to show that every term t: set has a representation of the form that appears in the definition of h. Consider the map

Φ: T_{Σ} → T_{Σ}

which is recursively defined by

Φ(∅) := ∅,
Φ(Insert(t, m)) := \{ \begin{matrix}Φ(t) & if m is subterm of Φ(t) \\ Insert(Φ(t), m) & else \end{matrix}
Φ(∅ ∪ t) := Φ(t)
Φ(Insert(t_{1}, e) ∪ t_{2}) := Insert(Φ(t_{1} ∪ t_{2}), e)
Φ(Delete(t_{1}, e) ∪ t_{2}) := Φ(Φ(Delete(t_{1}, e)) ∪ t_{2})
Φ((t_{1} ∪ t_{2}) ∪ t_{3}) := Φ(Φ(t_{1} ∪ t_{2}) ∪ t_{3})
Φ(Delete(∅), n) := ∅
Φ(Delete(Delete(t, m), n)) := Φ(Delete(Φ(Delete(t, m)), n)),
Φ(Delete(Insert(t, m), n)) := \{ \begin{matrix}Φ(t) & m = n \\ Φ(Insert(t, m)) & m ≠ n \end{matrix}
Φ(Delete(t_{1} ∪ t_{2}), n) := Φ(Delete(Φ(t_{1} ∪ t_{2}), n))

By structural induction, it is easy to see that M ⊧ Φ(t) = t for every model M and every term t. Furthermore, iterated application of Φ will always terminate and finally give a term of the desired form.

set is generated, which means that every element of A(set) can be expressed by some term t. Also, we know that every term t has an equivalent term t̃= Φ^{n}(t) of the form which appears in the definition of h, and hence A(t) = h(s) for some s ∈ S(set) which can be read of the term t̃.

• h is injective: Assume there are terms a, b such that S(a) ≠ S(b). Without loss of generality, we can assume the existence of an element S(e) ∈ S(a)\ S(b) (exchange roles of a and b if necessary). We know that S(e) ∈ S(a) and S(e) ∉ S(b), i.e. S(e ∈ a) = true und S(e ∈ b) = false. By the according axioms of sp, we can conclude

a = Insert(a, e), b = Delete(b, e).

Since A is a model, we also know that

A(a) = A(Insert(a, e)), A(b) = A(Delete(b, e))

and hence

A(a) = A(Insert(a, e)) ≠ A(Delete(b, e)) = A(b)

so A(a) ≠ A(b) which was to prove.

Now, we know that h is a bijection between S(set) and A(set). It remains to show that it is also a homomorphism.

For the constant term ∅, the claim is immediate by the definition of h. For Insert and Delete terms we show the claim by computation. Note that each step is justified by the axioms of sp, the definition of h, and/or the definition of semantics. Take a set s = {s_{1}, …, s_{r}} and an element a. Then

h(S(Insert)(s, a)) = h(s ∪ {a})

= h({s_{1}, …, s_{r}, a}) = A(Insert(Insert(… Insert(∅, s_{1}) …, s_{r}), a)) = A(Insert)(A(Insert(… Insert(∅, s_{1}) …, s_{r})), A(a)) = A(Insert)(h(s), h(a)).

h(S(Delete)(s, a)) = h(s \ {a})

Case 1. a ∉ s. Then

h(s \ {a}) = h(s)

= h({s_{1}, …, s_{r}}) = A(Insert(… Insert(∅, s_{1}) …, s_{r})) = A(Delete(Insert(… Insert(∅, s_{1}) …, s_{r}), a)) = A(Delete)(A(Insert(… Insert(∅, s_{1}) …, s_{r})), A(a)) = A(Delete)(h(s), h(a)).

Case 2. a ∈ s. W.l.o.g. a = s_{r}. Then

h(s \ {a}) = h({s_{1}, …, s_{r−1}})

= A(Insert(… Insert(∅, s_{1}) …, s_{r−1})) = A(Delete(Insert(… Insert(∅, s_{1}) …, s_{r}), s_{r})) = A(Delete)(A(Insert(… Insert(∅, s_{1}) …, s_{r})), A(a)) = A(Delete)(h(s), h(a)).

It remains to consider the union. Take two sets s = {s_{1}, …, s_{r}} and a set t. We proceed by induction on the size of t. In the base case, we have

h(S(∪)(t, s)) = h(S(∪)(∅, s))

= h(s) = A(Insert(… Insert(∅, s_{1}) …, s_{r})) = A(∅ ∪ Insert(… Insert(∅, s_{1}) …, s_{r})) = A(∪)(A(∅), A(Insert(… Insert(∅, s_{1}) …, s_{r}))) = A(∪)(h(∅), h(s)).

As for the induction step, assume that the claim holds for all sets t = {t_{1}, …, t_{m}} of size m ≥ 0, and prove that it still holds for t ∪ {t_{m+1}} where t_{m+1} ∉ t.

h(S(∪)(t ∪ {t_{m+1}}, s)) = h({t_{1}, …, t_{m+1}, s_{1}, …, s_{r}})
= h({t_{1}, …, t_{m}, s_{1}, …, s_{r}} ∪ {t_{m+1}})
= A(Insert)(h({t_{1}, …, t_{m}, s_{1}, …, s_{r}}), h(t_{m+1}))
= A(Insert)(h(t ∪ s), h(t_{m+1}))
= A(Insert)(A(∪)(h(t), h(s)), h(t_{m+1}))
= A(Insert(Insert(… Insert(∅, t_{1}) …, t_{m}) ∪

Insert(… Insert(∅, s_{1}) …, s_{r}), t_{m+1}))

= A(Insert(… Insert(∅, t_{1}) …, t_{m+1}) ∪
Insert(… Insert(∅, s_{1}) …, s_{r}))
= A(∪)(Insert(… Insert(∅, t_{1}) …, t_{m+1}),
Insert(… Insert(∅, s_{1}) …, s_{r}))
= A(∪)(h({t_{1}, …, t_{m+1}}), h({s_{1}, …, s_{r}}))
= A(∪)(h(t ∪ {t_{m+1}}), h(s)).

We have now proven that h is compatible with all the operations of sp, so h is a homomorphism. And since we proved before that h is also bijective, we finally know that h is an isomorphism. This shows that S is isomorphic to A and since A was an arbitrary model of sp, all models are isomorphic to S. This means that S is strictly adequate quod erat demonstrandum.

3. Let e: el and s, t: set be arbitrary. Prove

M(sp) ⊧ (e ∈ Delete(s, e)) = False
M(sp) ⊧ (e ∈ s) ⇒ (e ∈ s ∪ t) = True.

To show this, use induction as a proof method.

We assume that the lecturer had a different specification in mind when he designed this exercise, because for our axiom system, it makes no sense to attack the first claim by induction. Using the last axiom on page 1, we find that

(e ∈ Delete(s, e)) = False

is equivalent to

Delete(s, e) = Delete(s, e),

i.e. there is nothing to prove.

Also for the second claim, there is a much easier way than induction. Let A be a generated model of sp. Let s: set and e: el be arbitrary terms with A(e ∈ s) = A(True), and let t: set. Then,

A(e ∈ s) = A(True)
⇒  A(Insert(s, e)) = A(s)
⇒ A(Insert(s, e) ∪ t) = A(s ∪ t)
⇒ A(Insert(s ∪ t, e)) = A(s ∪ t)
⇒  A(e ∈ s ∪ t) = A(True).

We dare to hand this in as a solution because every proof (without induction) can be viewed as a special induction proof in which the induction step makes no use of the induction hypothesis.