Verification of Abstract Data Types
OVERVIEW
- more examples: BAG and INT
- equality of type instances
- consistency and completeness
- data type induction
(example)
- what is an implementation?
- verifying an implementation
- example: algebra/implementation of STACK
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
:L07.n
>Key=A
END OF LECTURE L07
?Again L07
?Course