module main {
  type stack_t = [int] int; // Define stack type as an array from int to int
  const capacity : int;     // Define the capacity of the stack
  var s : stack_t;          // Stack variable
  var top_index : int;      // Index of the top element in the stack

  // Initialize the stack
  init {
    top_index = 0;          // Start with an empty stack
  }

  // Procedure to push an element onto the stack
  procedure push(elem : int)
    modifies s, top_index;
  {
    if (top_index < capacity) {
      s[top_index] := elem;
      top_index := top_index + 1;
    }
  }

  // Procedure to pop the top element from the stack
  procedure pop()
    modifies top_index;
  {
    if (top_index > 0) {
      top_index := top_index - 1;
    }
  }

  // Function to get the top element of the stack
  function top() returns (int)
  {
    if (top_index > 0) {
      return s[top_index - 1];
    } else {
      return -1; // Return -1 if the stack is empty
    }
  }

  // Main control block
  control {
    // Initialize the stack capacity (e.g., capacity of 5)
    set(capacity, 5);

    // Initialize the system
    init;

    // Perform some operations
    call push(3);
    call push(5);
    call push(7);
    assert top() == 7;
    call pop();
    assert top() == 5;

    // Check properties
    check;
    print_results;
  }
}
