theory week08B_demo_sol imports Main begin \ \Syntax and State Space\ type_synonym vname = string type_synonym state = "vname \ nat" type_synonym aexp = "state \ nat" type_synonym bexp = "state \ bool" datatype com = SKIP | Assign vname aexp ("_ :== _ " [60,60] 60) | Semi com com ("_;; _" [50, 51] 50) | Cond bexp com com ("IF _ THEN _ ELSE _" [0,0,59] 60) | While bexp com ("WHILE _ DO _ OD" [0,45] 60) \ \Example Program\ definition A :: vname where "A \ ''A''" definition B :: vname where "B \ ''B''" lemma [simp]: "A \ B" by (simp add: A_def B_def) lemma [simp]: "B \ A" by (simp add: A_def B_def) definition factorial :: com where "factorial \ B :== (\s. 1);; WHILE (\s. s A \ 0) DO B :== (\s. s B * s A);; A :== (\s. s A - 1) OD" \ \Execution\ inductive eval :: "com \ state \ state \ bool" ("_/ \ _" [60,60] 61) where Skip [intro!,simp]: "(SKIP, s) \ s" | Assign [intro!,simp]: "(x :== a, s) \ s (x := a s)" | Semi [intro!]: "\ (c\<^sub>1,s) \ s''; (c\<^sub>2,s'') \ s' \ \ (c\<^sub>1;; c\<^sub>2, s) \ s'" | IfTrue: "\ b s; (c\<^sub>1,s) \ s' \ \ (IF b THEN c\<^sub>1 ELSE c\<^sub>2, s) \ s'" | IfFalse: "\ \b s; (c\<^sub>2,s) \ s' \ \ (IF b THEN c\<^sub>1 ELSE c\<^sub>2, s) \ s'" | WhileFalse: "\b s \ (WHILE b DO c OD, s) \ s" | WhileTrue: "\b s; (c,s) \ s''; (WHILE b DO c OD, s'') \ s'\ \ (WHILE b DO c OD, s) \ s'" (* Isabelle provides eval.induct which allows the elimination of terms cs \ t. In practice, we will have cs as a tuple (c,s). To avoid to manually have to split cs every time, we can use split_format as below to define an induction rule that will work on terms of the form (c, s) \ t.*) thm eval.induct lemmas eval_induct = eval.induct [split_format (complete)] thm eval_induct (* In practice, it is also useful to have elimination rules for precisely when e.g. c=SKIP, or c= c1;;c2, etc. (If c=SKIP, eval_induct has many useless cases). The command inductive_cases allows exactly this.*) inductive_cases skip [elim!]: "(SKIP, s) \ s'" and assign [elim!]: "(x :== a, s) \ s'" and semi [elim!]: "(c\<^sub>1;; c\<^sub>2, s) \ s'" and "if" [elim!]: "(IF b THEN c\<^sub>1 ELSE c\<^sub>2, s) \ s'" and while: "(WHILE b DO c OD, s) \ s'" thm skip assign semi "if" while lemma skip_eq [simp]: "(SKIP, s) \ s' = (s' = s)" by blast lemma assign_eq [simp]: "(x :== a, s) \ s' = (s' = s (x := a s))" by blast \ \---------------------------------------------------------------------\ \ \Example Proof\ primrec fac :: "nat \ nat" where "fac 0 = 1" |"fac (Suc n) = (Suc n) * fac n" (* Need to relate the final state of B to values of A and B *at each iteration* of the loop *) lemma factorial_partial_correct_helper: "(prog, s) \ s' \ prog = WHILE \s. 0 < s A DO B :== (\s. s B * s A) ;; A :== (\s. s A - Suc 0) OD \ s' B = s B * fac (s A)" apply (induct rule: eval_induct) apply (simp_all) apply (case_tac "s A") apply (simp) apply clarsimp (*sledgehammer*) by (simp add: distrib_left distrib_right) lemma factorial_partial_correct: "(factorial, s) \ s' \ s' B = fac (s A)" apply (unfold factorial_def) apply clarsimp apply (clarsimp simp: factorial_partial_correct_helper) done \ \---------------------------------------------------------------------\ type_synonym assn = "state => bool" definition hoare_valid :: "assn \ com \ assn \ bool" ("\ {(1_)}/ (_)/ {(1_)}" 50) where "\ {P} c {Q} \ \s s'. P s \ (c,s) \ s' \ Q s'" inductive hoare :: "assn \ com \ assn \ bool" ("\ ({(1_)}/ (_)/ {(1_)})" 50) where h_skip: "\ {P} SKIP {P}" | h_assign: "\ {\s. P (s(x:= a s))} x:==a {P}" | h_semi: "\ \ {P} c\<^sub>1 {R}; \ {R} c\<^sub>2 {Q} \ \ \ {P} c\<^sub>1;;c\<^sub>2 {Q}" | h_if: "\ \ {\s. P s \ b s} c\<^sub>1 {Q}; \ {\s. P s \ \b s} c\<^sub>2 {Q} \ \ \ {P} IF b THEN c\<^sub>1 ELSE c\<^sub>2 {Q}" | h_while: "\ \ {\s. P s \ b s} c {P}; \s. P s \ \b s \ Q s \ \ \ {P} WHILE b DO c OD {Q}" | conseq: "\ \s. P s \ P' s; \ {P'} c {Q'}; \s. Q' s \ Q s \ \ \ {P} c {Q}" \ \Soundness Proof\ (* When a while loop is fully executed to a state s', then the loop condition is false in s' (otherwise there would have been another iteration). Moreover, if the loop satisfies an invariant P, then P is true when the loop exits. *) lemma while_final: "\(prog, s) \ s'; \s. P s \ b s \ (\s'. (c, s) \ s' \ P s'); P s; prog = WHILE b DO c OD\ \ P s' \ \ b s'" apply (induct rule: eval_induct) apply (simp_all) done (* To show that a postcondition Q holds after a While loop, we need to find a predicate P that is an invariant of the loop (i.e. preserved by the loop body at each iteration) and is "enough" to prove the postcondition when the proof exits.*) lemma while_sound: "\\ {\a. P a \ b a} c {P}; \s. P s \ \ b s \ Q s\ \ \ {P} WHILE b DO c OD {Q}" apply (clarsimp simp: hoare_valid_def) apply (subgoal_tac "P s' \ \ b s'") apply blast apply (rule while_final) apply (simp_all) done theorem hoare_sound: "\ {P} c {Q} \ \ {P} c {Q}" proof(induct rule: hoare.induct) case (h_while P b c Q) then show ?case by(rule_tac while_sound) qed (auto simp add: hoare_valid_def) (*OR*) theorem hoare_sound2: "\ {P} c {Q} \ \ {P} c {Q}" apply (induct rule:hoare.induct) by (fastforce elim: while_sound simp: hoare_valid_def)+ \ \--------------------------------------------------------------------------------------\ \ \derived rules\ lemma h_ass: "(\s. P s \ Q (s(x := a s))) \ \ {P} x :== a {Q}" apply (rule_tac Q'=Q in conseq) prefer 2 apply (rule h_assign) apply (blast)+ done \ \example proof\ lemma "\ {\s. True} x :== (\s. 2) {\s. s x = 2}" apply (rule h_ass) apply simp done lemma "\ {\s. s A = n} factorial {\s. s B = fac n}" apply (unfold factorial_def) apply (rule h_semi) prefer 2 apply (rule_tac P="\s. s B * fac (s A) = fac n" in h_while) apply (rule h_semi) prefer 2 apply (rule h_assign) apply (rule h_ass) apply clarsimp apply (case_tac "s A", simp) apply clarsimp apply (simp add: add_mult_distrib2 comm_semiring_class.distrib) apply clarsimp apply (rule h_ass) apply clarsimp done \ \Bonus content: completeness proof\ text \ In our setting, Hoare Logic is complete. In other settings, stating this result may require some additional caveats. For this reason, it's more often called relative completeness. The classic reference is: S. A. Cook. Soundness and completeness of an axiom system for program verification, SIAM J. Comput. 7 (1978) 7-90; Corrigendum, 10(1981), p. 612. \ lemma hoare_complete: assumes "\ {P} c {Q}" shows "\ {P} c {Q}" proof - \ \ The \ assumption is easier to apply in this form:\ from assms have "\s s'. P s \ (c, s) \ s' \ Q s'" unfolding hoare_valid_def by blast thus ?thesis \ \ Structural induction is the only reasonable choice here: we don't have an inductively defined predicate as a premise. \ proof(induct c arbitrary: P Q) case SKIP then show ?case by(force intro: conseq h_skip) next case (Assign x1 x2) then show ?case by(rule_tac h_ass) force next case (Semi c1 c2) show ?case \ \ We need to invent an intermediate assertion that holds between c1 and c2 here. We don't know much about what holds after c1. But we know that if we continue with c2, we'll reach a state where Q holds: \ by(rule h_semi[where R="\s. \s'. (c2,s) \ s' \ Q s'"]) (auto intro: Semi) next case (Cond x1 c1 c2) show ?case by(force intro: h_if Cond IfTrue IfFalse) next case (While x1 c) show ?case \ \ We need to invent a loop invariant here. Similarly to the Semi case, we don't know what c does. But we do know that if we keep looping and terminate, we should reach a state where Q holds: \ by (rule conseq[where P'="\s. \s'. (While x1 c, s) \ s' \ Q s'" and Q'=Q, rotated, OF h_while]) (auto intro: WhileTrue While WhileFalse) qed qed end