ProgramAnalysis hints
A few hints to help you if you get stuck on certain problems in lab 1.
Beware! Don't read further if you don't want spoilers!
Hint: Definition of validate
Our solution defines validate
as a function of validate'
, and validate' takes an additional flag indicating whether the state on which `p
will be run is nonzero.
Definition validate p := validate' p false.
Fixpoint validate' (p : Prog) (nz : bool) : bool.
Admitted.
In other words, if nz = true
, then validate'
can oeprate under the assumption that p
will only be run with nonzero states. When calling validate'
recursively, make sure
to pass an nz
that corresponds to the state after the current operation.
Hint: Arithmetic lemmas
Some lemmas about arithmetic on natural numbers are necessary to prove the
soundness of this validator. Some of them can be proven inline using lia
.
The rest that we needed we found from the standard library by using Search
.
Hint: Soundness of validate
To prove soundness of validate'
from hint 1, it makes sense to do
induction on the input program. The key to choosing the predicate P
is to relate the nz
indicator to the state of a program during a
hypothetical execution of the program.
Hint: Soundness of validate
(more details)
To prove soundness of validate'
by induction on the program and
develop a workable P
, consider the two cases in executing validate'
separately. Split the soundness of validate'
into the case where
the indicator passed into validate'
is true and in the case where it is false.
Hint: Soundness of validate
(spoiler)
To prove soundness of validate'
by induction on the program, one workable P
is
forall p,
(validate' p true = true ->
forall s, s <> 0 -> runPortable p s = (true, run p s)) /\
(validate' p false = true ->
forall s, runPortable p s = (true, run p s)).