Verification of Abstract Data Types

OVERVIEW



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