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