(*<*) theory sol10_1 imports "~~/src/HOL/IMP/Hoare" begin (*>*) text {* \ExerciseSheet{9}{17.~12.~2013} *} 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 [simp]: "(a::int) max a b = b" (*<*)by (metis order_less_imp_le sup_absorb2 sup_int_def)(*>*) lemma [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) apply (rule Assign') apply simp apply (rule Assign') apply simp done (*>*) (*<*) (* More automatic proof *) lemma "\ {\s. True} MAX {\s. s ''c'' = max (s ''a'') (s ''b'')}" unfolding MAX_def by (rule Seq[rotated] Assign Assign' If | simp add: algebra_simps)+ (*>*) 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''::=N 0;; WHILE (Less (V ''c'') (V ''y'')) DO ( ''z''::=Plus (V ''z'') (V ''x'');; ''c''::=Plus (V ''c'') (N 1))" (*>*) text {* Prove that @{text "MUL"} does the right thing. *} lemma "\ {\s. 0 \ s ''y''} MUL {\s. s ''z'' = s ''x'' * s ''y''}" (*<*)oops(*>*) text {* \paragraph{Hints} You may want to use the lemma @{text "algebra_simps"}, that contains some useful lemmas like distributivity. Note that we use a backward assignment rule. This implies that the best way to do proofs is also backwards, i.e., on a semicolon @{text "S\<^sub>1; S\<^sub>2"}, you first continue the proof for @{text "S\<^sub>2"}, thus instantiating the intermediate assertion, and then do the proof for @{text "S\<^sub>1"}. However, the first premise of the @{text "Seq"}-rule is about @{text "S\<^sub>1"}. Hence, you may want to use the @{text "rotated"}-attribute, that rotates the premises of a lemma: *} lemmas Seq_bwd = Seq[rotated] lemmas hoare_rule[intro?] = Seq_bwd Assign Assign' If (*<*) 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 ''c'' \ s ''c'' \ s ''y''"]) apply simp apply (rule Seq_bwd) apply (rule Assign) apply (rule Assign') apply (simp add: algebra_simps) apply simp apply (rule Seq_bwd) apply (rule Assign) apply (rule Assign') apply simp done (*>*) (*<*) (* More automatic proof *) lemma "\ {\s. 0 \ s ''y''} MUL {\s. s ''z'' = s ''x'' * s ''y''}" unfolding MUL_def by (rule hoare_rule While'[where P="\s. s ''z'' = s ''x'' * s ''c'' \ s ''c'' \ s ''y''"] | simp add: algebra_simps)+ (*>*) 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 by (rule hoare_rule | simp add: algebra_simps)+ (*>*) text {* What we really want to specify is, that @{text "MAX"} computes the maximum of the values of @{text "a"} and @{text "b"} in the initial state. Moreover, we may require that @{text "a"} and @{text "b"} are not changed. For this, we can use logical variables in the specification. Prove the following more accurate specification for @{text "MAX"}: *} lemma "\ {\s. a=s ''a'' \ b=s ''b''} MAX {\s. s ''c'' = max a b \ a = s ''a'' \ b = s ''b''}" (*<*) unfolding MAX_def by (rule hoare_rule | simp add: algebra_simps)+ (*>*) 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 by (rule hoare_rule | simp add: algebra_simps)+ 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 by (rule hoare_rule While'[where P="\s. s ''z'' = x * s ''c'' \ s ''c'' \ y \ x = s ''x'' \ y = s ''y'' "] | simp add: algebra_simps)+ (*>*) (*<*) end (*>*)