(*<*) theory sol11 imports "~~/src/HOL/IMP/Hoare_Sound_Complete" "~~/src/HOL/IMP/VCG" begin (*>*) text {* \ExerciseSheet{11}{13.~1.~2015} *} text {* There is a template available on the courses homepage *} text {* \Exercise{Forward Assignment Rule} Think up and prove a forward assignment rule, i.e., a rule of the form @{text "\ {P} x::=a {\}"}, where @{text "\"} is some suitable postcondition. Hint: To prove this rule, use the completeness property, and prove the rule semantically. *} (*<*) lemma fwd_Assign: "\ {P} x::=a {\s'. \s. P s \ s'=s[a/x]}" apply (rule hoare_complete) unfolding hoare_valid_def by auto (*>*) lemmas fwd_Assign' = weaken_post[OF fwd_Assign] text {* Redo the proofs for @{text "MAX"} and @{text "MUL"} from the previous exercise sheet, this time using your forward assignment rule. *} definition MAX :: com where "MAX \ IF (Less (V ''a'') (V ''b'')) THEN ''c''::=V ''b'' ELSE ''c''::=V ''a''" lemma "\ {\s. True} MAX {\s. s ''c'' = max (s ''a'') (s ''b'')}" (*<*) unfolding MAX_def apply (rule If) apply (rule fwd_Assign') apply (auto) [1] apply (rule fwd_Assign') apply (auto) done (*>*) 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))" lemma "\ {\s. 0 \ s ''y''} MUL {\s. s ''z'' = s ''x'' * s ''y''}" (*<*) unfolding MUL_def apply(rule Seq) apply(rule Seq) apply(rule fwd_Assign) apply(rule fwd_Assign) apply (rule strengthen_pre) prefer 2 apply (rule While'[where P="\s. s ''z'' = s ''x'' * s ''c'' \ s ''c'' \ s ''y''"]) apply(rule Seq) apply(rule fwd_Assign) apply(rule fwd_Assign') apply(auto simp add: algebra_simps) done (*>*) text {* \Exercise{Using the VCG} For each of the three programs given here, you must prove partial correctness. You should first write an annotated program, and then use the verification condition generator from @{text "VCG.thy"}. *} text{* \paragraph{Preliminaries.} *} text {* Some abbreviations, freeing us from having to write double quotes for concrete variable names: *} abbreviation "aa \ ''a''" abbreviation "bb \ ''b''" abbreviation "cc \ ''c''" abbreviation "dd \ ''d''" abbreviation "ee \ ''e''" abbreviation "ff \ ''f''" abbreviation "pp \ ''p''" abbreviation "qq \ ''q''" abbreviation "rr \ ''r''" text {* Some useful simplification rules: *} declare algebra_simps[simp] declare power2_eq_square[simp] 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.} Consider the following program @{text "MULT"} for performing multiplication and the following assertions @{text "P_MULT"} and @{text "Q_MULT"}: *} definition MULT :: com where "MULT \ cc ::= N 0 ;; FOR dd FROM (N 0) TO (V aa) DO cc ::= Plus (V cc) (V bb)" definition P_MULT :: "int \ int \ assn" where "P_MULT i j \ \s. s aa = i \ s bb = j \ 0 \ i" definition Q_MULT :: "int \ int \ assn" where "Q_MULT i j \ \s. s cc = i * j \ s aa = i \ s bb = j" text {* Define an annotated program @{text "AMULT i j"}, so that when the annotations are stripped away, it yields @{text "MULT"}. (The parameters @{text "i"} and @{text "j"} will appear only in the loop annotations.) *} text{* Hint: The program @{text "AMULT i j"} will be essentially @{text "MULT"} with an invariant annotation @{text "iMULT i j"} at the FOR loop, which you have to define: *} definition iMULT :: "int \ int \ assn" where (*<*) "iMULT i j \ \s. s aa = i \ s bb = j \ s cc = s dd * j \ s dd \ i" (*>*) definition AMULT :: "int \ int \ acom" where "AMULT i j \ (cc ::= N 0) ;; {iMULT i j} FOR dd FROM (N 0) TO (V aa) DO cc ::= Plus (V cc) (V bb)" lemmas MULT_defs = MULT_def P_MULT_def Q_MULT_def iMULT_def AMULT_def lemma strip_AMULT: "strip (AMULT i j) = MULT" (*<*) unfolding MULT_defs by simp (*>*) 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 MULT_correct: "\ {P_MULT i j} MULT {Q_MULT i j}" (*<*) unfolding strip_AMULT[of i j, symmetric] apply(rule vc_sound') unfolding MULT_defs by auto (*>*) text {* \paragraph{Division.} Define an annotated version of this division program, which yields the quotient and remainder of @{text "aa/bb"} in variables @{text "''q''"} and @{text "''r''"}, respectively. *} definition DIV :: com where "DIV \ qq ::= N 0 ;; rr ::= N 0 ;; FOR cc FROM (N 0) TO (V aa) DO ( rr ::= Plus (V rr) (N 1) ;; IF Less (V rr) (V bb) THEN Com.SKIP ELSE ( rr ::= N 0 ;; qq ::= Plus (V qq) (N 1)) )" definition P_DIV :: "int \ int \ assn" where "P_DIV i j \ \s. s aa = i \ s bb = j \ 0 \ i \ 0 < j" definition Q_DIV :: "int \ int \ assn" where "Q_DIV i j \ \ s. i = s qq * j + s rr \ 0 \ s rr \ s rr < j \ s aa = i \ s bb = j" definition iDIV :: "int \ int \ assn" where (*<*) "iDIV i j \ \ s. s cc = s qq * j + s rr \ 0 \ s rr \ s rr < j \ s cc \ i \ s aa = i \ s bb = j" (*>*) text{* *} definition ADIV :: "int \ int \ acom" where "ADIV i j \ qq ::= N 0 ;; rr ::= N 0 ;; {iDIV i j} FOR cc FROM (N 0) TO (V aa) DO ( rr ::= Plus (V rr) (N 1) ;; IF Less (V rr) (V bb) THEN SKIP ELSE ( rr ::= N 0 ;; qq ::= Plus (V qq) (N 1) ) )" lemma strip_ADIV: "strip (ADIV i j) = DIV" (*<*) unfolding ADIV_def DIV_def by simp (*>*) lemma DIV_correct: "\ {P_DIV i j} DIV {Q_DIV i j}" (*<*) unfolding strip_ADIV[of i j, symmetric] apply(rule vc_sound') unfolding DIV_def ADIV_def P_DIV_def Q_DIV_def iDIV_def by auto (*>*) text {* \paragraph{Square roots.} Define an annotated version of this square root program, which yields the square root of input @{text "aa"} (rounded down to the next integer) in output @{text "bb"}. *} definition SQR :: com where "SQR \ bb ::= N 0 ;; cc ::= N 1 ;; WHILE (Not (Less (V aa) (V cc))) DO ( bb ::= Plus (V bb) (N 1);; cc ::= Plus (V cc) (Plus (V bb) (Plus (V bb) (N 1))) )" definition P_SQR :: "int \ assn" where "P_SQR i \ \s. s aa = i \ 0 \ i" definition Q_SQR :: "int \ assn" where "Q_SQR i \ \s. s aa = i \ (s bb)^2 \ i \ i < (s bb + 1)^2" (*<*) definition iSQR :: "int \ assn" where "iSQR i \ \s. s aa = i \ 0 \ s bb \ (s bb)^2 \ i \ s cc = (s bb + 1)^2" definition ASQR :: "int \ acom" where "ASQR i \ bb ::= N 0 ;; cc ::= N 1 ;; {iSQR i} WHILE (Not (Less (V aa) (V cc))) DO ( bb ::= Plus (V bb) (N 1);; cc ::= Plus (V cc) (Plus (V bb) (Plus (V bb) (N 1))) )" lemma strip_ASQR: "strip (ASQR i) = SQR" unfolding ASQR_def SQR_def by simp lemma SQR_correct: "\ {P_SQR i} SQR {Q_SQR i}" unfolding strip_ASQR[of i, symmetric] apply(rule vc_sound') unfolding SQR_def ASQR_def P_SQR_def Q_SQR_def iSQR_def by auto (*>*) (*<*) end (*>*)