
module main int)
{
    const capacity : int = n;
    type stack_t = record {
        arr : array [0, capacity-1] of int;
        top : int;
    };

    var s : stack_t;

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

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

    procedure top() : int
    {
        assume(s.top > 0);
        return s.arr[s.top - 1];
    }
}
