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.

# Homework 10

This is the task corresponding to homework 10.

## Resources

### Definitions File

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 Aassign ("(_ ::= _)" [1000, 61] 61)
notation Aseq ("_;;/ _"  [60, 61] 60)
notation Aif ("(IF _/ THEN _/ ELSE _)"  [0, 0, 61] 61)
end

bundle COM begin
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

### Template File

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

### Check File

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

Terms and Conditions