nemouchi
/
Orca2017
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

talk demo

This commit is contained in:
yakoub 2019-03-08 13:44:08 +00:00
parent 1e1ca2dc4b
commit 195be89bf9
1 changed files with 4 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
C-verifier/src/Examples/algorithms_presentation.thy
View File

@ -368,7 +368,7 @@ lemma swap_count_down_preserves_list:
apply rel_simp+
done
(*DEMO VCG step by step and Program annotation*)
(*DEMO VCG step by step and Program annotation WP*)
lemma EXAMPLE_vcg_step_by_step_wp:
assumes "r \<bowtie> x"
@ -411,6 +411,7 @@ lemma EXAMPLE_vcg_step_by_step_wp:
apply (metis gcd.commute gcd_diff1)+
done
(*DEMO VCG step by step and Program annotation SP*)
lemma EXAMPLE_vcg_step_by_step_sp:
assumes "r \<bowtie> x"
assumes "vwb_lens r" "vwb_lens x"
@ -462,6 +463,8 @@ apply (hoare_sp_rule_apply)
apply (metis gcd.commute gcd_diff1)+
done
(*DEMO VCG Proof Annotation*)
lemma EXAMPLE_vcg_step_by_step_proof_annotation:
assumes "r \<bowtie> x"
assumes "vwb_lens r" "vwb_lens x"
@ -469,8 +472,6 @@ lemma EXAMPLE_vcg_step_by_step_proof_annotation:
"\<lbrace>\<guillemotleft>b\<guillemotright> >\<^sub>u 0 \<and> \<guillemotleft>a\<guillemotright>>\<^sub>u 0\<rbrace>
r :== \<guillemotleft>a::int\<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>
VRT uop nat (bop max (&r) (&x))*)
WHILE \<not>(&r =\<^sub>u &x)
DO
IF &r >\<^sub>u &x