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 06

This task corresponds to homework 06.

Resources

Definitions File

theory Defs
imports "IMP.Wp_Demo" "IMP.Small_Step"
begin

end

Template File

theory Submission
imports Defs
begin

definition "square \<equiv>
''z'' ::= N 1;;
''a'' ::= N 0;;
WHILE Less (N 0) (V ''n'') DO (
''a'' ::= Plus (V ''a'') (V ''z'');;
''z'' ::= Plus (V ''z'') (N 2);;
''n'' ::= Plus (V ''n'') (N (-1))
)"

theorem square_correct: "s ''n'' \<equiv> n \<Longrightarrow> n \<ge> 0 \<Longrightarrow> wlp square (\<lambda>s'. let a = s' ''a'' in a = n*n) s"
sorry

fun cfg_step :: "com * state \<Rightarrow> com * state" where
"cfg_step _ = undefined"

theorem small_step_cfg_step: "cs \<rightarrow> cs' \<Longrightarrow> cfg_step cs = cs'"
sorry

theorem final_cfg_step: "final cs \<Longrightarrow> cfg_step cs = cs"
sorry

fun cfg_steps :: "nat \<Rightarrow> com * state \<Rightarrow> com * state" where
"cfg_steps 0 cs = cs" |
"cfg_steps (Suc n) cs = cfg_steps n (cfg_step cs)"

theorem small_steps_cfg_steps:
"cs \<rightarrow>* cs' \<Longrightarrow> \<exists>n. cfg_steps n cs = cs'"
sorry

theorem cfg_steps_small_steps:
"cfg_steps n cs = cs' \<Longrightarrow> cs \<rightarrow>* cs'"
sorry

corollary cfg_steps_correct:
"cs \<rightarrow>* cs' \<longleftrightarrow> (\<exists>n. cfg_steps n cs = cs')"
by (metis small_steps_cfg_steps cfg_steps_small_steps)

definition
"is_sim R step step' \<equiv> \<forall>a b a'. R a b \<and> step a a' \<longrightarrow> (\<exists>b'. R a' b' \<and> step' b b')"

lemma is_sim_star:
assumes "is_sim R step step'" "R a b" "step\<^sup>*\<^sup>* a a'"
shows "\<exists>b'. R a' b' \<and> step'\<^sup>*\<^sup>* b b'"
sorry

inductive terminating for step where
"terminating step x"

theorem terminating_simulation:
assumes "is_sim R step step'" "terminating step' b" "R a b"
shows "terminating step a"
sorry

theorem wlp_whileI':
assumes INIT: "I s\<^sub>0"
assumes STEP: "\<And>s. I s \<Longrightarrow> (if bval b s then wlp c I s else Q s)"
shows "wlp (WHILE b DO c) Q s\<^sub>0"
sorry

end

Check File

theory Check
imports Submission
begin

theorem square_correct: "s ''n'' \<equiv> n \<Longrightarrow> n \<ge> 0 \<Longrightarrow> wlp square (\<lambda>s'. let a = s' ''a'' in a = n*n) s"
by (rule Submission.square_correct)

theorem small_step_cfg_step: "cs \<rightarrow> cs' \<Longrightarrow> cfg_step cs = cs'"
by (rule Submission.small_step_cfg_step)

theorem final_cfg_step: "final cs \<Longrightarrow> cfg_step cs = cs"
by (rule Submission.final_cfg_step)

theorem small_steps_cfg_steps:
"cs \<rightarrow>* cs' \<Longrightarrow> \<exists>n. cfg_steps n cs = cs'"
by (rule Submission.small_steps_cfg_steps)

theorem cfg_steps_small_steps:
"cfg_steps n cs = cs' \<Longrightarrow> cs \<rightarrow>* cs'"
by (rule Submission.cfg_steps_small_steps)

theorem terminating_simulation:
assumes "is_sim R step step'" "terminating step' b" "R a b"
shows "terminating step a"
using assms by (rule Submission.terminating_simulation)

theorem wlp_whileI':
assumes INIT: "I s\<^sub>0"
assumes STEP: "\<And>s. I s \<Longrightarrow> (if bval b s then wlp c I s else Q s)"
shows "wlp (WHILE b DO c) Q s\<^sub>0"
using assms by (rule Submission.wlp_whileI')

end

Terms and Conditions