I agree Our site saves small pieces of text information (cookies) on your device in order to deliver better content and for statistical purposes. You can disable the usage of cookies by changing the settings of your browser. By browsing our website without changing the browser settings you grant us permission to store that information on your device.
theory Defs imports "HOL-IMP.VCG" "HOL-IMP.Hoare_Sound_Complete" "HOL-IMP.Hoare_Total" begin
bundle ACOM begin
no_notation SKIP ("SKIP")
no_notation Assign ("_ ::= _" [1000, 61] 61)
no_notation Seq ("_;;/ _" [60, 61] 60)
no_notation If ("(IF _/ THEN _/ ELSE _)" [0, 0, 61] 61)
notation Askip ("SKIP")
notation Aassign ("(_ ::= _)" [1000, 61] 61)
notation Aseq ("_;;/ _" [60, 61] 60)
notation Aif ("(IF _/ THEN _/ ELSE _)" [0, 0, 61] 61)
end
bundle COM begin
no_notation Askip ("SKIP")
no_notation Aassign ("(_ ::= _)" [1000, 61] 61)
no_notation Aseq ("_;;/ _" [60, 61] 60)
no_notation Aif ("(IF _/ THEN _/ ELSE _)" [0, 0, 61] 61)
notation SKIP ("SKIP")
notation Assign ("_ ::= _" [1000, 61] 61)
notation Seq ("_;;/ _" [60, 61] 60)
notation If ("(IF _/ THEN _/ ELSE _)" [0, 0, 61] 61)
end
unbundle COM
definition MUL :: com where
"MUL =
''z''::=N 0;;
''c''::=N 0;;
WHILE (Less (V ''c'') (V ''y'')) DO (
''z''::=Plus (V ''z'') (V ''x'');;
''c''::=Plus (V ''c'') (N 1))"
abbreviation "MUL_invar sorig s \<equiv>
s ''z'' = s ''x'' * s ''c'' \<and> s ''c'' \<le> s ''y'' \<and>
(\<forall>v. v\<notin>{''z'',''c''} \<longrightarrow> s v = sorig v)"
unbundle ACOM
definition MUL_annot :: "state \<Rightarrow> acom" where
"MUL_annot sorig =
''z''::=N 0;;
''c''::=N 0;;
{MUL_invar sorig} WHILE (Less (V ''c'') (V ''y'')) DO (
''z''::=Plus (V ''z'') (V ''x'');;
''c''::=Plus (V ''c'') (N 1))"
lemma MUL_annot_strip: "strip (MUL_annot sorig) = MUL"
unfolding MUL_def MUL_annot_def
by auto
theorem MUL_partially_correct:
"\<turnstile> {\<lambda>s. 0 \<le> s ''y'' \<and> s=sorig}
MUL
{\<lambda>s. s ''z'' = s ''x'' * s ''y'' \<and> (\<forall>v. v\<notin>{''z'',''c''} \<longrightarrow> s v = sorig v)}"
unfolding MUL_annot_strip[of sorig,symmetric]
by (rule vc_sound'; force simp add: MUL_annot_def algebra_simps)
unbundle COM
definition SQRT :: com where
"SQRT =
''r'' ::= N 0;;
''s'' ::= N 1;;
WHILE (Not (Less (V ''x'') (V ''s''))) DO (
''r'' ::= Plus (V ''r'') (N 1);;
''s'' ::= Plus (V ''s'') (V ''r'');;
''s'' ::= Plus (V ''s'') (V ''r'');;
''s'' ::= Plus (V ''s'') (N 1)
)"
abbreviation "SQRT_invar sorig s \<equiv>
s ''s'' = (s ''r'' + 1)^2
\<and> s ''r'' \<ge> 0 \<comment> \<open>We do not need this constraint for partial correctness\<close>
\<and> (s ''r'')^2 \<le> s ''x''
\<and> (\<forall>v. v\<notin>{''r'',''s''} \<longrightarrow> s v = sorig v)"
unbundle ACOM
definition SQRT_annot :: "state \<Rightarrow> acom" where
"SQRT_annot sorig =
''r'' ::= N 0;;
''s'' ::= N 1;;
{SQRT_invar sorig} WHILE (Not (Less (V ''x'') (V ''s''))) DO (
''r'' ::= Plus (V ''r'') (N 1);;
''s'' ::= Plus (V ''s'') (V ''r'');;
''s'' ::= Plus (V ''s'') (V ''r'');;
''s'' ::= Plus (V ''s'') (N 1)
)"
lemma SQRT_annot_strip: "strip (SQRT_annot sorig) = SQRT"
unfolding SQRT_annot_def SQRT_def
by auto
theorem SQRT_partially_correct:
"\<turnstile> {\<lambda>s. s=sorig \<and> s ''x'' \<ge> 0}
SQRT
{\<lambda>s. (s ''r'')^2 \<le> s ''x'' \<and> s ''x'' < (s ''r''+1)^2 \<and> (\<forall>v. v\<notin>{''s'',''r''} \<longrightarrow> s v = sorig v)}"
unfolding SQRT_annot_strip[of sorig, symmetric]
apply (rule vc_sound')
apply (force simp: SQRT_annot_def power2_eq_square algebra_simps)+
done
lemmas Seq_bwd = Hoare_Total.Seq[rotated]
unbundle COM
lemma IfT:
assumes "\<turnstile>\<^sub>t {P1} c\<^sub>1 {Q}" and "\<turnstile>\<^sub>t {P2} c\<^sub>2 {Q}"
shows "\<turnstile>\<^sub>t {\<lambda>s. (bval b s \<longrightarrow> P1 s) \<and> (\<not> bval b s \<longrightarrow> P2 s)} IF b THEN c\<^sub>1 ELSE c\<^sub>2 {Q}"
by (auto intro: assms hoaret.intros)
lemmas hoareT_rule[intro?] = Seq_bwd Hoare_Total.Assign Hoare_Total.Assign' IfT
theorem MUL_totally_correct:
"\<turnstile>\<^sub>t {\<lambda>s. 0 \<le> s ''y'' \<and> s=sorig}
MUL
{\<lambda>s. s ''z'' = s ''x'' * s ''y'' \<and> (\<forall>v. v\<notin>{''z'',''c''} \<longrightarrow> s v = sorig v)}"
unfolding MUL_def
by (rule hoareT_rule Hoare_Total.While_fun'[where P="MUL_invar sorig" and f="\<lambda>s. nat (s ''y'' - s ''c'')"]
| clarsimp simp add: algebra_simps [])+
theorem SQRT_totally_correct:
"\<turnstile>\<^sub>t {\<lambda>s. s=sorig \<and> s ''x'' \<ge> 0}
SQRT
{\<lambda>s. (s ''r'')^2 \<le> s ''x'' \<and> s ''x'' < (s ''r''+1)^2 \<and> (\<forall>v. v\<notin>{''s'',''r''} \<longrightarrow> s v = sorig v)}"
unfolding SQRT_def
by (rule hoareT_rule Hoare_Total.While_fun'[where P="SQRT_invar sorig" and f="\<lambda>s. nat (s ''x'' - s ''r''* s ''r'')"]
| clarsimp simp add: algebra_simps power2_eq_square [])+
end
theory Submission imports Defs begin
definition DIV :: com where
"DIV = undefined"
theorem DIV_correct:
"\<turnstile> {\<lambda>s. s=s\<^sub>0 \<and> s ''p'' > 0 \<and> s ''q'' > 0}
DIV
{\<lambda>s. s\<^sub>0 ''q'' * s ''n'' + s ''r'' = s\<^sub>0 ''p'' \<and> 0 \<le> s ''r'' \<and> s ''r'' < s\<^sub>0 ''q''}"
sorry
theorem DIV_t_correct:
"\<turnstile>\<^sub>t {\<lambda>s. s=s\<^sub>0 \<and> s ''p'' > 0 \<and> s ''q'' > 0}
DIV
{\<lambda>s. s\<^sub>0 ''q'' * s ''n'' + s ''r'' = s\<^sub>0 ''p'' \<and> s ''r'' < s\<^sub>0 ''q''}"
sorry
end
theory Check imports Submission begin
theorem DIV_correct:
"\<turnstile> {\<lambda>s. s=s\<^sub>0 \<and> s ''p'' > 0 \<and> s ''q'' > 0}
DIV
{\<lambda>s. s\<^sub>0 ''q'' * s ''n'' + s ''r'' = s\<^sub>0 ''p'' \<and> 0 \<le> s ''r'' \<and> s ''r'' < s\<^sub>0 ''q''}"
by (rule Submission.DIV_correct)
theorem DIV_t_correct:
"\<turnstile>\<^sub>t {\<lambda>s. s=s\<^sub>0 \<and> s ''p'' > 0 \<and> s ''q'' > 0}
DIV
{\<lambda>s. s\<^sub>0 ''q'' * s ''n'' + s ''r'' = s\<^sub>0 ''p'' \<and> s ''r'' < s\<^sub>0 ''q''}"
by (rule Submission.DIV_t_correct)
end