module StackModule {
  var capacity: integer;
  var operation: enum { POP, PUSH, TOP };
  var s: [integer]integer;
  var top_value: integer;
  var stack_size: integer;

  next {
    if ((operation == PUSH) && (stack_size < capacity)) {
      s' = s[stack_size -> top_value];
      stack_size' = (stack_size + 1);
    } else {
      if ((operation == POP) && (stack_size > 0)) {
        stack_size' = (stack_size - 1);
      } else {
        if ((operation == TOP) && (stack_size > 0)) {
          top_value' = s[(stack_size - 1)];
        }
      }
    }

  }
  invariant spec: (stack_size <= capacity);

}
