Duck Source Code:
Pointer Array Implementation of Stack

```
project: Stack

****************************************************

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 [itex]R[/itex] is <delta/>-congruence."
getexpl:  /home/klin/he/stackexp2.html

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

[]
```

[Back]
This page was generated by Kumo on Wed Oct 13 18:03:25 PDT 1999.