Implementing a stack

Oct 20, 2014 at 1:15 PM
Hello,

I'm still learning Boogie and I'm hitting another brick wall. I'm trying to implement a generic stack that can store objects of heterogeneous types.

I tried to write a class with the methods peak, push and pop following what is the done for the heap in the Boogie 2 documentation (section 5).

Here is my (probably lame) attempt:
type Ref;
type Field t;
type StackType t = [Ref, Field t]t;

const unique C.data: <t>[Field e]t;
const unique C.next: Field Ref;

function C.peak(this: <t>[StackType t]t) returns(<t>[Field t]t)
requires stack != null;
{C.data}

procedure C.push(this: <t>[StackType t]t, e : <t>[Field t]t) returns(res: bool)
  modifies this;
  ensures (C.data == e && C.next == old(this));
{res:=true;}

procedure C.pop(this: <t>[StackType t]t) returns(res: <t>[Field t]t)
  requires stack != null;
  modifies this;
  ensures (forall o:Ref, f: <t>[Field t]t :: old(this)[o,f] && C.data == f && C.next == o);
{res:= C.data}

procedure main(stack : StackType) returns (res: bool)
  requires stack == null;
{
  stack.push(7);
  
  assert stack != null; 
  assert 7 == stack.pop();
  assert stack == null;
  
  res:= true;
}
This code does not compile. Am I going in the right direction?

Thanks a lot for your help.
Oct 22, 2014 at 9:21 AM
I've made some progress but still not there yet. I've defined empty and push as functions (constructors). Now, the problem is pop, a procedure that will return the top element of the stack and modifies the stack.

In my code here:

http://rise4fun.com/Boogie/D9gx

neither the stack is modified nor the correct value is returned. Any idea about what can be the problem?

Thanks a lot.