Computer Aided Formal Reasoning Fall, 1995 Lecture notes 14 Judith Underwood

Abstract Data Types II

Today we’ll continue to look at abstract data types and their implementations; we’ll then examine specifications in general and tools available for developing a specification into an implementation.

Abstract Implementation

Last time we saw how to give a concrete implementation of an abstract data type and check that it satisfies the axioms in the specification. As an example, we looked at implementing stacks of natural numbers with the type list nat. We can also use one abstract data type to give an abstract implementation of another, and we will demonstrate this by using an abstract data type for arrays to implement stacks.

First, we describe the ADT for arrays (of natural numbers). We begin with the structure:

(* structure type *)
Record [Str_ARRAY:STR] ElimOver Type
Fields [Array   :Setoid]
       [newarray:Array.dom]
       [assign  :nat->Array.dom->nat->Array.dom]
       [access  :Array.dom->nat->nat];

Recall that Array:Setoid means Array is a type with equality. There are three array operations. First, newarray is an array with all elements zero (as we shall see). Second, assign, given a natural number n, an array A, and an index i, returns a new array identical to A except with A[i] set to n. Finally, access, given A and i, returns the value of A[i].

These intended behaviours are described by the axioms in the specification:

(* axioms *)
[A:Str_ARRAY];
[EqARRAY  = Equivalence (eq|A.Array)];
[AxARRAY1 = {i:nat}Eq (A.access A.newarray i) zero];
[AxARRAY2 = {n,i,j:nat}{arr:A.Array.dom}
    and ((Eq i j) ->
          (Eq (A.access (A.assign n arr i) j) n))
        ((not (Eq i j)) ->
          (Eq (A.access (A.assign n arr i) j) (A.access arr j)))
];
[Ax_ARRAY = and3 EqARRAY AxARRAY1 AxARRAY2];
Discharge A;
[ARRAY = make_SPEC Str_ARRAY Ax_ARRAY : SPEC];

Now we will use this ADT to provide an abstract implementation for stacks. Recall the (simple) ADT for stacks was:

Record [Str_STACK:STR] ElimOver Type
Fields [Stack:Setoid]
       [empty:Stack.dom]
       [push :nat->Stack.dom->Stack.dom]

       [pop  :Stack.dom->Stack.dom]
       [top  :Stack.dom->nat];
(* axioms *)
[S:Str_STACK];
[EqSTACK  = Equivalence (eq|S.Stack)];
[AxSTACK1 = eq (S.pop S.empty) S.empty];
[AxSTACK2 = Eq (S.top S.empty) zero];
[AxSTACK3 = {n:nat}{s:S.Stack.dom}eq (S.pop (S.push n s)) s];
[AxSTACK4 = {n:nat}{s:S.Stack.dom}Eq (S.top (S.push n s)) n];
[STACK = make_SPEC Str_STACK Ax_STACK : SPEC];

To give an abstract implementation of stacks using arrays, we provide a function from

ARRAY.Str to STACK.Str:
Goal refine_STACK_to_ARRAY :
     ARRAY.Str -> STACK.Str;
Intros A;
Lego> Refine make_Str_STACK;
Refine by  make_Str_STACK
  ?2 : Setoid
  ?3 : dom ?2
  ?4 : nat->(dom ?2)->dom ?2
  ?5 : (dom ?2)->dom ?2
  ?6 : (dom ?2)->nat

The idea is that a stack is a pair consisting of an array and a pointer to the array element just beyond the top of the stack. The pointer will be represented by a natural number, so that if the pointer is zero, we have the empty stack. We must describe these pairs and the intended equality on them in the Setoid part of the implementation:

Lego> Refine make_Setoid;
Refine by  make_Setoid
  ?7 : SET
  ?8 : ?7->?7->Prop
  ?3 : dom (make_Setoid ?7 ?8)
  ?4 : nat->(dom (make_Setoid ?7 ?8))->dom (make_Setoid ?7 ?8)
  ?5 : (dom (make_Setoid ?7 ?8))->dom (make_Setoid ?7 ?8)
  ?6 : (dom (make_Setoid ?7 ?8))->nat

The domain is a pair consisting of the carrier set of Array, extracted from A, along with nat. To make future goals look nicer, we give it a name:

[domImpl =  A.Array.dom # nat];
Lego> defn  domImpl = (dom (Array A))#nat
      domImpl : Type
Lego> Refine domImpl;
Refine by  domImpl
  ?8 : domImpl->domImpl->Prop

We now need to supply the equality predicate on these stacks; we’ll do this explicitly, by defining

eqImpl:
(* equality over the impl domain *)
[eqImpl [s,s':domImpl] =

       and (Eq s.2 s'.2)
          ({i:nat}(Lt i s.2)->
              (Eq (A.access s.1 i) (A.access s'.1 i)))];
Lego> Refine eqImpl;
Refine by  eqImpl
  ?3 : dom (make_Setoid domImpl eqImpl)
  ?4 : nat->(dom (make_Setoid domImpl eqImpl))->
                        dom (make_Setoid domImpl eqImpl)
  ?5 : (dom (make_Setoid domImpl eqImpl))->dom (make_Setoid domImpl eqImpl)
  ?6 : (dom (make_Setoid domImpl eqImpl))->nat

This says that two array-stacks are equal when their pointers are equal (as natural numbers) and for all indices i less than the pointer value, the arrays are equal at i.

The remainder of the implementation is fairly straightforward. The empty stack is

(A.newarray,zero)

push n s is implemented by assign:

(A.assign n s.1 s.2,suc s.2)

The new stack consists of the old array s.1 with place s.2 set equal to n. Note that push also increments the pointer (s.2).

pop s just decrements the pointer:

(s.1, pred s.2)

and top s returns either zero or the top of the stack if the pointer is nonzero. Recall that the pointer is the successor of the position of the top element of the stack.

if_zero s.2 zero (A.access s.1 (pred s.2));

The proof that, given an A:ARRAY.Str, the resulting implementation of stacks satisfies the axioms is reasonably straightforward.

General specification operations

Specification languages often include tools for manipulating specifications. These can be reflected in type theory as well. We can also describe some semantic properties we wish specifications to have. The definitions in this section are from lib_adt, which imports lib_sigma and lib_setoid. lib_sigma redefines sigma types as an inductive type and introduces fresh notation for working with them.

The basic definitions in the library are:

[STR = Type];                           (* class of structure types *)
(* class of specifications/ADTs *)
Record [SPEC:Type] ElimOver Type
Fields [Str:STR]
       [Ax: Str->Prop];
[Spec[S:STR]  = S->Prop];                   (* class of S-specifications *)
[Mod [SP:SPEC]= Sigma SP.Str SP.Ax];      (* model set of SP with proofs *)
[Consistent [SP:SPEC] = Ex [s:SP.Str] SP.Ax s]; (* consistency of a spec *)

The idea is that Mod SP is the type of models of the specification; a specification is consistent if it has a model.

We saw last time that we may wish to extend a specification with extra information – either by simply adding an axiom or by extending the signature as well. To extend the structure part of a specification, we combine the parts with a sigma type:

[Extend [SP:SPEC][ext_str:SP.Str->STR]
        [S'=Sigma SP.Str [s:SP.Str]s.ext_str]
        [ext_ax:S'->Prop]
      = make_SPEC S' [s':S']and (SP.Ax s'.sig_pi1) (ext_ax s')
      : SPEC
];

Note that ext_str can depend on SP. The new structure is a sigma type which pairs SP.Str and ext_str. The axioms must be expressed as a function from this new structure to Prop. Extending the axioms only is simpler:

[Extend_AxOnly [SP:SPEC][ext_ax:SP.Str->Prop]
      = make_SPEC SP.Str [s:SP.Str]and (SP.Ax s) (ext_ax s)
      : SPEC
];

Tools for combining specifications allow for modular implementation; a problem may be broken down into two or more independent parts which can be implemented separately, then recombined to form an implementation of the whole. Here are two such operations.

[Join [S|STR][SP,SP':S.Spec]
    = make_SPEC S [s:S]and (SP s) (SP' s)
    : SPEC
];

Join combines two axiom sets for a given structure S; to merge two different structures, we would use Cross:

(* Cross *)
[Cross [SP,SP':SPEC]
     = [S= Prod SP.Str SP'.Str]
       make_SPEC S [s:S]and (SP.Ax s.sig_pi1) (SP'.Ax s.sig_pi2)
     : SPEC
];

Cross combines two specifications by creating a new specification consisting of the product of the two structures and the conjunction of the two sets of axioms.