(*<*) theory ex11 imports VC HoareT begin (*>*) text {* \ExerciseSheet{11}{8.~1.~2013} *} 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"}. *} 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 \ ''d''" 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 {* Rotated rule for sequential composition: *} lemmas SeqTR = HoareT.Seq[rotated] text {* Prove the following syntax-directed conditional rule (for total correctness): *} lemma IfT: assumes "\\<^sub>t {P1} c\<^isub>1 {Q}" and "\\<^sub>t {P2} c\<^isub>2 {Q}" shows "\\<^sub>t {\s. (bval b s \ P1 s) \ (\ bval b s \ P2 s)} IF b THEN c\<^isub>1 ELSE c\<^isub>2 {Q}" (*<*) apply(rule hoaret_complete) using assms[THEN hoaret_sound] unfolding hoare_tvalid_def by blast (*>*) 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 MULT2 :: com where "MULT2 \ FOR dd FROM (N 0) TO (V aa) DO cc ::= Plus (V cc) (V bb)" definition MULT :: com where "MULT \ cc ::= N 0 ; MULT2" 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" (*>*) text{* *} definition AMULT2 :: "int \ int \ acom" where "AMULT2 i j \ {iMULT i j} FOR dd FROM (N 0) TO (V aa) DO cc ::= Plus (V cc) (V bb)" definition AMULT :: "int \ int \ acom" where "AMULT i j \ (cc ::= N 0) ; AMULT2 i j" lemmas MULT_defs = MULT2_def MULT_def P_MULT_def Q_MULT_def iMULT_def AMULT2_def AMULT_def lemma strip_AMULT: "strip (AMULT i j) = MULT" (*<*) unfolding AMULT_def MULT_def AMULT2_def MULT2_def 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 {* 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. You can define the measure first: *} definition mMULT :: "state \ nat" where (*<*) "mMULT \ \s. nat (s aa - s dd)" (*>*) text{* *} lemma MULT_totally_correct: "\\<^sub>t {P_MULT i j} MULT {Q_MULT i j}" (*<*) unfolding MULT_def apply (rule SeqTR) unfolding MULT2_def apply (rule SeqTR) apply(rule HoareT.While'[of "iMULT i j"_ mMULT]) apply (rule SeqTR) apply (rule HoareT.Assign) apply (rule HoareT.Assign') unfolding MULT_defs apply auto unfolding mMULT_def apply auto apply (rule HoareT.Assign) apply (rule HoareT.Assign') apply auto done (*>*) 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 DIV1 :: com where "DIV1 \ qq ::= N 0 ; rr ::= N 0" definition DIV_IF :: com where "DIV_IF \ IF Less (V rr) (V bb) THEN SKIP ELSE (rr ::= N 0 ; qq ::= Plus (V qq) (N 1))" definition "DIV2 \ rr ::= Plus (V rr) (N 1) ; DIV_IF" definition DIV :: com where "DIV \ DIV1 ; FOR cc FROM (N 0) TO (V aa) DO DIV2" lemmas DIV_defs = DIV1_def DIV_IF_def DIV2_def DIV_def 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 ADIV1 :: acom where "ADIV1 \ qq ::= N 0 ; rr ::= N 0" definition ADIV_IF :: acom where "ADIV_IF \ IF Less (V rr) (V bb) THEN ASKIP ELSE (rr ::= N 0 ; qq ::= Plus (V qq) (N 1))" definition ADIV2 :: acom where "ADIV2 \ rr ::= Plus (V rr) (N 1) ; ADIV_IF" definition ADIV :: "int \ int \ acom" where "ADIV i j \ ADIV1 ; {iDIV i j} FOR cc FROM (N 0) TO (V aa) DO ADIV2" lemmas ADIV_defs = ADIV1_def ADIV_IF_def ADIV2_def ADIV_def lemma strip_ADIV: "strip (ADIV i j) = DIV" (*<*) unfolding ADIV_defs DIV_defs 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_defs ADIV_defs P_DIV_def Q_DIV_def iDIV_def by auto (*>*) (* Measure function: *) definition mDIV :: "state \ nat" where (*<*) "mDIV \ \s. nat (s aa - s cc)" (*>*) text{* *} lemma DIV_totally_correct: "\\<^sub>t {P_DIV i j} DIV {Q_DIV i j}" (*<*) unfolding DIV_def apply(rule SeqTR) apply(rule SeqTR) apply(rule HoareT.While'[where P = "iDIV i j" and f = mDIV]) unfolding iDIV_def mDIV_def DIV_defs Q_DIV_def P_DIV_def by (rule SeqTR HoareT.Assign HoareT.Assign' IfT HoareT.Skip HoareT.While'[where P = "iDIV i j" and f = mDIV] | force)+ (*>*) 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 SQR1 :: com where "SQR1 \ bb ::= N 0 ; cc ::= N 1" definition SQR2 :: com where "SQR2 \ bb ::= Plus (V bb) (N 1); cc ::= Plus (V cc) (V bb); cc ::= Plus (V cc) (V bb); cc ::= Plus (V cc) (N 1)" definition SQR :: com where "SQR \ SQR1 ; (WHILE (Not (Less (V aa) (V cc))) DO SQR2)" lemmas SQR_defs = SQR1_def SQR2_def SQR_def 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 ASQR1 :: acom where "ASQR1 \ bb ::= N 0 ; cc ::= N 1" definition ASQR2 :: acom where "ASQR2 \ bb ::= Plus (V bb) (N 1); cc ::= Plus (V cc) (V bb); cc ::= Plus (V cc) (V bb); cc ::= Plus (V cc) (N 1)" definition ASQR :: "int \ acom" where "ASQR i \ ASQR1 ; ({iSQR i} WHILE (Not (Less (V aa) (V cc))) DO ASQR2)" lemmas ASQR_defs = ASQR1_def ASQR2_def ASQR_def lemma strip_ASQR: "strip (ASQR i) = SQR" unfolding ASQR_defs SQR_defs by simp lemma SQR_correct: "\ {P_SQR i} SQR {Q_SQR i}" unfolding strip_ASQR[of i, symmetric] apply(rule vc_sound') unfolding SQR_defs ASQR_defs P_SQR_def Q_SQR_def iSQR_def by auto definition "mSQR \ \s. nat (s aa - s bb * s bb)" lemma SQR_totally_correct: "\\<^sub>t {P_SQR i} SQR {Q_SQR i}" unfolding SQR_def apply(rule SeqTR) apply(rule HoareT.While'[where P = "iSQR i" and f = mSQR]) unfolding iSQR_def mSQR_def SQR_defs Q_SQR_def P_SQR_def by (rule SeqTR HoareT.Assign HoareT.Assign' IfT HoareT.Skip | force)+ (*>*) text {* \Homework{Be Original}{15.~1.~2013} Deadline of previous homework was extended, so polish your submission a bit! *} (*<*) end (*>*)