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)