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

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.

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.
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...

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
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

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)