Homework Assignment

Instructions:

1. Copy PVS source file N.pvs into your working directory.
2. Prove all the theorems.
3. Turn in all source (.pvs), proof (.prf) and status (.status) files.

Notes and Hints:

This assignment illustrates specification and implementation of non-inductive Abstract Data Type and issues arise in the underlying mathematics.

• Theory stacks_spec_1 is an abstract specification of stack. The stack_law_1 stack_law_2 and stack_law_3 are identities that any implementation of stacks_spec_1 must satisfy.

• Theory stacks_impl_1 represents abstract stacks with a record consisting of an array and a pointer to the next available slot for pushing an item. To prove that stacks_impl_1 implements stacks_spec_1, one must prove that each of the identities holds. In this case, at least one of the identities fails to hold, and your goal is to understand why.

• Theories stacks_impl_2 and stacks_impl_3 attempts to resolve the problems arising in stacks_impl_1. This will be discussed in class.
• N.pvs Introduces the PVS array and record constructs. You can read more about them in the PVS Language Reference [PDF]. Pay particular attention to with clauses.
• Arrays and records are represented by functions in the PVS logic. The rule for proving function equality is based on the Principle of Extensionality, which says, ``Two functions, f and g are provably equal if they give equal results for all possible arguments.'' That is,

  f = g  if  ∀x: f(x) = g(x)

  The Prover command (apply-extensionality n) instantiates this principle, if applicable, for sequent formula n.