theory hw_template
imports HoareT Vars
begin
datatype acom =
ASKIP |
Aassign vname aexp ("(_ ::= _)" [1000, 61] 61) |
Aseq acom acom ("_;/ _" [60, 61] 60) |
Aif bexp acom acom ("(IF _/ THEN _/ ELSE _)" [0, 0, 61] 61) |
Awhile assn "state \ nat" bexp acom ("({_,_}/ WHILE _/ DO _)" [0, 0, 61] 61)
instantiation com :: vars
begin
fun vars_com :: "com \ vname set" where
"vars_com SKIP = {}"
|"vars_com (x ::= a) = {x} \ vars a"
|"vars_com (c1 ; c2) = vars_com c1 \ vars_com c2"
|"vars_com (IF b THEN c1 ELSE c2) = vars b \ vars_com c1 \ vars_com c2"
|"vars_com (WHILE b DO c) = vars b \ vars_com c"
instance ..
end
instantiation acom :: vars
begin
fun vars_acom :: "acom \ vname set" where
"vars_acom ASKIP = {}"
|"vars_acom (x ::= a) = {x} \ vars a"
|"vars_acom (c1 ; c2) = vars_acom c1 \ vars_acom c2"
|"vars_acom (IF b THEN c1 ELSE c2) = vars b \ vars_acom c1 \ vars_acom c2"
|"vars_acom ({I,M} WHILE b DO c) = vars b \ vars_acom c"
instance ..
end
lemma aval_vars: "\s1 = s2 on X; vars a \ X\ \ aval a s1 = aval a s2"
by (metis aval_eq_if_eq_on_vars set_mp)
lemma confinement: "(c,s) \ t \ s = t on (UNIV - vars c)"
by (induction rule: big_step_induct) auto
text {* \paragraph{1.} Write a function for identifying
certain annotated while loops trivially well-behaved w.r.t. termination, which we call
``FOR loops". Namely, a FOR loop is an annotated command of the form
@{text "Awhile I M (Less (V x) a) (c ; x ::= (Plus (V x) (N 1)))"}
where @{text "x"} does not appear in @{text "a"} or @{text "c"}
and the sets of variables of @{text "a"} and @{text "c"} are disjoint.
FOR loops should be identified via a function @{text "isF"},
where @{text "isF b d"} tests if @{text "Awhile I M b d"} is a FOR loop: *}
fun isF :: "bexp \ acom \ bool" where
(* your definition goes here *)
"isF b a = undefined"
(* Some tests for isF: *)
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''"
lemma "isF (Less (V dd) (V aa)) (cc ::= Plus (V cc) (V bb) ; dd ::= Plus (V dd) (N 1))"
by simp
lemma "\ isF (Less (V dd) (V dd)) (cc ::= Plus (V cc) (V bb) ; dd ::= Plus (V dd) (N 1))"
by simp
lemma "\ isF (Less (V dd) (V aa)) (dd ::= Plus (V cc) (V bb) ; dd ::= Plus (V dd) (N 1))"
by simp
lemma "\ isF (Less (V dd) (V aa)) (cc ::= Plus (V cc) (V bb) ; cc ::= Plus (V dd) (N 1))"
by simp
lemma "\ isF (Less (V dd) (V aa)) (cc ::= Plus (V cc) (V bb) ; dd ::= Plus (V cc) (N 1))"
by simp
text {* \paragraph{2.} Define a verification condition
generator @{text "vc"} for total correctness.
The ``precondition" function, @{text "pre"} similar to that from the
partial-correctness case, is given in the template: *}
fun pre :: "acom \ assn \ assn" where
"pre ASKIP Q = Q" |
"pre (Aassign x a) Q = (\s. Q(s(x := aval a s)))" |
"pre (Aseq c\<^isub>1 c\<^isub>2) Q = pre c\<^isub>1 (pre c\<^isub>2 Q)" |
"pre (Aif b c\<^isub>1 c\<^isub>2) Q =
(\s. (bval b s \ pre c\<^isub>1 Q s) \
(\ bval b s \ pre c\<^isub>2 Q s))" |
"pre (Awhile I M b c) Q = I"
fun vc :: "acom \ assn \ bool" where
(* your definition goes here *)
"vc a Q = undefined"
text{* \paragraph{3.} Define a function that strips away annotations: *}
fun strip :: "acom \ com" where
(* your definition goes here *)
"strip ac = undefined"
text {* \paragraph{4.} Prove the following facts about your operators
(analogous to the partial-correctness case), culminating with soundness.
For the theorem @{text "vc_sound"}, in the WHILE case, you will need to distinguuish
between FOR loops and non FOR loops, and
provide a suitable measure in the case of the former. (Recall that
the verification condition generator should ignore the measure
annotation at FOR loops.) *}
lemma pre_mono: "\s. P s \ P' s \ pre c P s \ pre c P' s"
sorry
lemma vc_mono: "\s. P s \ P' s \ vc c P \ vc c P'"
sorry
lemma vc_sound: "vc c Q \ \\<^sub>t {pre c Q} strip c {Q}"
sorry
corollary vc_sound': "vc c Q \ (\s. P s \ pre c Q s) \ \\<^sub>t {P} strip c {Q}"
sorry
text {* APPENDIX: Some tests for your definition of @{text "vc"} *}
text{* The following is not part of the homework. It gives you a couple
of tests that will allow you to gain some confidence in your constructions. (These
are the programs from exercise sheet 11.) *}
declare algebra_simps[simp] declare power2_eq_square[simp]
text {* Multiplication *}
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"
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 ;
dd ::= N 0 ;
{iMULT i j, undefined}
WHILE Less (V dd) (V aa) DO
(
cc ::= Plus (V cc) (V bb) ;
dd ::= Plus (V dd) (N 1)
)"
text{* Note that the annotated program @{text "AMULT"} has a dummy measure annotation,
@{text "undefined"}.
Yet, since the FOR condition holds,
your @{text "vc"} function should be able to include a proper measure instead
of @{text "undefined"} and prove the program correct. *}
lemma "isF (Less (V dd) (V aa))
(cc ::= Plus (V cc) (V bb) ; dd ::= Plus (V dd) (N 1))"
by simp
lemma MULT_totally_correct: "\\<^sub>t {P_MULT i j} (strip (AMULT i j)) {Q_MULT i j}"
apply(rule vc_sound') unfolding AMULT_def P_MULT_def Q_MULT_def iMULT_def by auto
text {* Division *}
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"
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 ADIV1 :: acom where "ADIV1 \ rr ::= Plus (V rr) (N 1) ; ADIV_IF"
definition ADIV :: "int \ int \ acom" where
"ADIV i j \
qq ::= N 0 ;
rr ::= N 0 ;
cc ::= N 0 ;
{iDIV i j, undefined}
WHILE (Less (V cc) (V aa)) DO
(
ADIV1 ;
cc ::= Plus (V cc) (N 1)
)"
lemmas ADIV_defs = ADIV1_def ADIV_IF_def ADIV_def
text{* Again, the annotated program provides a dummy measure,
but your @{text "vc"} should consider a proper measure instead. *}
lemma "isF (Less (V cc) (V aa)) (ADIV1 ; cc ::= Plus (V cc) (N 1))"
unfolding ADIV_defs by simp
lemma DIV_correct: "\\<^sub>t {P_DIV i j} (strip (ADIV i j)) {Q_DIV i j}"
apply(rule vc_sound') unfolding ADIV_defs P_DIV_def Q_DIV_def iDIV_def by auto
text {* Square roots *}
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 "mSQR \ \s. nat (s aa - s bb * s bb)"
definition ASQR1 :: acom where
"ASQR1 \
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 \
bb ::= N 0;
cc ::= N 1;
{iSQR i, mSQR}
WHILE (Not (Less (V aa) (V cc))) DO
ASQR1"
lemmas ASQR_defs = ASQR1_def ASQR_def
text{* This time, the FOR condition does not hold,
so @{text "vc"} should consider the given measure @{text "mSQR"}. *}
lemma "\ isF (Not (Less (V aa) (V cc))) ASQR1"
unfolding ASQR1_def by simp
lemma SQR_totally_correct: "\\<^sub>t {P_SQR i} (strip (ASQR i)) {Q_SQR i}"
apply(rule vc_sound')
unfolding ASQR_defs P_SQR_def Q_SQR_def iSQR_def mSQR_def by auto
end