Implementing a stack

Oct 20, 2014 at 1:15 PM

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 <t>[Field e]t;
const unique Field Ref;

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

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

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] && == f && == o);

procedure main(stack : StackType) returns (res: bool)
  requires stack == null;
  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:

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

Thanks a lot.