

module stack(n : int)
{
  var s : array[0..n-1] of int;
  var top : int;

  procedure top() returns (t: int)
  {
    assume(top >= 0);
    t := s[top];
  }

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

  procedure push(e: int)
  {
    assume(top < n);
    top := top + 1;
    s[top] := e;
  }

  init {
    top := -1;
  }
}

module main {
  const capacity : int = 5; // Example capacity of the stack

  instance stk : stack(capacity);

  // Example transitions
  stk.push(10);
  stk.push(20);
  stk.pop();
  stk.push(30);

  control {
    // Basic assertions
    assert(stk.top() == 30); // Check top element after operations
    assert(stk.top() != 20); // Ensure top element is not 20 after pop
  }
}
