(*<*) theory ex09 imports Hoare Vars begin (*>*) text {* \ExerciseSheet{9}{11.~12.~2012} *} (* Short repetition of Hoare-Logic *) thm Skip -- "Does nothing" thm Assign -- "P must hold for new value already before assignment" thm If -- "Show triple for both branches, assuming that branch has been taken" thm Seq -- "Transitivity. Provide intermediate assertion Q" thm While -- "Provide invariant P, that holds initially and is preserved by body of loop." thm conseq -- "Strengthen precondition, weaken postcondition" text {* \Exercise{Hoare Logic} In this exercise, you shall prove correct some Hoare triples. First, write a program that stores the maximum of the values of variables @{text "a"} and @{text "b"} in variable @{text "c"}. *} definition MAX :: com where "MAX \ IF (Less (V ''a'') (V ''b'')) THEN ''c''::=V ''b'' ELSE ''c''::=V ''a'' " text {* For the next task, you will need the following lemmas. Hint: Sledgehammering may be a good idea. *} lemma max1[simp]: "(a::int) max a b = b" (*<*)by (metis order_less_imp_le sup_absorb2 sup_int_def)(*>*) lemma max2[simp]: "\(a::int) max a b = a" (*<*)by (metis leI min_max.sup_absorb1)(*>*) text {* Show that @{text "MAX"} satisfies the following Hoare-triple: *} lemma "\ {\s. True} MAX {\s. s ''c'' = max (s ''a'') (s ''b'')}" unfolding MAX_def apply (rule If) (* Assign does not match precondition here. So we have to use a consequence rule *) apply (rule strengthen_pre) prefer 2 apply (rule Assign) apply simp apply (rule Assign') (* Assign' is a shortcut for Assign + strengthen_pre, and leaves the subgoals in the right order, so you don't need prefer.*) apply simp done lemma "\ {\s. True} MAX {\s. s ''c'' = max (s ''a'') (s ''b'')}" unfolding MAX_def apply (rule If) apply (rule Assign') apply simp apply (rule Assign') apply simp done (* Automatic. Just apply matching rules *) lemma "\ {\s. True} MAX {\s. s ''c'' = max (s ''a'') (s ''b'')}" unfolding MAX_def by (rule If Assign' | simp)+ text {* Now define a program @{text "MUL"} that returns the product of @{text "x"} and @{text "y"} in variable @{text "z"}. You may assume that @{text "y"} is not negative. *} definition MUL :: com where "MUL \ ''z'' ::= N 0; ''c'' ::= V ''y''; WHILE Less (N 0) (V ''c'') DO ( ''z'' ::= Plus (V ''z'') (V ''x''); ''c'' ::= Plus (V ''c'') (N -1) ) " values "{map t [''z''] |t. (MUL, <''x'' := 20, ''y'' := 2>) \ t}" lemmas Seq_bwd = Seq[rotated] -- "It's better to prove with the second command of a sequential composition first. The Seq_bwd rule leaves you with the right order of subgoals, so that no prefer 2 is required" lemma "\ {\s. 0 \ s ''y''} MUL {\s. s ''z'' = s ''x'' * s ''y''}" unfolding MUL_def apply (rule Seq_bwd) apply (rule While'[where P = "\s. s ''z'' = s ''x'' * (s ''y'' - s ''c'') \ s ''c'' \ 0"]) apply (rule Seq_bwd) apply (rule Assign) -- "Be careful: If the Assign-rule matches, you have to apply it instead of Assign', otherwise you'll be left with a schematic goal that's more tedious to prove" apply (rule Assign') apply (fastforce simp add: algebra_simps) apply (fastforce simp add: algebra_simps) apply (rule Seq_bwd) apply (rule Assign) apply (rule Assign') apply (fastforce simp add: algebra_simps) done text {* Lessons learned from the above proof: Try the hoare rules in the following order: *} lemmas hoare = Skip If Seq_bwd Assign Assign' text {* So we arrive at a mostly automatic proof. You only have to come up with the loop invariant : *} lemma "\ {\s. 0 \ s ''y''} MUL {\s. s ''z'' = s ''x'' * s ''y''}" unfolding MUL_def apply (rule hoare While'[where P = "\s. s ''z'' = s ''x'' * (s ''y'' - s ''c'') \ s ''c'' \ 0"] | fastforce simp add: algebra_simps )+ done text {* Note that our specifications still have a problem, as programs are allowed to overwrite arbitrary variables. For example, regard the following (wrong) implementation of @{text "MAX"}: *} definition "MAX_wrong \ ''a''::=N 0; ''b''::=N 0; ''c''::=N 0" text {* Prove that @{text "MAX_wrong"} also satisfies the specification for @{text "MAX"}: *} lemma "\ {\s. True} MAX_wrong {\s. s ''c'' = max (s ''a'') (s ''b'')}" unfolding MAX_wrong_def apply (rule hoare | simp) + done lemma "\ {\s. a=s ''a'' \ b=s ''b''} MAX {\s. s ''c'' = max a b \ a = s ''a'' \ b = s ''b''}" unfolding MAX_def apply (rule hoare | simp) + done text {* The specification for @{text "MUL"} has the same problem. Fix it! *} definition "MUL_wrong \ ''z''::=N 0; ''x''::=N 0" lemma "\ {\s. 0 \ s ''y''} MUL_wrong {\s. s ''z'' = s ''x'' * s ''y''}" unfolding MUL_wrong_def apply (rule hoare | simp) + done lemma "\ {\s. 0 \ s ''y'' \ x = s ''x'' \ y = s ''y''} MUL {\s. s ''z'' = x*y \ x = s ''x'' \ y = s ''y''}" unfolding MUL_def (* We have to add to the invariant that x and y are not changed! *) apply (rule hoare While'[where P = "\s. s ''z'' = s ''x'' * (s ''y'' - s ''c'') \ s ''c'' \ 0 \ x = s ''x'' \ y = s ''y'' "] | fastforce simp add: algebra_simps )+ done end