Extend the reasoning in the queue example of an alg. specification.

[cionx]

The book features the following example of an algebraic specification and its possible application:

1.  is_empty empty = true
2.  is_empty (enq x q) = false
3a. front (enq x q) = x            if is_empty q = true
3b. front (enq x q) = front q      if is_empty q = false
4a. deq (enq x q) = empty          if is_empty q = true
4b. deq (enq x q) = enq x (deq q)  if is_empty q = false

  front (deq (enq 1 (enq 2 empty)))
=   { equation 4b }
  front (enq 1 (deq (enq 2 empty)))
=   { equation 4a }
  front (enq 1 empty)
=   { equation 3a }
  1

But to use equations 3a, 4a and 4b we still need to explain why these equations apply. More explicitly, we need to argue why

• is_empty (enq 2 empty) is false to use 4b,
• is_empty empty is true to use 4a,
• is_empty empty is true to use 3a.

These points are intuitively clear. But I believe that in our formal setting we need to rely on equations 1 and 2 to ensure that our intuition is property reflected by the formalism.

[clarksmr]

Thanks!