project: Stack

****************************************************
spec: /cse/grad/klin/obj3/stack.obj

relation:
   op _R_ : Stack Stack -> Bool .
   var I1 I2 : Nat .
   var A1 A2 : Arr .
   eq (s I1 || A1) R (s I2 || A2) =
          I2 == I1 and A1[I1] == A2[I1] and (I1 || A1) R (I1 || A2) .
   eq (0 || A1) R (0 || A2) = true .
[]

cobasis: {top, pop}

*****************************************************
proof: <<Lemma1>>
    goal: (forall X  Y : Nat)
            ((s Y) <= X  implies (exists Z : Nat)(X = s Z  and  Y <= Z )) .

by: induction on X by scheme {0,s} []

*****************************************************
proof: <<Lemma2>>
    goal: (forall X  Y : Nat) ( s X <= Y  implies  X <= Y  ) .

by: induction on X by scheme {0,s} []

*****************************************************
proof: <<PutAndBar>>
    goal: (forall I J N : Nat  A : Arr)
             (  I <= J   implies  (I || put(N,J,A)) R (I || A) ) .

by: induction on I by scheme {0,s} []

*****************************************************
proof: <<StackThm>>
  goal:  pop empty = empty  and 
   ((forall N I : Nat  A : Arr)  top push(N, I || A) = N  ) and
   ((forall N I : Nat  A : Arr)  pop push(N, I || A) = (I || A) ) .

by: coinduction []

****************************************************
display:
   title: "Lemma for Pointer Array Implementation of Stack"
   putdir: /net/cs/htdocs/groups/tatami/demos/array/lemma1

<<Lemma1>> 
   subtitle: "We prove a basic property about the order on natural number."
[]


***************************************************
display:
   title: "Lemma for Pointer Array Implementation of Stack"
   putdir: /net/cs/htdocs/groups/tatami/demos/array/lemma2

<<Lemma2>> 
   subtitle: "We prove a basic property about the order on natural number."
[]

***************************************************
display:
   title: "Key Lemma for Stack Implementation"
   putdir: /net/cs/htdocs/groups/tatami/demos/array/putandbar
   gethomepage:  /home/klin/he/putandbarhome.html


<<PutAndBar>> 
   subtitle: "We prove the key lemma for stack implementation."
[]

****************************************************
display:
   title: "Pointer Array Implementation of Stack "
   putdir: /net/cs/htdocs/groups/tatami/demos/array
   gethomepage: /home/klin/he/stackhome.html
   getspecexpl: /home/klin/he/stackspecexp.html

<<StackThm>>
   subtitle: "We show that array-with-pointer"+
             " implementation of stack is correct. "
   getexpl:  /home/klin/he/stackexp1.html   

   <<StackThm.1>>
   subtitle: "We prove <math>R</math> is <delta/>-congruence."
   getexpl:  /home/klin/he/stackexp2.html   

   <<StackThm.2>>
   subtitle: "We prove the main result."
   getexpl:  /home/klin/he/stackexp4.html   

[]