type T = int // to allow doing new T[cap], but can be other type

class {:autocontracts} Stack
{
    var elems: array<T>;
    var size : nat; // used size

    constructor (cap: nat)
        ensures elems.Length == cap
        ensures size == 0
    {
        elems := new T[cap];
        size := 0;
    }

    predicate method isEmpty()
        reads this
    {
        size == 0
    }

    predicate method isFull()
        reads this
    {
        size == elems.Length
    }

    method push(x : T)
        modifies this, elems
        requires size < elems.Length
        ensures top() == x
        ensures size == old(size) + 1
        ensures forall i :: 0 <= i < size - 1 ==> elems[i] == old(elems)[i]
    {
        elems[size] := x;
        size := size + 1;
    }

    function method top(): T
        reads this, elems
        requires size > 0
    {
        elems[size - 1]
    }

    method pop()
        modifies this
        requires size > 0
        ensures size == old(size) - 1
    {
        size := size - 1;
    }

    predicate Valid()
        reads this
    {
        size <= elems.Length
    }
}

// A simple test case to check on the console.
method {:verify false} Main()
{
    var s := new Stack(3);
    s.push(1);
    s.push(2);
    s.push(3);
    s.pop();
    var x := s.top();
    print "top=", x, " (should be 2)\n";
}