(*<*) theory ex11 imports VC HoareT begin (*>*) text {* \ExerciseSheet{11}{13.~01.~2012} *} text {* \Exercise{Using the VCG, Total correctness} For each of the three programs given here, you must prove partial correctness and total correctness. For the partial correctness proofs, you should first write an annotated program, and then use the verification condition generator from @{text "VC.thy"}. For the total correctness proofs, use the Hoare rules from @{text "HoareT.thy"}. *} (*<*) definition MAX::acom where "MAX = ( IF (Less (V ''0'') (V ''1'')) THEN ''2'' ::= V ''1'' ELSE ''2'' ::= V ''0'')" lemma "\ {\_. True} strip MAX {\s. s ''2'' = max (s ''0'') (s ''1'')}" apply (rule vc_sound') unfolding MAX_def by auto (*>*) text {* A convenient loop construct: *} abbreviation For :: "vname \ aexp \ aexp \ com \ com" ("(FOR _/ FROM _/ TO _/ DO _)" [0, 0, 0, 61] 61) where "FOR v FROM a1 TO a2 DO c \ v ::= a1 ; WHILE (Less (V v) a2) DO (c ; v ::= Plus (V v) (N 1))" abbreviation Afor :: "assn \ vname \ aexp \ aexp \ acom \ acom" ("({_}/ FOR _/ FROM _/ TO _/ DO _)" [0, 0, 0, 0, 61] 61) where "{b} FOR v FROM a1 TO a2 DO c \ v ::= a1 ; {b} WHILE (Less (V v) a2) DO (c ; v ::= Plus (V v) (N 1))" text {* \paragraph{Multiplication.} Define an annotated program @{text "MULTIPLY x y"}, so that when the annotations are stripped away, it yields the program below. (The parameters @{text "x"} and @{text "y"} will appear only in the loop annotations.) *} definition MULTIPLY :: "int \ int \ acom" where (*<*) "MULTIPLY x y = ( ''c'' ::= N 0 ; {\s. s ''a'' = x \ s ''b'' = y \ s ''c'' = s ''d'' * y \ s ''d'' \ x} FOR ''d'' FROM (N 0) TO (V ''a'') DO ''c'' ::= Plus (V ''c'') (V ''b''))" (*>*) lemma "strip (MULTIPLY x y) = (''c'' ::= N 0 ; FOR ''d'' FROM (N 0) TO (V ''a'') DO ''c'' ::= Plus (V ''c'') (V ''b''))" (*<*) by (simp add: MULTIPLY_def) (*>*) text {* Once you have the correct loop annotations, then the partial correctness proof can be done in two steps, with the help of lemma @{text "vc_sound'"}. *} lemma MULTIPLY_correct: "\ {\s. s ''a'' = x \ s ''b'' = y \ 0 \ x} strip (MULTIPLY x y) {\s. s ''c'' = x*y \ s ''a'' = x \ s ''b'' = y}" by (rule vc_sound', auto simp add: MULTIPLY_def algebra_simps) lemma MULTIPLY_correct': "\ {\s. s ''a'' = x \ s ''b'' = y \ 0 \ x} strip (MULTIPLY x y) {\s. s ''c'' = x*y \ s ''a'' = x \ s ''b'' = y}" apply (rule vc_sound_opt) apply (simp add: MULTIPLY_def) apply (auto simp add: algebra_simps) done text {* The total correctness proof will look much like the Hoare logic proofs from Exercise Sheet 9, but you must use the rules from @{text "HoareT.thy"} instead. Also note that when using rule @{text "HoareT.While'"}, you must instantiate both the predicate @{text "P :: state \ bool"} and the measure @{text "f :: state \ nat"}. The measure must decrease every time the body of the loop is executed. *} lemma MULTIPLY_totally_correct: "\\<^sub>t {\s. s ''a'' = x \ s ''b'' = y \ 0 \ x} strip (MULTIPLY x y) {\s. s ''c'' = x*y \ s ''a'' = x \ s ''b'' = y}" (*<*) apply (simp add: MULTIPLY_def) apply (rule HoareT.Semi [rotated]) apply (rule HoareT.Semi [rotated]) apply (rule HoareT.While' [where f="\s. nat (s ''a'' - s ''d'')" and P="\s. s ''a''=x \ s ''b''=y \ s ''c'' = s ''d'' * y \ s ''d'' \ x"]) apply (rule HoareT.Semi [rotated]) apply (rule HoareT.Assign) apply (rule HoareT.Assign') apply (clarsimp simp add: algebra_simps) apply clarsimp apply (rule HoareT.Assign) apply (rule HoareT.Assign') apply clarsimp done (*>*) text {* \paragraph{Division.} Define an annotated version of this division program, which yields the quotient and remainder of @{text "''a''/''b''"} in variables @{text "''q''"} and @{text "''r''"}, respectively. *} definition DIVIDE :: "int \ int \ acom" where (*<*) "DIVIDE x y = ( ''q'' ::= N 0 ; ''r'' ::= N 0 ; {\s. (*<*)s ''c'' = s ''q'' * y + s ''r'' \ 0 \ s ''r'' \ s ''r'' < y \ s ''c'' \ x \ s ''a'' = x \ s ''b'' = y(*>*)} FOR ''c'' FROM (N 0) TO (V ''a'') DO ( ''r'' ::= Plus (V ''r'') (N 1) ; IF Less (V ''r'') (V ''b'') THEN ASKIP ELSE (''r'' ::= N 0 ; ''q'' ::= Plus (V ''q'') (N 1))))" (*>*) lemma "strip (DIVIDE x y) = ( ''q'' ::= N 0 ; ''r'' ::= N 0 ; FOR ''c'' FROM (N 0) TO (V ''a'') DO ( ''r'' ::= Plus (V ''r'') (N 1) ; IF Less (V ''r'') (V ''b'') THEN SKIP ELSE (''r'' ::= N 0 ; ''q'' ::= Plus (V ''q'') (N 1))))" (*<*) by (simp add: DIVIDE_def) (*>*) text {* Again, with the right annotations the partial correctness proof should be automatic. *} lemma DIVIDE_correct: "\ {\s. s ''a'' = x \ s ''b'' = y \ 0 \ x \ 0 < y} strip (DIVIDE x y) {\s. x = s ''q'' * y + s ''r'' \ 0 \ s ''r'' \ s ''r'' < y \ s ''a'' = x \ s ''b'' = y}" by (rule vc_sound', auto simp add: DIVIDE_def algebra_simps) text {* Also prove total correctness (replace @{text "\"} with @{text "\\<^sub>t"}). *} (*<*) lemma DIVIDE_totally_correct: "\\<^sub>t {\s. s ''a'' = x \ s ''b'' = y \ 0 \ x \ 0 < y} strip (DIVIDE x y) {\s. x = s ''q'' * y + s ''r'' \ 0 \ s ''r'' \ s ''r'' < y \ s ''a'' = x \ s ''b'' = y}" apply (simp add: DIVIDE_def) apply (rule HoareT.Semi [rotated]) apply (rule HoareT.Semi [rotated]) apply (rule HoareT.While' [where f="\s. nat (s ''a'' - s ''c'')" and P="\s. s ''c'' = s ''q'' * y + s ''r'' \ 0 \ s ''r'' \ s ''r'' < y \ s ''c'' \ x \ s ''a'' = x \ s ''b'' = y"]) apply (rule HoareT.Semi [rotated]) apply (rule HoareT.Assign) (* bh: What am I doing wrong here? It seems like the apply-style Hoare rules get stuck on the if-then-else: The schematic variables never get properly instantiated. *) apply (rule_tac P\<^isub>2="\s. (s ''c'' = s ''q'' * y + s ''r'' - 1 \ 0 \ s ''r'' - 1 \ s ''r'' - 1 < y \ s ''c'' \ x \ s ''a'' = x \ s ''b'' = y) \ bval (Less (V ''c'') (V ''a'')) s \ nat (s ''a'' - s ''c'') = n" in HoareT.Semi [rotated]) apply (rule HoareT.If) apply (rule HoareT.strengthen_pre [OF _ HoareT.Skip]) apply clarsimp apply (rule HoareT.Semi [rotated]) apply (rule HoareT.Assign) apply (rule HoareT.Assign') apply (clarsimp simp add: algebra_simps) apply (rule HoareT.Assign') apply clarsimp apply clarsimp apply (rule HoareT.Assign) apply (rule HoareT.Semi [rotated]) apply (rule HoareT.Assign) apply (rule HoareT.Assign') apply simp done (*>*) text {* \paragraph{Square roots.} Define an annotated version of this square root program, which yields the square root of input @{text "''a''"} (rounded down to the next integer) in output @{text "''b''"}. *} definition SQUAREROOT :: "int \ acom" where (*<*) "SQUAREROOT x = ( ''b'' ::= N 0 ; ''c'' ::= N 1 ; {\s. s ''a'' = x \ (s ''b'')\ \ x \ s ''c'' = (s ''b'' + 1)\} WHILE (Not (Less (V ''a'') (V ''c''))) DO ( ''b'' ::= Plus (V ''b'') (N 1); ''c'' ::= Plus (V ''c'') (V ''b''); ''c'' ::= Plus (V ''c'') (V ''b''); ''c'' ::= Plus (V ''c'') (N 1)))" (*>*) lemma "strip (SQUAREROOT x) = ( ''b'' ::= N 0 ; ''c'' ::= N 1 ; WHILE (Not (Less (V ''a'') (V ''c''))) DO ( ''b'' ::= Plus (V ''b'') (N 1); ''c'' ::= Plus (V ''c'') (V ''b''); ''c'' ::= Plus (V ''c'') (V ''b''); ''c'' ::= Plus (V ''c'') (N 1)))" (*<*) by (simp add: SQUAREROOT_def) (*>*) text {* Prove partial correctness using the VC generator, as shown. *} lemma SQUAREROOT_correct: "\ {\s. s ''a'' = x \ 0 \ x} strip (SQUAREROOT x) {\s. s ''a'' = x \ (s ''b'')\ \ x \ x < (s ''b'' + 1)\}" by (rule vc_sound', auto simp add: SQUAREROOT_def power2_eq_square algebra_simps) text {* Finally, prove total correctness of the square root algorithm. *} (*<*) lemma SQUAREROOT_totally_correct: "\\<^sub>t {\s. s ''a'' = x \ 0 \ x} strip (SQUAREROOT x) {\s. s ''a'' = x \ (s ''b'')\ \ x \ x < (s ''b'' + 1)\}" apply (simp add: SQUAREROOT_def) apply (rule HoareT.Semi [rotated]) apply (rule HoareT.While' [where f="\s. nat (s ''a'' - s ''b'' * s ''b'')" and P="\s. s ''a'' = x \ 0 \ s ''b'' \ (s ''b'')\ \ x \ s ''c'' = (s ''b'' + 1)\"]) apply (rule HoareT.Semi [rotated]) apply (rule HoareT.Assign) apply (rule HoareT.Semi [rotated]) apply (rule HoareT.Assign) apply (rule HoareT.Semi [rotated]) apply (rule HoareT.Assign) apply (rule HoareT.Assign') apply (clarsimp simp add: algebra_simps power2_eq_square) apply clarsimp apply (rule HoareT.Semi [rotated]) apply (rule HoareT.Assign) apply (rule HoareT.Assign') apply clarsimp done (*>*) (*<*) end (*>*)