43158

1 
header{* Hoare Logic for Total Correctness *}


2 


3 
theory HoareT imports Hoare_Sound_Complete Util begin


4 


5 
text{*


6 
Now that we have termination, we can define


7 
total validity, @{text"\<Turnstile>\<^sub>t"}, as partial validity and guaranteed termination:*}


8 


9 
definition hoare_tvalid :: "assn \<Rightarrow> com \<Rightarrow> assn \<Rightarrow> bool"


10 
("\<Turnstile>\<^sub>t {(1_)}/ (_)/ {(1_)}" 50) where


11 
"\<Turnstile>\<^sub>t {P}c{Q} \<equiv> \<forall>s. P s \<longrightarrow> (\<exists>t. (c,s) \<Rightarrow> t \<and> Q t)"


12 


13 
text{* Proveability of Hoare triples in the proof system for total


14 
correctness is written @{text"\<turnstile>\<^sub>t {P}c{Q}"} and defined


15 
inductively. The rules for @{text"\<turnstile>\<^sub>t"} differ from those for


16 
@{text"\<turnstile>"} only in the one place where nontermination can arise: the


17 
@{term While}rule. *}


18 


19 
inductive


20 
hoaret :: "assn \<Rightarrow> com \<Rightarrow> assn \<Rightarrow> bool" ("\<turnstile>\<^sub>t ({(1_)}/ (_)/ {(1_)})" 50)


21 
where


22 
Skip: "\<turnstile>\<^sub>t {P} SKIP {P}" 


23 
Assign: "\<turnstile>\<^sub>t {\<lambda>s. P(s[a/x])} x::=a {P}" 


24 
Semi: "\<lbrakk> \<turnstile>\<^sub>t {P\<^isub>1} c\<^isub>1 {P\<^isub>2}; \<turnstile>\<^sub>t {P\<^isub>2} c\<^isub>2 {P\<^isub>3} \<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>t {P\<^isub>1} c\<^isub>1;c\<^isub>2 {P\<^isub>3}" 


25 
If: "\<lbrakk> \<turnstile>\<^sub>t {\<lambda>s. P s \<and> bval b s} c\<^isub>1 {Q}; \<turnstile>\<^sub>t {\<lambda>s. P s \<and> \<not> bval b s} c\<^isub>2 {Q} \<rbrakk>


26 
\<Longrightarrow> \<turnstile>\<^sub>t {P} IF b THEN c\<^isub>1 ELSE c\<^isub>2 {Q}" 


27 
While:


28 
"\<lbrakk> \<And>n::nat. \<turnstile>\<^sub>t {\<lambda>s. P s \<and> bval b s \<and> f s = n} c {\<lambda>s. P s \<and> f s < n}\<rbrakk>


29 
\<Longrightarrow> \<turnstile>\<^sub>t {P} WHILE b DO c {\<lambda>s. P s \<and> \<not>bval b s}" 


30 
conseq: "\<lbrakk> \<forall>s. P' s \<longrightarrow> P s; \<turnstile>\<^sub>t {P}c{Q}; \<forall>s. Q s \<longrightarrow> Q' s \<rbrakk> \<Longrightarrow>


31 
\<turnstile>\<^sub>t {P'}c{Q'}"


32 


33 
text{* The @{term While}rule is like the one for partial correctness but it


34 
requires additionally that with every execution of the loop body some measure


35 
function @{term[source]"f :: state \<Rightarrow> nat"} decreases. *}


36 


37 
lemma strengthen_pre:


38 
"\<lbrakk> \<forall>s. P' s \<longrightarrow> P s; \<turnstile>\<^sub>t {P} c {Q} \<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>t {P'} c {Q}"


39 
by (metis conseq)


40 


41 
lemma weaken_post:


42 
"\<lbrakk> \<turnstile>\<^sub>t {P} c {Q}; \<forall>s. Q s \<longrightarrow> Q' s \<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>t {P} c {Q'}"


43 
by (metis conseq)


44 


45 
lemma Assign': "\<forall>s. P s \<longrightarrow> Q(s[a/x]) \<Longrightarrow> \<turnstile>\<^sub>t {P} x ::= a {Q}"


46 
by (simp add: strengthen_pre[OF _ Assign])


47 


48 
lemma While':


49 
assumes "\<And>n::nat. \<turnstile>\<^sub>t {\<lambda>s. P s \<and> bval b s \<and> f s = n} c {\<lambda>s. P s \<and> f s < n}"


50 
and "\<forall>s. P s \<and> \<not> bval b s \<longrightarrow> Q s"


51 
shows "\<turnstile>\<^sub>t {P} WHILE b DO c {Q}"


52 
by(blast intro: assms(1) weaken_post[OF While assms(2)])


53 


54 
text{* Our standard example: *}


55 


56 
abbreviation "w n ==


57 
WHILE Less (V ''y'') (N n)


58 
DO ( ''y'' ::= Plus (V ''y'') (N 1); ''x'' ::= Plus (V ''x'') (V ''y'') )"


59 


60 
lemma "\<turnstile>\<^sub>t {\<lambda>s. 0 <= n} ''x'' ::= N 0; ''y'' ::= N 0; w n {\<lambda>s. s ''x'' = \<Sum> {1 .. n}}"


61 
apply(rule Semi)


62 
prefer 2


63 
apply(rule While'


64 
[where P = "\<lambda>s. s ''x'' = \<Sum> {1..s ''y''} \<and> 0 <= n \<and> 0 <= s ''y'' \<and> s ''y'' \<le> n"


65 
and f = "\<lambda>s. nat n  nat (s ''y'')"])


66 
apply(rule Semi)


67 
prefer 2


68 
apply(rule Assign)


69 
apply(rule Assign')


70 
apply (simp add: atLeastAtMostPlus1_int_conv algebra_simps)


71 
apply clarsimp


72 
apply arith


73 
apply fastsimp


74 
apply(rule Semi)


75 
prefer 2


76 
apply(rule Assign)


77 
apply(rule Assign')


78 
apply simp


79 
done


80 


81 


82 
text{* The soundness theorem: *}


83 


84 
theorem hoaret_sound: "\<turnstile>\<^sub>t {P}c{Q} \<Longrightarrow> \<Turnstile>\<^sub>t {P}c{Q}"


85 
proof(unfold hoare_tvalid_def, induct rule: hoaret.induct)


86 
case (While P b f c)


87 
show ?case


88 
proof


89 
fix s


90 
show "P s \<longrightarrow> (\<exists>t. (WHILE b DO c, s) \<Rightarrow> t \<and> P t \<and> \<not> bval b t)"


91 
proof(induct "f s" arbitrary: s rule: less_induct)


92 
case (less n)


93 
thus ?case by (metis While(2) WhileFalse WhileTrue)


94 
qed


95 
qed


96 
next


97 
case If thus ?case by auto blast


98 
qed fastsimp+


99 


100 


101 
text{*


102 
The completeness proof proceeds along the same lines as the one for partial


103 
correctness. First we have to strengthen our notion of weakest precondition


104 
to take termination into account: *}


105 


106 
definition wpt :: "com \<Rightarrow> assn \<Rightarrow> assn" ("wp\<^sub>t") where


107 
"wp\<^sub>t c Q \<equiv> \<lambda>s. \<exists>t. (c,s) \<Rightarrow> t \<and> Q t"


108 


109 
lemma [simp]: "wp\<^sub>t SKIP Q = Q"


110 
by(auto intro!: ext simp: wpt_def)


111 


112 
lemma [simp]: "wp\<^sub>t (x ::= e) Q = (\<lambda>s. Q(s(x := aval e s)))"


113 
by(auto intro!: ext simp: wpt_def)


114 


115 
lemma [simp]: "wp\<^sub>t (c\<^isub>1;c\<^isub>2) Q = wp\<^sub>t c\<^isub>1 (wp\<^sub>t c\<^isub>2 Q)"


116 
unfolding wpt_def


117 
apply(rule ext)


118 
apply auto


119 
done


120 


121 
lemma [simp]:


122 
"wp\<^sub>t (IF b THEN c\<^isub>1 ELSE c\<^isub>2) Q = (\<lambda>s. wp\<^sub>t (if bval b s then c\<^isub>1 else c\<^isub>2) Q s)"


123 
apply(unfold wpt_def)


124 
apply(rule ext)


125 
apply auto


126 
done


127 


128 


129 
text{* Now we define the number of iterations @{term "WHILE b DO c"} needs to


130 
terminate when started in state @{text s}. Because this is a truly partial


131 
function, we define it as an (inductive) relation first: *}


132 


133 
inductive Its :: "bexp \<Rightarrow> com \<Rightarrow> state \<Rightarrow> nat \<Rightarrow> bool" where


134 
Its_0: "\<not> bval b s \<Longrightarrow> Its b c s 0" 


135 
Its_Suc: "\<lbrakk> bval b s; (c,s) \<Rightarrow> s'; Its b c s' n \<rbrakk> \<Longrightarrow> Its b c s (Suc n)"


136 


137 
text{* The relation is in fact a function: *}


138 


139 
lemma Its_fun: "Its b c s n \<Longrightarrow> Its b c s n' \<Longrightarrow> n=n'"


140 
proof(induct arbitrary: n' rule:Its.induct)


141 
(* new release:


142 
case Its_0 thus ?case by(metis Its.cases)


143 
next


144 
case Its_Suc thus ?case by(metis Its.cases big_step_determ)


145 
qed


146 
*)


147 
case Its_0


148 
from this(1) Its.cases[OF this(2)] show ?case by metis


149 
next


150 
case (Its_Suc b s c s' n n')


151 
note C = this


152 
from this(5) show ?case


153 
proof cases


154 
case Its_0 with Its_Suc(1) show ?thesis by blast


155 
next


156 
case Its_Suc with C show ?thesis by(metis big_step_determ)


157 
qed


158 
qed


159 


160 
text{* For all terminating loops, @{const Its} yields a result: *}


161 


162 
lemma WHILE_Its: "(WHILE b DO c,s) \<Rightarrow> t \<Longrightarrow> \<exists>n. Its b c s n"


163 
proof(induct "WHILE b DO c" s t rule: big_step_induct)


164 
case WhileFalse thus ?case by (metis Its_0)


165 
next


166 
case WhileTrue thus ?case by (metis Its_Suc)


167 
qed


168 


169 
text{* Now the relation is turned into a function with the help of


170 
the description operator @{text THE}: *}


171 


172 
definition its :: "bexp \<Rightarrow> com \<Rightarrow> state \<Rightarrow> nat" where


173 
"its b c s = (THE n. Its b c s n)"


174 


175 
text{* The key property: every loop iteration increases @{const its} by 1. *}


176 


177 
lemma its_Suc: "\<lbrakk> bval b s; (c, s) \<Rightarrow> s'; (WHILE b DO c, s') \<Rightarrow> t\<rbrakk>


178 
\<Longrightarrow> its b c s = Suc(its b c s')"


179 
by (metis its_def WHILE_Its Its.intros(2) Its_fun the_equality)


180 


181 
lemma wpt_is_pre: "\<turnstile>\<^sub>t {wp\<^sub>t c Q} c {Q}"


182 
proof (induct c arbitrary: Q)


183 
case SKIP show ?case by simp (blast intro:hoaret.Skip)


184 
next


185 
case Assign show ?case by simp (blast intro:hoaret.Assign)


186 
next


187 
case Semi thus ?case by simp (blast intro:hoaret.Semi)


188 
next


189 
case If thus ?case by simp (blast intro:hoaret.If hoaret.conseq)


190 
next


191 
case (While b c)


192 
let ?w = "WHILE b DO c"


193 
{ fix n


194 
have "\<forall>s. wp\<^sub>t ?w Q s \<and> bval b s \<and> its b c s = n \<longrightarrow>


195 
wp\<^sub>t c (\<lambda>s'. wp\<^sub>t ?w Q s' \<and> its b c s' < n) s"


196 
unfolding wpt_def by (metis WhileE its_Suc lessI)


197 
note strengthen_pre[OF this While]


198 
} note hoaret.While[OF this]


199 
moreover have "\<forall>s. wp\<^sub>t ?w Q s \<and> \<not> bval b s \<longrightarrow> Q s" by (auto simp add:wpt_def)


200 
ultimately show ?case by(rule weaken_post)


201 
qed


202 


203 


204 
text{*\noindent In the @{term While}case, @{const its} provides the obvious


205 
termination argument.


206 


207 
The actual completeness theorem follows directly, in the same manner


208 
as for partial correctness: *}


209 


210 
theorem hoaret_complete: "\<Turnstile>\<^sub>t {P}c{Q} \<Longrightarrow> \<turnstile>\<^sub>t {P}c{Q}"


211 
apply(rule strengthen_pre[OF _ wpt_is_pre])


212 
apply(auto simp: hoare_tvalid_def hoare_valid_def wpt_def)


213 
done


214 


215 
end
