# 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]
 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)

```