Formal Specifi cations—2 Algebraic 603
Consider an abstract data type which has four operations defi ned over the sorts s1, s2, s3 with syntax
opa : s1 s2 -> s1
opb : s1 s2 -> s2
opc : s1 s2 s3 -> s1
opd : s1 -> s1
and consider the reduction of the term t where
t = opd(opa(opc(k1,k2,k3),opb(m1,m2)))
where k1, m1 ∈ s1; k2, m2 ∈ s2 and k3, m3 ∈ s3. Any variable identifi er ending with 1 (2 or 3) will be taken
to belong to sort s1 (s2 or s3) respectively.
We now look for those axioms whose left-hand sides have opd as the left-most operation. (Remember,
we are choosing always to work from the left-hand side of a rule to the right). For the purpose of this
discussion, suppose two such axioms are found:
FORALL
u1 : s1
u2 : s2
u3 : s3
AXIOMS: ...