Algebraic Specifications and Abstract Data Types

OVERVIEW



WHAT ARE ALGEBRAIC SPECS?

USER-DEFINED TYPES

ALGEBRAIC SPECS and AXIOMATIC VERIFICATION

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

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 (axioms) of an algebraic specification.

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)