Content
 Duck Script:   Array Implementation of Stack : Proof Web
```spec: 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: 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: array/lemma2

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

***************************************************
display:
title: "Key Lemma for Stack Implementation"
putdir: array/putandbar
gethomepage: putandbarhome.html

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

****************************************************
display:
title: "Pointer Array Implementation of Stack "
putdir: array
gethomepage: stackhome.html
getspecexpl: specexp.html

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

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

<<StackThm.2>>
subtitle: "We prove the main result."
getexpl:  stackexp3.html
[]

```

 The Specification of Array

```  obj DATA is
sort Nat .
op 0 : -> Nat .
op s_ : Nat -> Nat [prec 1] .
op _+_ : Nat Nat -> Nat [comm] .
op _<=_ : Nat Nat -> Bool .
var N M : Nat .
eq N + 0 = N .
eq N + s M = s(N + M) .
eq 0 <= N = true .
eq s N <= 0 = false .
eq s N <= s M = N <= M .
eq N <= N = true .
endo

th ARR is sort Arr .
pr  DATA .
op  nil : -> Arr .
op  put : Nat Nat Arr -> Arr .
op  _[_] : Arr Nat -> Nat .
var I J N : Nat .  var A : Arr .
eq  nil[I]  =  0 .
cq  put(N,I,A)[J] = N if I == J .
cq  put(N,I,A)[J] = A[J] if not I == J .
endth

bth PTR+ARR is
bsort Stack .
pr ARR .
op  _||_ : Nat Arr -> Stack [prec 10].
op  empty : -> Stack .
bop  push : Nat Stack -> Stack .
bop  top_ : Stack -> Nat .
bop  pop_ : Stack -> Stack .
var I N : Nat .  var A : Arr .
eq  empty  =  0 || nil .
eq  push(N, I || A )  = s I || put(N,I,A) .
eq  top s I || A  =  A[I] .
eq  top 0 || A  =  0 .
eq  pop s I || A  =  I || A .
eq  pop 0 || A  =  0 || A .
endb
```