Homework Assignment
Instructions:
-
Copy PVS source file
N.pvs
into your working directory.
-
Prove all the theorems.
- 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.