c
module main int)
{
    const MAX_CAPACITY: int = n;
    var s: array[0, MAX_CAPACITY) of int; // stack
    var top: int; // index of the top element

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

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

    function top_element() : int
        requires top >= 0;
    {
        return s[top];
    }

    procedure init()
    {
        top := -1;
    }

    procedure main()
    {
        havoc top;
        assume top >= -1;
        if top >= 0 {
            pop();
        } else {
            push(0);
        }
    }
}
