
module main int)
{
    const capacity : int = n;
    type stack_t = record {
        top : int;
        elements : array[int] of int;
    };

    var s : stack_t;

    procedure push(val: int)
        requires s.top < capacity;
        modifies s;
    {
        s.elements[s.top] := val;
        s.top := s.top + 1;
    }

    procedure pop()
        requires s.top > 0;
        modifies s;
    {
        s.top := s.top - 1;
    }

    function top() : int
        requires s.top > 0;
    {
        return s.elements[s.top - 1];
    }

    procedure init()
    {
        s.top := 0;
        havoc s.elements;
    }

    procedure print_stack()
    {
        var i : int;
        for i := 0 to s.top - 1 do
            print("Element at index ", i, " is ", s.elements[i]);
    }
}
