(*<*)
theory tmpl_10hw
imports
"~~/src/HOL/IMP/Hoare"
"~~/src/HOL/IMP/Small_Step"
"~~/src/HOL/IMP/Star"
begin
(*>*)
text \
\NumHomework{Floyd's Method for Program Verification}{Dec 22}
A flow graph is a directed graph with labeled edges.
Labels come with an enabled predicate and an effect function.
The enabled predicate checks whether a label is enabled in a state,
and the effect function applies the effect of a label to a state.
The following formalizes this setting:
\
type_synonym ('n,'l) flowgraph = "'n \ 'l \ 'n \ bool"
locale flowgraph =
fixes G :: "('n,'l) flowgraph"
fixes enabled :: "'l \ 's \ bool"
fixes effect :: "'l \ 's \ 's"
begin
text \Define a small-step semantics on flow graphs:
Configurations are pairs of nodes and states. A step is induced
by an enabled edge, and applies the effect of the edge to the state.
\
inductive step :: "('n\'s) \ ('n\'s) \ bool"
(* YOU: Add def *)
text \We form the reflexive transitive closure over our small-step semantics: \
abbreviation "steps \ star step"
text \The idea of Floyd's method is to annotate an invariant over states
to each node in the flow graph, and show that the invariant is preserved
by the edges: \
context
fixes I :: "'n \ ('s \ bool)"
assumes preserve: "\ I n s; G n l n'; enabled l s \ \ I n' (effect l s)"
begin
text \Show that the invariant is preserved by multiple steps: \
lemma preserves:
assumes "I n s"
assumes "steps (n,s) (n',s')"
shows "I n' s'"
oops (* YOU! *)
end
end
text \Now, let's instantiate the flow graph framework for IMP-programs.
Edges are labeled by conditions, assignments, or skip.\
datatype label = Assign vname aexp | Cond bexp | Skip
text \Define the enabled and effect functions for edges: \
fun enabled :: "label \ state \ bool"
where "enabled l s = undefined" (* YOU! *)
fun effect :: "label \ state \ state"
where "effect l s = undefined" (* YOU! *)
text \For nodes, we use commands. Similar to the small-step semantics,
a node indicates the command that still has to be executed.
Define the flow graph for IMP programs. We give you the case for
assignment and if-false here, you have to define the other
cases. Make sure that you use the same intermediate steps as
@{const small_step} does, this will simplify the next proof:
\
inductive cfg :: "com \ label \ com \ bool"
where
"cfg (x::=a) (Assign x a) SKIP"
| "cfg (IF b THEN c1 ELSE c2) (Cond (Not b)) c2"
(* YOU: Add other rules *)
text \The following instantiates the flow graph framework:\
interpretation flowgraph cfg enabled effect .
term step term steps
text \Show that execution of flow graphs and the small-step semantics
coincide:\
lemma steps_eq: "cs \* cs' \ steps cs cs'" oops (* YOU! *)
text \Combine your results to prove the following theorem, which allows
you to prove correctness of programs with Floyd's method.
(Hint: Big and small-step semantics are equivalent!)\
lemma floyd:
assumes PRE: "\s. P s \ I c s"
assumes PRES: "\n s c l c'. \cfg c l c'; I c s; enabled l s \ \ I c' (effect l s)"
assumes POST: "\s. I SKIP s \ Q s"
shows "\ {P} c {Q}"
oops (* YOU! *)
text \
\NumHomework{Application of Floyd's Method}{Dec 22}
{\bf 5 bonus points, quite hard}
Apply Floyd's method to verify the following program:
\
definition "P \
''r''::= N 0;;
WHILE (Less (N 0) (V ''x'')) DO (
''r'' ::= Plus (N 2) (V ''r'');;
''x'' ::= Plus (N (-1)) (V ''x'')
)"
lemma "\ { \s. s ''x'' = x \ x \ 0 } P {\s. s ''r'' = 2*x}"
oops (* YOU! *)
(*<*)
end
(*>*)