theory tut09 imports "HOL-IMP.Hoare_Sound_Complete" begin text \\ExerciseSheet{09}{16.12.2017}\ text \ \Exercise{Hoare Logic} In this exercise, you shall prove correct some Hoare triples. \ paragraph "Step 1" text \ 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''" paragraph "Step 2" text \Prove these lemmas about @{const max}:\ lemma [simp]: "(a::int) max a b = b" sorry lemma [simp]: "\(a::int) max a b = a" sorry text \Show that @{const "Max"} satisfies the following Hoare triple:\ lemma "\ {\s. True} Max {\s. s ''c'' = max (s ''a'') (s ''b'')}" sorry paragraph "Step 3" 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 \ undefined" paragraph "Step 4" text \ Prove that @{text "MUL"} does the right thing. \ lemma "\ {\s. 0 \ s ''y''} MUL {\s. s ''z'' = s ''x'' * s ''y''}" oops text \ \emph{Hints:} \<^item> You may want to use the lemma @{text "algebra_simps"}, containing some useful lemmas like distributivity. \<^item> 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 @{term "c\<^sub>1;; c\<^sub>2"}, you first continue the proof for @{term "c\<^sub>2"}, thus instantiating the intermediate assertion, and then do the proof for @{term "c\<^sub>1"}. However, the first premise of the @{text "Seq"}-rule is about @{text "c\<^sub>1"}. In an Isar proof, this is no problem. In an @{command apply}-style proof, the ordering matters. Hence, you may want to use the [@{attribute "rotated"}] attribute: \ lemmas Seq_bwd = Seq[rotated] lemmas hoare_rule[intro?] = Seq_bwd Assign Assign' If paragraph "Step 5" 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 @{const "Max"}: \ definition "MAX_wrong = (''a''::=N 0;;''b''::=N 0;;''c''::= N 0)" text \Prove that @{const "MAX_wrong"} also satisfies the specification for @{const "Max"}:\ lemma "\ {\s. True} MAX_wrong {\s. s ''c'' = max (s ''a'') (s ''b'')}" sorry text \What we really want to specify is, that @{const "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 @{const "Max"}: \ lemma "\ {\s. a=s ''a'' \ b=s ''b''} Max {\s. s ''c'' = max a b \ a = s ''a'' \ b = s ''b''}" sorry text \ The specification for @{const "MUL"} has the same problem. Fix it! \ text \ \Exercise{Forward Assignment Rule} Think up and prove correct a forward assignment rule, i.e., a rule of the form @{term "\ {P} x::=a {Q}"}, where @{term Q} is some suitable postcondition. Hint: To prove this rule, use the completeness property, and prove the rule semantically. \ lemma "\ {\s. True} Max {\s. s ''c'' = max (s ''a'') (s ''b'')}" sorry lemma "\ {\s. 0 \ s ''y''} MUL {\s. s ''z'' = s ''x'' * s ''y''}" sorry end