Axiomatic Specification of ADTs

As you can see, these notes are not fully converted yet... stay tuned

Algebraic Specifications and Abstract Data Types

  OVERVIEW
    Algebraic Specs and Axiomatic Proofs
    Many-Sorted Algebras
    Syntax and Semantics of Specification
    Example: STACK type
    Example: SET type

  ASSIGNMENT: A6*

?Course 
?Lecture L06.1
?"Next Lecture" L07

:L06.1
WHAT ARE ALGEBRAIC SPECS?

  Up to now have seen axiomatic proof of programs
   with very simple data (integers)
 
  Exception: arrays... structured data

   The behavior of an array is unambiguously defined
   by the designer of a programming language.

   Inference rules and axioms for arrays (and for
   records and other built-in structured types) 
   can be designed from the language definition.

   So we can do axiomatic proofs with arrays, 
   records, etc.

:L06.1.1
USER-DEFINED TYPES

  What about types that are user-defined, that are
   not built-in to a programming language?

   Where is the definition of their behavior so we 
   can get axioms and inference rules for them?

  We need a way of specifying the behavior of 
   user-defined types so that their properties can be 
   used during verification of programs that use
   those types.

:L06.1.2
USER-DEFINED TYPES

  Specs of user-defined data types must be abstract,
   that is, they must state behavior and logical 
   properties without bias towards low-level details:

  Example:  Suppose we need to specify the behavior 
   of a data type STACK, with ops push, pop, etc...
   If we specify something like 
       push(S,e) is  S[(top+=1)] := e
       pop(S)    is  top -= 1
   we imply in the specs that a STACK is an array at
   the low implementation level...
   What if we wanted to build STACK as a linked list?
 
  Specs should not prefer or exclude any reasonable 
   implementation method...

L06.2
ALGEBRAIC SPECS and AXIOMATIC VERIFICATION

  We will specify the behavior of a user-defined 
   type as a many-sorted algebra

  Many-sorted algebra is 

    -- collection of elements of various types 
       (types are called "sorts")

    -- operations that manipulate these elements

:L06.2.1
ALGEBRAIC SPECS and AXIOMATIC VERIFICATION

  Specification has three main parts:

    -- syntax (what are the sorts, ops, arguments)

    -- semantics (what do the ops do?)

    -- restrictions (are there exceptions or limits?)

  Semantics component provide axioms that can be
   used in axiomatic proofs of programs that use the
   specified type 
   
:L06.3
EXAMPLE: ALGEBRAIC SPECIFICATION of QUEUE (Syntax)
 sorts: QUEUE, INT, BOOLEAN
 operations:
    new:               --> QUEUE
    add:   QUEUE x INT --> QUEUE
    del:   QUEUE       --> QUEUE
    head:  QUEUE       --> INT U { error }
    empty: QUEUE       --> BOOLEAN
:L06.3.1
EXAMPLE: ALGEBRAIC SPECIFICATION of QUEUE (Syntax)
 sorts: QUEUE, INT, BOOLEAN
 operations:
    new:               --> QUEUE
    add:   QUEUE x INT --> QUEUE
    del:   QUEUE       --> QUEUE
    head:  QUEUE       --> INT U { error }
    empty: QUEUE       --> BOOLEAN

EXAMPLE: ALGEBRAIC SPECIFICATION of STACK (Syntax)
 sorts: STACK, INT, BOOLEAN
 operations:
    new:               --> STACK
    push:  STACK x INT --> STACK
    pop:   STACK       --> STACK
    top:   STACK       --> INT U { error }
    empty: STACK       --> BOOLEAN
:L06.3.2
>.window[text 5 6 8 50]
>.titles[off]
Note that these two syntax specfications have
essentially the same form...

they differ in the name QUEUE becoming STACK,
 and the names of the operations being a bit
 different...


But, clearly, STACK and QUEUE are two very
different data types... 
STACK is LIFO, and QUEUE is FIFO, for example

This behavioral difference is captured not
in the syntax, but in the semantic component
of an algebraic specification.

?Back .window[text] L06.4

:L06.4
EXAMPLE: ALGEBRAIC SPECIFICATION of STACK (Semantics)

:L06.5
EXAMPLE: ALGEBRAIC SPECIFICATION of STACK (Semantics)











    new:               --> STACK       (operations)
    push:  STACK x INT --> STACK
    pop:   STACK       --> STACK
    top:   STACK       --> INT U { error }
    empty: STACK       --> BOOLEAN
:L06.6
EXAMPLE: ALGEBRAIC SPECIFICATION of STACK (Semantics)

    pop(new()) = new()
    pop(push(S,i)) = S








    new:               --> STACK       (operations)
    push:  STACK x INT --> STACK
    pop:   STACK       --> STACK
    top:   STACK       --> INT U { error }
    empty: STACK       --> BOOLEAN
:L06.7
EXAMPLE: ALGEBRAIC SPECIFICATION of STACK (Semantics)

    pop(new()) = new()
    pop(push(S,i)) = S

    top(new()) = error
    top(push(S,i)) = i





    new:               --> STACK       (operations)
    push:  STACK x INT --> STACK
    pop:   STACK       --> STACK
    top:   STACK       --> INT U { error }
    empty: STACK       --> BOOLEAN
:L06.8
EXAMPLE: ALGEBRAIC SPECIFICATION of STACK (Semantics)

    pop(new()) = new()
    pop(push(S,i)) = S

    top(new()) = error
    top(push(S,i)) = i

    empty(new()) = true
    empty(push(S,i)) = false


    new:               --> STACK       (operations)
    push:  STACK x INT --> STACK
    pop:   STACK       --> STACK
    top:   STACK       --> INT U { error }
    empty: STACK       --> BOOLEAN
:L06.8.0
>.window[text 5 5 9 52]
>.title[top left COMMENTS ON AXIOMS]
  no implementation implied here

  cannot get a feel for, say, how "push" affects 
   a stack by examining one, or a few, axioms.  

   In operational specs, you can.
?More .window[text] L06.8.0.1

:L06.8.0.1
EXAMPLE: ALGEBRAIC SPECIFICATION of STACK (Semantics)

    pop(new()) = new()
    pop(push(S,i)) = S

    top(new()) = error
    top(push(S,i)) = i

    empty(new()) = true
    empty(push(S,i)) = false


    new:               --> STACK       (operations)
    push:  STACK x INT --> STACK
    pop:   STACK       --> STACK
    top:   STACK       --> INT U { error }
    empty: STACK       --> BOOLEAN

:L06.8.1
>.window[text 5 5 9 52]
>.title[top left HOW DOES ONE KNOW WHEN TO STOP?]
  generator
   an operation of the specified type that is 
   necessary to construct any specific instance 
   of the type

  obviously, an operation that produces an 
   element of a sort other than the specified 
   type cannot be a generator
?More .window[text] L06.9

:L06.9
EXAMPLE: ALGEBRAIC SPECIFICATION of STACK (Semantics)

    pop(new()) = new()        
    pop(push(S,i)) = S       
                          
    top(new()) = error     
    top(push(S,i)) = i    
                       
    empty(new()) = true 
    empty(push(S,i)) = false 


    new:               --> STACK       (operations)
    push:  STACK x INT --> STACK
    pop:   STACK       --> STACK
  x top:   STACK       --> INT U { error }
  x empty: STACK       --> BOOLEAN
:L06.10.1
>.window[text 5 5 10 51]
>.title[top left new / push / pop ?]
"new" is obviously a generator, since it is the
only operation that creates an original STACK

(push(pop(push(push(new(),4),7)),3)
   produces the same stack instance as
(push(push(new(),4),3)

Any stack that can be built using "pop" can
also be built another way without "pop".


Concept: "canonical representation"

Consider the stack "3 4 (bottom)", that is, with
two elements, 3 on top and 4 on bottom...

(push(push(new(),4),3)    in canonical form

(push(pop(push(push(new(),4),7)),3)     not
?More .window[text] L06.11
:L06.11
EXAMPLE: ALGEBRAIC SPECIFICATION of STACK (Semantics)

    pop(new()) = new()        
    pop(push(S,i)) = S       
                          
    top(new()) = error     
    top(push(S,i)) = i    
                       
    empty(new()) = true 
    empty(push(S,i)) = false 


   new:               --> STACK       (operations)
   push:  STACK x INT --> STACK
  x pop:   STACK       --> STACK
  x top:   STACK       --> INT U { error }
  x empty: STACK       --> BOOLEAN
:L06.12
>.window[text 5 5 6 51]
>.title[top left AXIOM CONSTRUCTION HUERISTIC]
Once generators have been identified,

  enumerate left-hand-sides for axioms by 
   all combinations of a non-generator applied 
   to the result of a generator


  examine each left-hand-side so produced and
   construct a right-hand-side that describes an
   equivalent, but differently stated, structure.



  each axiom is an equation... LHS = RHS
   thus axioms are rewrite rules... 
   tell how to take a sequence of operations from 
   the algebra and transform to new (shorter,
   simpler) sequence.
?More .window[text] L06.13

:L06.13
EXAMPLE: ALGEBRAIC SPECIFICATION of STACK (Semantics)

    pop(new()) = new()        |
    pop(push(S,i)) = S        | see how these
                              | axioms were generated
    top(new()) = error        | by the hueristic
    top(push(S,i)) = i        |
                              | 
    empty(new()) = true       |
    empty(push(S,i)) = false  |


   new:               --> STACK       (operations)
   push:  STACK x INT --> STACK
  x pop:   STACK       --> STACK
  x top:   STACK       --> INT U { error }
  x empty: STACK       --> BOOLEAN
:L06.14
ANOTHER EXAMPLE: SET of INT
:L06.15
ANOTHER EXAMPLE: SET of INT

 sorts: SET, INT, BOOLEAN
:L06.16
ANOTHER EXAMPLE: SET of INT

 sorts: SET, INT, BOOLEAN
 operations:
     empty:            --> SET
     insert: SET x INT --> SET
     delete: SET x INT --> SET
     member: SET x INT --> BOOLEAN
:L06.17
ANOTHER EXAMPLE: SET of INT

 sorts: SET, INT, BOOLEAN
 operations:
    empty:            --> SET
    insert: SET x INT --> SET
   x delete: SET x INT --> SET
   x member: SET x INT --> BOOLEAN
:L06.18
ANOTHER EXAMPLE: SET of INT

 sorts: SET, INT, BOOLEAN
 operations:
    empty:            --> SET
    insert: SET x INT --> SET
   x delete: SET x INT --> SET
   x member: SET x INT --> BOOLEAN
 axioms
   member(empty(),j)
   member(insert(S,j),k)
:L06.19
ANOTHER EXAMPLE: SET of INT

 sorts: SET, INT, BOOLEAN
 operations:
    empty:            --> SET
    insert: SET x INT --> SET
   x delete: SET x INT --> SET
   x member: SET x INT --> BOOLEAN
 axioms
   member(empty(),j)
   member(insert(S,j),k)
   
   delete(empty(),j)
   delete(insert(S,j),k)
:L06.20
ANOTHER EXAMPLE: SET of INT

 sorts: SET, INT, BOOLEAN
 operations:
    empty:            --> SET
    insert: SET x INT --> SET
   x delete: SET x INT --> SET
   x member: SET x INT --> BOOLEAN
 axioms
   member(empty(),j) = false
   member(insert(S,j),k) 
   
   delete(empty(),j)
   delete(insert(S,j),k)
:L06.21
ANOTHER EXAMPLE: SET of INT

 sorts: SET, INT, BOOLEAN
 operations:
    empty:            --> SET
    insert: SET x INT --> SET
   x delete: SET x INT --> SET
   x member: SET x INT --> BOOLEAN
 axioms
   member(empty(),j) = false
   member(insert(S,j),k) = 
     if (j=k) then true else member(S,k)
   delete(empty(),j)
   delete(insert(S,j),k)
:L06.22
ANOTHER EXAMPLE: SET of INT

 sorts: SET, INT, BOOLEAN
 operations:
    empty:            --> SET
    insert: SET x INT --> SET
   x delete: SET x INT --> SET
   x member: SET x INT --> BOOLEAN
 axioms
   member(empty(),j) = false
   member(insert(S,j),k) = 
     if (j=k) then true else member(S,k)
   delete(empty(),j) = empty()
   delete(insert(S,j),k)
:L06.23
ANOTHER EXAMPLE: SET of INT

 sorts: SET, INT, BOOLEAN
 operations:
    empty:            --> SET
    insert: SET x INT --> SET
   x delete: SET x INT --> SET
   x member: SET x INT --> BOOLEAN
 axioms
   member(empty(),j) = false
   member(insert(S,j),k) = 
     if (j=k) then true else member(S,k)
   delete(empty(),j) = empty()
   delete(insert(S,j),k) =
     if (j=k) then delete(S,j) 
              else insert(delete(S,k),j)
:L06.n
>Key=A
END OF LECTURE L06

?Again L06
?Course 
?"Next Lecture" L07

:L07
>Key=L
L07: Verification of Abstract Data Types

  OVERVIEW

     more examples: BAG and INT
     equality of type instances
     consistency and completeness
     data type induction
     what is an implementation?
     verifying an implementation
     example: algebra/implementation of STACK

  ASSIGNMENT: A7*

?Course 
?Lecture L07.1
?"Next Lecture" L08

:L07.1
ANOTHER ALGEBRA: type BAG (multiset)

sorts: BAG, INT, BOOLEAN
operations:
   empty:            --> BAG
   insert: BAG x INT --> BAG
   delete: BAG x INT --> BAG
   member: BAG x INT --> BOOLEAN

:L07.1.1
ANOTHER ALGEBRA: type BAG (multiset)

sorts: BAG, INT, BOOLEAN
operations:
  empty:            --> BAG
  insert: BAG x INT --> BAG
 x delete: BAG x INT --> BAG
 x member: BAG x INT --> BOOLEAN

:L07.2
ANOTHER ALGEBRA: type BAG (multiset)

sorts: BAG, INT, BOOLEAN
operations:
  empty:            --> BAG
  insert: BAG x INT --> BAG
 x delete: BAG x INT --> BAG
 x member: BAG x INT --> BOOLEAN

axioms
  member(empty(),i)
  member(insert(B,i),j)

  delete(empty(),i)
  delete(insert(B,i),j)
:L07.3
ANOTHER ALGEBRA: type BAG (multiset)

sorts: BAG, INT, BOOLEAN
operations:
  empty:            --> BAG
  insert: BAG x INT --> BAG
 x delete: BAG x INT --> BAG
 x member: BAG x INT --> BOOLEAN

axioms
  member(empty(),i) = false
  member(insert(B,i),j) = if (i=j) then true  
                          else member(B,j) 
  delete(empty(),i) = empty()
  delete(insert(B,i),j) = if (i=j) then B  
                          else insert(delete(B,j),i)
:L07.4
>.window[text 4 6 10 48]
>.titles[off]
The essential difference between SET and BAG is
captured in the "delete(insert ... )" axiom.

delete an item after inserting that item always
returns the original BAG... not necessarily so
for SET.
?Continue  .window[text] L07.5

:L07.5
ANOTHER EXAMPLE: type INT
 sorts: INT, BOOLEAN
 operations:
    zero:            --> INT
    succ:  INT       --> INT
    add:   INT x INT --> INT
    equal: INT x INT --> BOOLEAN
:L07.5.0
>.window[text 7 6 10 50]
>.title[top left CANONICAL FORM]
We will use Church's representation for 
integers, that is, every integer K is obtained 
by taking the Kth successor of the zero element.

Our operation "zero()" creates the zero element
for our algebra: 0 = zero().

example: the integer 4 is represented as
  3 = succ( succ( succ( zero() ) ) )
?More .window[text] L07.5.0.1
:L07.5.0.1
ANOTHER EXAMPLE: type INT
 sorts: INT, BOOLEAN
 operations:
   zero:            --> INT
   succ:  INT       --> INT
  x add:   INT x INT --> INT
  x equal: INT x INT --> BOOLEAN
:L07.5.1
>.window[text 12 6 5 50]
>.title[top left MORE ON THE AXIOM HUERISTIC]
In earlier examples we created one axiom for 
every combination of a non-generator applied 
to a generator.

Now we see that sometimes each combination may 
create several axioms... it depends on how many
arguments of the same type occurr in the
operations...
?Continue .window[text] L07.6

:L07.6
ANOTHER EXAMPLE: type INT
 sorts: INT, BOOLEAN
 operations:
   zero:            --> INT
   succ:  INT       --> INT
  x add:   INT x INT --> INT
  x equal: INT x INT --> BOOLEAN
:L07.7
ANOTHER EXAMPLE: type INT
 sorts: INT, BOOLEAN
 operations:
   zero:            --> INT
   succ:  INT       --> INT
  x add:   INT x INT --> INT
  x equal: INT x INT --> BOOLEAN
 axioms
   add(zero(),zero()) 
   add(succ(n),zero())
   add(zero(),succ(n))
   add(succ(n),succ(m))

   equal(zero(),zero()) 
   equal(succ(n),zero())
   equal(zero(),succ(n))
   equal(succ(n),succ(m))
:L07.8
ANOTHER EXAMPLE: type INT
 sorts: INT, BOOLEAN
 operations:
   zero:            --> INT
   succ:  INT       --> INT
  x add:   INT x INT --> INT
  x equal: INT x INT --> BOOLEAN
 axioms
   add(zero(),zero()) = zero()
   add(succ(n),zero()) = succ(n)
   add(zero(),succ(n)) = succ(n)
   add(succ(n),succ(m)) = succ(succ(add(n,m))

   equal(zero(),zero()) = true
   equal(succ(n),zero()) = false
   equal(zero(),succ(n)) = false
   equal(succ(n),succ(m)) = equal(n,m)
:L07.9
DATA TYPE INDUCTION

  use to prove that some property P holds for 
   every element of some type T.

  similar technique to mathematical induction

  take operations that map to the type, and
   separate them into 
     a) those that have no arguments of type T
     b) those that do have arguments of type T

  will show our goal by showing that every element
   of T has property P when it is first created 
   (point (a) above) and that every time it is 
   transformed (point (b) above) it retains the 
   property P...

:L07.10
DATA TYPE INDUCTION (continued)

  basis: show P holds for the result of each 
   operation that maps to type T but needs no args 
   of type T

  induction: show for each other operation mapping 
   to type T that if P holds for the args of type T, 
   then it also holds for the result.

  Example: STACK
    basis: 
      show P(new())
    induction:
      show P(S) ==> P(push(S,i))  for arbitrary i
      show P(S) ==> P(pop(S))

:L07.11
>.window[text 3 5 8 51]
>.title[top left NORMAL FORM LEMMA]
  can use our canonical (normal) form to 
   ease these proofs..

   If we have proven a normal form lemma 
   (used informally up to now) we can do the 
   DT Induction for generators only, instead of 
   for all operations mapping to the type.


  STACK: normal form lemma is

   forall S in STACK, either 
     S = new()  or
     S = push(...(push(new(),e1)...),en)

?More .window[text] L07.12
:L07.12
DATA TYPE INDUCTION (continued)

  basis: show P holds for the result of each 
   operation that maps to type T but needs no args 
   of type T

  induction: show for each other operation mapping 
   to type T that if P holds for the args of type T, 
   then it also holds for the result.

  Example: STACK 
    basis: 
      show P(new())
    induction:
      show P(S) ==> P(push(S,i))  for arbitrary i
     show P(S) ==> P(pop(S))
:L07.13
DATA TYPE INDUCTION (continued)

  basis: show P holds for the result of each 
   operation that maps to type T but needs no args 
   of type T

  induction: show for each other operation mapping 
   to type T that if P holds for the args of type T, 
   then it also holds for the result.

  Example: STACK (normal form)
    basis: 
      show P(new())
    induction:
      show P(S) ==> P(push(S,i))  for arbitrary i

:L07.14
EXAMPLE DATA TYPE INDUCTION

UDIR: UNIX Directory
sorts: UDIR, INT, ID, BOOLEAN
operations: 
   /:                 --> UDIR
   mkdir:  UDIR x ID  --> UDIR
   cd:     UDIR x ID  --> UDIR
   pwd:    UDIR       --> ID
   up:     UDIR x INT --> ID
   isName: ID         --> BOOLEAN
:L07.15
>.window[text 11 5 7 51]
>.title[top left CANONICAL FORM]
For UDIR, the generators are /, mkdir, cd.

/ makes the root of a directory tree.
mkdir hangs subtrees off a directory.
cd changes the current location.


The operation "isName" is auxiliary, that
is, it will be used in the axioms, but is
not a visible operation of the type.

operation: 
  isName("..") = false, otherwise true

  this allows ".." to be a special ID

  we will use ".." to mean "parent"

?More .window[text] L07.16

:L07.16
UDIR: UNIX Directory
 sorts: UDIR, INT, ID, BOOLEAN
 operations: 
   /:                 --> UDIR
   mkdir:  UDIR x ID  --> UDIR
   cd:     UDIR x ID  --> UDIR
  x pwd:    UDIR       --> ID
  x up:     UDIR x INT --> ID
  * isName: ID         --> BOOLEAN


=================================================================

Verifying implementations of Algebraic Specs

  OVERVIEW

     Example: Unix DIrectory UDIR
     Data type induction
     verifying an implementation

  ASSIGNMENT: A8*

?Course 
?Lecture L08.1
?"Next Lecture" L09

:L08.1
UDIR: UNIX Directory
 sorts: UDIR, INT, ID, BOOLEAN
 operations: 
   /:                 --> UDIR
   mkdir:  UDIR x ID  --> UDIR
   cd:     UDIR x ID  --> UDIR
  x pwd:    UDIR       --> ID
  x up:     UDIR x INT --> ID
  * isName: ID         --> BOOLEAN

:L08.2
UDIR: UNIX Directory
 sorts: UDIR, INT, ID, BOOLEAN
 operations: 
   /:                 --> UDIR
   mkdir:  UDIR x ID  --> UDIR
   cd:     UDIR x ID  --> UDIR
  x pwd:    UDIR       --> ID
  x up:     UDIR x INT --> ID
  * isName: ID         --> BOOLEAN
 axioms
   pwd(/) = 
   pwd(mkdir(D,i) =
   pwd(cd(D,i)) =
   up(/,n) =
   up(mkdir(D,i),n) =
   up(cd(D,i),n) =
:L08.3
UDIR: UNIX Directory
 sorts: UDIR, INT, ID, BOOLEAN
 operations: 
   /:                 --> UDIR
   mkdir:  UDIR x ID  --> UDIR
   cd:     UDIR x ID  --> UDIR
  x pwd:    UDIR       --> ID
  x up:     UDIR x INT --> ID
  * isName: ID         --> BOOLEAN
 axioms
   pwd(/) = "/" 
   pwd(mkdir(D,i) = pwd(D)
   pwd(cd(D,i)) = if isName(i) then up(D,1) else i
   up(/,n) = "/"
   up(mkdir(D,i),n) = up(D,n)
   up(cd(D,i),n) = if isName(i) 
     then up(D,n-1) else up(D,n+1)