This commit is contained in:
Yakoub Nemouchi 2019-02-25 19:35:48 +00:00
parent adf28d8c4a
commit d10f2e31fb
2 changed files with 9 additions and 7 deletions

View File

@ -404,7 +404,7 @@ lemma gcd_correct_sp_H1_H3:
assumes "r \<bowtie> x"
assumes "vwb_lens r" "vwb_lens x"
shows
"\<lbrace>\<guillemotleft>b\<guillemotright> >\<^sub>u 0 \<and> \<guillemotleft>a\<guillemotright>>\<^sub>u 0\<rbrace>
"\<lbrace> \<guillemotleft>b\<guillemotright> >\<^sub>u 0 \<and> \<guillemotleft>a\<guillemotright>>\<^sub>u 0 \<rbrace>
r :== \<guillemotleft>a\<guillemotright>;
x :== \<guillemotleft>b\<guillemotright>;
INVAR &r >\<^sub>u0 \<and> &x >\<^sub>u 0 \<and> bop gcd (&r) (&x) =\<^sub>u bop gcd \<guillemotleft>a\<guillemotright> \<guillemotleft>b\<guillemotright>
@ -416,7 +416,7 @@ lemma gcd_correct_sp_H1_H3:
ELSE x :== (&x - &r)
FI
OD
\<lbrace>&r =\<^sub>u &x \<and> &r =\<^sub>u bop gcd \<guillemotleft>a\<guillemotright> \<guillemotleft>b\<guillemotright>\<rbrace>\<^sub>P"
\<lbrace> &r =\<^sub>u &x \<and> &r =\<^sub>u bop gcd \<guillemotleft>a\<guillemotright> \<guillemotleft>b\<guillemotright> \<rbrace>\<^sub>P"
apply (insert assms)
apply (vcg sp)
apply (auto simp: gcd_diff1_nat gcd_diff1)

View File

@ -245,8 +245,8 @@ lemma antiframe_prog_hoare_basic_weak:
assumes indep_g_l :"g \<bowtie> l"
assumes region :"g' \<subseteq>\<^sub>L g"
assumes modifies :"{&g', &l}:[PROG] = PROG" (*TODO: From algebraic laws of program of antiframe this assumption can be derived from {&g'}:[PROG] = PROG*)
assumes hoare : "\<lbrace>p\<rbrace>PROG\<lbrace>q\<rbrace>\<^sub>P"
shows "\<lbrace>p \<and> r\<rbrace>g':[PROG]\<lbrace>(\<exists>l \<bullet> q) \<and> (\<exists>g' \<bullet> r)\<rbrace>\<^sub>P"
assumes hoare : "\<lbrace>P\<rbrace>PROG\<lbrace>Q\<rbrace>\<^sub>P"
shows "\<lbrace>P \<and> R\<rbrace>MODIFY g' DO PROG OD\<lbrace>(\<exists>l \<bullet> Q) \<and> (\<exists>g' \<bullet> R)\<rbrace>\<^sub>P"
using vwb_lens_g vwb_lens_g' vwb_lens_l indep_g_l modifies hoare
unfolding lens_indep_def
apply (simp add:prog_rep_eq)
@ -1043,9 +1043,11 @@ lemma while_scp_invr_vrt_hoare_prog_sp:
subsection \<open>Hoare for while loop\<close>
lemma while_hoare_prog_basic:
assumes WF: "wf R"
assumes induct_step:"\<And>st. \<lbrace>b \<and> invar \<and> vari =\<^sub>u \<guillemotleft>st\<guillemotright>\<rbrace>body\<lbrace>invar \<and>(vari,\<guillemotleft>st\<guillemotright>)\<^sub>u\<in>\<^sub>u\<guillemotleft>R\<guillemotright>\<rbrace>\<^sub>P"
shows "\<lbrace>invar\<rbrace>WHILE b DO body OD\<lbrace>\<not>b \<and> invar\<rbrace>\<^sub>P"
assumes WF: " wf R "
assumes induct_step:" \<And>st. \<lbrace>b \<and> invar \<and> vari =\<^sub>u \<guillemotleft>st\<guillemotright>\<rbrace>
body
\<lbrace>invar \<and>(vari,\<guillemotleft>st\<guillemotright>)\<^sub>u\<in>\<^sub>u\<guillemotleft>R\<guillemotright>\<rbrace>\<^sub>P "
shows " \<lbrace>invar\<rbrace>WHILE b DO body OD\<lbrace>\<not>b \<and> invar\<rbrace>\<^sub>P "
unfolding while_lfp_prog_mu_prog
proof (rule pre_str_prog_hoare[where ps=invar,OF _ lfp_prog_hoare_prog[OF WF if_prog_mono_prog cond_prog_hoare_basic, of _ vari] ], goal_cases)
case 1