Manuel Kauers Hagenberg, January 29, 2003 RISC-Linz

Formal Specification of Abstract Datatypes

Exercise 2: Initial Specifications

Consider the classical algebra of integers containing the operators Zero, Succ, Pred, Plus, Minus, Mult, and Leq.

1. Design an initial specification for the abstract data type “integer.”

initial spec sp

sorts:  bool, int
operators:  True : → bool

False : → bool And : bool × bool → bool Impl : bool × bool → bool Succ : int → int Pred : int → int Zero : → int Plus : int × int → int Minus : int × int → int Mult : int × int → int Leq : int × int → bool

generated sorts: bool, int
variables:  a, b, m, n, k
eqns:  True ≠ False

And(a, True) = a And(a, False) = False Impl(False, a) = True Impl(True, a) = a Succ(Pred(n)) = n Pred(Succ(n)) = n Plus(m, Succ(n)) = Succ(Plus(m, n)) Plus(m, Pred(n)) = Pred(Plus(m, n)) Plus(m, Zero) = m Minus(m, Succ(n)) = Pred(Minus(m, n)) Minus(m, Pred(n)) = Succ(Minus(m, n)) Minus(m, Zero) = m Mult(m, Succ(n)) = Plus(Mult(m, n), m) Mult(m, Pred(n)) = Minus(Mult(m, n), m) Mult(m, Zero) = Zero Leq(Zero, Zero) = True Leq(Zero, Succ(Zero)) = True Leq(Zero, Pred(Zero)) = False Impl(And(Leq(m, n), Leq(n, k)), Leq(m, k)) = True Leq(m, n) = Leq(Succ(m), Succ(n))

end spec.

2. Show that this specification is adequate using the proof technique of characteristic term algebras.

First we extend the abbreviating notation Succ^{n}(Zero) also to negative n. In particular, we mean

Succ^{n}(Zero) = \{ \begin{matrix}Zero & if n = 0 \\ Succ(Succ^{n−1}(Zero)) & if n > 0 \\ Pred(Succ^{n+1}(Zero)) & if n < 0 \end{matrix}

For instance, Succ^{−2}(Zero) = Pred(Pred(Zero)), where “=” means that both sides denote the same term.

With this, we are ready to define the characteristic term algebra as follows:

C(bool) = {True, False}
C(int) = {Succ^{n}(Zero) : n ∈ ℤ}

where the operations of sp are defined as follows:

C(True) := True
C(False) := False
C(Succ)(Succ^{n}(Zero)) := Succ^{n+1}(Zero)
C(Pred)(Succ^{n}(Zero)) := Succ^{n−1}(Zero)
C(Plus)(Succ^{n}(Zero), Succ^{m}(Zero)) := Succ^{n+m}(Zero)
C(Minus)(Succ^{n}(Zero), Succ^{m}(Zero)) := Succ^{n−m}(Zero)
C(Mult)(Succ^{n}(Zero), Succ^{m}(Zero)) := Succ^{n·m}(Zero)
C(Leq)(Succ^{n}(Zero), Succ^{m}(Zero)) := \{ \begin{matrix}True & if n ≥ m \\ False & otherwise \end{matrix}

In these definitions, m and n denote integers, and ·, +, − denote the usual operations on ℤ. Furthermore, C(And) and C(Impl) are defined as usual.

In order to show that sp is adequate, we show that C ⊧ sp and that C is a characteristic term algebra. For the latter, we have to show that A ⊧ (C(t) = t) for every model A and every term t.

In a first step, we have to show that C is actually a model of sp. For the boolean sort, this is trivial and left to the reader. (However, we don’t claim that what we don’t leave to the reader is not trivial…)

We proceed by checking consistency of C with the axioms of sp. Throughout the proofs, we assume C(m) = Succ^{p}(Zero), C(n) = Succ^{q}(Zero) and C(k) = Succ^{r}(Zero) with p, q, r ∈ ℤ.

• Succ(Pred(m)) = Pred(Succ(m)) = m is immediate from the definition.

• Plus(m, Succ(n)) = Succ(Plus(m, n)):

C(Plus(m, Succ(n))) = C(Plus)(C(m), C(Succ(n)))

= C(Plus)(C(m), C(Succ)(C(n))) = C(Plus)(Succ^{p}(Zero), C(Succ)(Succ^{q}(Zero))) = C(Plus)(Succ^{p}(Zero), Succ^{q+1}(Zero)) = Succ^{p+q+1}(Zero) = Succ(Succ^{p+q}(Zero)) = C(Succ)(Succ^{p+q}(Zero)) = C(Succ)(C(Plus)(Succ^{p}(Zero), Succ^{q}(Zero))) = C(Succ)(C(Plus)(C(m), C(n))) = C(Succ(Plus(m, n))).

The axioms Plus(m, Zero) and

Plus(m, Pred(n)) = Pred(Plus(m, n))

are verified in the same way.

• Minus(m, Succ(n)) = Pred(Minus(m, n)):

C(Minus(m, Succ(n))) = C(Minus)(C(m), C(Succ(n)))

= C(Minus)(C(m), C(Succ)(C(n))) = C(Minus)(Succ^{p}(Zero), Succ(Succ^{q}(Zero))) = C(Minus)(Succ^{p}(Zero), Succ^{q+1}(Zero)) = Succ^{p−(q+1)}(Zero) = Succ^{(p−q)−1}(Zero) = Pred(Succ^{p−q}(Zero)) = C(Pred)(Succ^{p−q}(Zero)) = C(Pred)(C(Minus)(Succ^{p}(Zero), Succ^{q}(Zero))) = C(Pred)(C(Minus)(C(m), C(n))) = C(Pred)(C(Minus(m, n))) = C(Pred(Minus(m, n))).

The axioms Minus(m, Zero) = m and

Minus(m, Pred(n)) = Succ(Plus(m, n))

are verified in the same way.

• Mult(m, Succ(n)) = Plus(Mult(m, n), n):

C(Mult(m, Succ(n))) = C(Mult)(C(m), C(Succ(n)))

= C(Mult)(C(m), C(Succ)(C(n))) = C(Mult)(Succ^{p}(Zero), C(Succ)(Succ^{q}(Zero))) = C(Mult)(Succ^{p}(Zero), Succ^{q+1}(Zero)) = Succ^{p·(q+1)}(Zero) = Succ^{pq+p}(Zero) = C(Plus)(Succ^{pq}(Zero), Succ(p)(Zero)) = C(Plus)(C(Mult)(Succ^{p}(Zero), Succ^{q}(Zero)),

Succ^{p}(Zero))

= C(Plus)(C(Mult)(C(m), C(n)), C(m)) = C(Plus)(C(Mult(m, n)), C(m)) = C(Plus(Mult(m, n)), m).

The axioms

Mult(m, Pred(n)) = Minus(Mult(m, n), m) and Mult(n, Zero) = Zero

are verified in the same way.

• Leq(Zero, Zero) = True, Leq(Zero, Succ(Zero)) = True and

Leq(Zero, Pred(Zero)) = False

are immediate from the definition (because 0 ≤ 1 and 0 > −1 in the integers).

• Impl(And(Leq(m, n), Leq(n, k)), Leq(m, k)) = True:

C(Impl(And(Leq(m, n), Leq(n, k)), Leq(m, k)))

= C(Impl)(C(And(Leq(m, n), Leq(n, k))), C(Leq(m, k)))
= C(Impl)(C(And)(C(Leq)(C(m), C(n)), C(Leq)(C(n), C(k))),

C(Leq)(C(m), C(k)))

= C(Impl)(C(And)(C(Leq)(Succ^{p}(Zero), Succ^{q}(Zero)),

C(Leq)(Succ^{q}(Zero), Succ^{r}(Zero))), C(Leq)(Succ^{p}(Zero), Succ^{r}(Zero))).

By the definition of C(Impl), C(And), and C(Leq), and by the fact that

p ≤ q ∧ q ≤ r ⇒ p ≤ r

in the integers (because of ≤’s properties there), the last term is equal to True as was to be shown.

• Leq(m, n) = Leq(Succ(m), Succ(n)): Similar to the last item, it is easy to see that this equation holds if and only if

p ≤ q ⇒ p + 1 ≤ q + 1

which is true in the integers, so the equation is true as well.

We finally conclude C ⊧ sp, i.e. C is a model of sp. It remains to show that C is characteristic, i.e. that A ⊧ (C(t) = t) for every model A of sp and every term t.

Let A be a model of sp. In the sequel, we will omit A(·) to make the proofs more readable. Moreover, we will write m ≡ n instead of A ⊧ (m = n). By simply writing “=” we mean syntactical equality of terms.

We have to prove C(t) ≡ t for all terms t. We proceed by structural induction. For t = Zero we have C(Zero) = Zero by definition of C, i.e. there is nothing to prove.

Now assume that C(s) ≡ s, and C(t) ≡ t for arbitrary terms s, t with C(s) = Succ^{m}(Zero), C(t) = Succ^{n}(Zero) (m, n ∈ ℤ).

• C(Succ(s)) ≡ Succ(s), C(Pred(s)) ≡ Pred(s) are immediate from the definition of C and the induction hypothesis.

• C(Plus(s, t)) ≡ Plus(s, t):

C(Plus(s, t)) = C(Plus)(C(s), C(t))

= C(Plus)(Succ^{m}(Zero), Succ^{n}(Zero))

= Succ^{m+n}(Zero) ≡^{∗} Plus(Succ^{m}(Zero), Succ^{n}(Zero))

= Plus(C(s), C(t)) ≡^{IH} Plus(s, t).

The asterix ∗ in the 5th step is now proven by two inductions on n. For n = 0, it is just

Succ^{m}(Zero) ≡ Plus(Succ^{m}(Zero), Zero)

which is one of the axioms. Now assume that

Succ^{m+n}(Zero) ≡ Plus(Succ^{m}(Zero), Succ^{n}(Zero))

for some n > 0 and show the claim for n + 1. Then

Plus(Succ^{m}(Zero), Succ^{n+1}(Zero))
= Plus(Succ^{m}(Zero), Succ(Succ^{n}(Zero)))
≡ Succ(Plus(Succ^{m}(Zero), Succ^{n}(Zero)))
≡^{IH} Succ(Succ^{m+n}(Zero))
= Succ^{m+n+1}(Zero).

This shows the claim for n ≥ 0. Now assume that

Succ^{m+n}(Zero) ≡ Plus(Succ^{m}(Zero), Succ^{n}(Zero))

for some n < 0, and show the claim for n − 1. Then

Plus(Succ^{m}(Zero), Succ^{n−1}(Zero))
= Plus(Succ^{m}(Zero), Pred(Succ^{n}(Zero)))
≡ Pred(Plus(Succ^{m}(Zero), Succ^{n}(Zero)))
≡^{IH} Pred(Succ^{m+n}(Zero))
= Succ^{m+n−1}(Zero).

Putting things together, we showed the claim for all n ∈ ℤ.

• C(Minus(s, t)) ≡ Minus(s, t): This should work in the same fashion. Let’s see:

C(Minus(s, t)) = C(Minus)(C(s), C(t))

= C(Minus)(Succ^{m}(Zero), Succ^{n}(Zero))

= Succ^{m−n}(Zero) ≡^{∗} Minus(Succ^{m}(Zero), Succ^{n}(Zero)) = Minus(C(s), C(t)) ≡^{IH} Minus(s, t).

We prove ∗ again by induction on n. First, for n = 0 we have

Succ^{m}(Zero) ≡ Minus(Succ^{m}(Zero), Zero)

by the corresponding axiom. Now assume that ∗ holds for n > 0 and show that it also holds for n + 1:

Minus(Succ^{m}(Zero), Succ^{n+1}(Zero))

= Minus(Succ^{m}(Zero), Succ(Succ^{n}(Zero)))
≡ Pred(Minus(Succ^{m}(Zero), Succ^{n}(Zero)))
≡^{IH} Pred(Succ^{m−n}(Zero))
≡ Succ^{m−n−1}(Zero) = Succ^{m−(n+1)}(Zero).

Note that Pred(Succ^{k}(Zero)) ≡ Succ^{k−1}(Zero) is true for both k ≥ 0 (by the axiom Pred(Succ(x)) = x) and k < 0 (by the definition of Succ^{k}(Zero)). For the second induction, assume ∗ for n < 0 and show it for n − 1.

Minus(Succ^{m}(Zero), Succ^{n−1}(Zero))

= Minus(Succ^{m}(Zero), Pred(Succ^{n}(Zero)))
≡ Succ(Minus(Succ^{m}(Zero), Succ^{n}(Zero)))
≡^{IH} Succ(Succ^{m−n}(Zero))
≡ Succ^{m−n+1}(Zero) = Succ^{m−(n−1)}(Zero),

where the last but one step is tackled the same way as above.

• C(Mult(s, t)) ≡ Mult(s, t):

C(Mult(s, t)) = C(Mult)(C(s), C(t))

= C(Mult)(Succ^{m}(Zero), Succ^{n}(Zero))

= Succ^{m·n}(Zero) ≡^{∗} Mult(Succ^{m}(Zero), Succ^{n}(Zero)) = Mult(C(s), C(t)) ≡^{IH} Mult(s, t)

Proof of ∗ by induction on n: For n = 0, we have Succ^{m·0}(Zero) = Zero ≡ Mult(Succ^{m}(Zero), Zero) by an axiom. Assume ∗ for n > 0 and prove it for n + 1.

Mult(Succ^{m}(Zero), Succ^{n+1}(Zero))

= Mult(Succ^{m}(Zero), Succ(Succ^{n}(Zero)))
≡ Plus(Mult(Succ^{m}(Zero), Succ^{n}(Zero)), Succ^{n}(Zero))
≡^{IH} Plus(Succ^{m·n}(Zero), Succ^{n}(Zero))
≡ Succ^{m·n+n}(Zero) = Succ^{m·(n+1)}(Zero).

Note that the last but one step has already been proven in the second subproof, i.e. in the proof of C(Plus(s, t)) ≡ Plus(s, t). Now, assume that ∗ holds for n < 0 and prove it for n − 1.

Mult(Succ^{m}(Zero), Succ^{n−1}(Zero))

= Mult(Succ^{m}(Zero), Pred(Succ^{n}(Zero)))
≡ Minus(Mult(Succ^{m}(Zero), Succ^{n}(Zero)), Succ^{n}(Zero))
≡^{IH} Minus(Succ^{m·n}(Zero), Succ^{n}(Zero))
≡ Succ^{m·n−n}(Zero) = Succ^{m·(n−1)}(Zero).

• C(Leq(s, t)) ≡ Leq(s, t). First case: Assume m ≤ n.

C(Leq(s, t)) = C(Leq)(C(s), C(t)) = C(Leq)(Succ^{m}(Zero), Succ^{n}(Zero))
= True ≡^{∗} Leq(Succ^{m}(Zero), Succ^{n}(Zero))
= Leq(C(s), C(t)) ≡^{IH} Leq(s, t).

To see ∗, we prove

Leq(Zero, Succ^{k}(Zero)) ≡ True  (1)

for k ≥ 0, and

Leq(Succ^{m}(Zero), Succ^{n}(Zero)) ≡ Leq(Zero, Succ^{n−m}(Zero)). (2)

Then Leq(Succ^{m}(Zero), Succ^{n}(Zero)) ≡^{(2)} Leq(Zero, Succ^{n−m}(Zero)) ≡^{(1)} True taking k = n − m ≥ 0 in the second step. The proofs of (1) and (2) proceed by induction (what a surprise…).

(1) For the base case, Leq(Zero, Zero) ≡ True is an axiom. Now assume that Leq(Zero, Succ^{k}(Zero)) ≡ True. Then, by the linearity axiom

Leq(Succ(Zero), Succ^{k+1}(Zero)) = True,

and using transitivity and Leq(Zero, Succ(Zero)) leads to Leq(Zero, Succ^{k+1}(Zero)) = True.

(2) For the base case we have Leq(Succ^{0}(Zero), Succ^{n}(Zero)) = Leq(Zero, Succ^{n−0}(Zero)),

i.e., there is nothing to prove. Now assume that

Leq(Succ^{m}(Zero), Succ^{n}(Zero)) = Leq(Zero, Succ^{n−m}(Zero)), holds for some m ∈ ℤ and any n ∈ ℤ. Then by the linearity axiom

Leq(Succ^{m+1}(Zero), Succ^{n}(Zero))

≡ Leq(Succ^{m+1−1}(Zero), Succ^{n−1}(Zero))
≡^{IH} Leq(Zero, Succ^{n−1−m}(Zero))
= Leq(Zero, Succ^{n−(m+1)}(Zero).

For the case when m > n, an analogous argument is possible. Sumarizing, we have shown that C is a characteristic term algebra and C is a model of sp. Obviously, C is a isomorphic to the natural algebra of integers, and putting all this things together is is shown that sp is an adequate specification of the integers.