(*<*) 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 (*>*)