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 []