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 Main
begin
type_synonym vname = string
type_synonym val = int
type_synonym state = "vname \<Rightarrow> val"
datatype aexp
= N int | V vname | Plus aexp aexp
| Minus aexp aexp | Mul aexp aexp | Div aexp aexp
fun aval :: "aexp \<Rightarrow> state \<Rightarrow> val" where
"aval (N n) s = n" |
"aval (V x) s = s x" |
"aval (Plus a\<^sub>1 a\<^sub>2) s = aval a\<^sub>1 s + aval a\<^sub>2 s" |
"aval (Div a\<^sub>1 a\<^sub>2) s = aval a\<^sub>1 s div aval a\<^sub>2 s" |
"aval (Mul a\<^sub>1 a\<^sub>2) s = aval a\<^sub>1 s * aval a\<^sub>2 s" |
"aval (Minus a\<^sub>1 a\<^sub>2) s = aval a\<^sub>1 s - aval a\<^sub>2 s"
definition null_state ("<>") where
"null_state \<equiv> \<lambda>x. 0"
syntax
"_State" :: "updbinds => 'a" ("<_>")
translations
"_State ms" == "_Update <> ms"
"_State (_updbinds b bs)" <= "_Update (_State b) bs"
datatype bexp = Bc bool | Not bexp | And bexp bexp | Less aexp aexp
fun bval :: "bexp \<Rightarrow> state \<Rightarrow> bool" where
"bval (Bc v) s = v" |
"bval (Not b) s = (\<not> bval b s)" |
"bval (And b\<^sub>1 b\<^sub>2) s = (bval b\<^sub>1 s \<and> bval b\<^sub>2 s)" |
"bval (Less a\<^sub>1 a\<^sub>2) s = (aval a\<^sub>1 s < aval a\<^sub>2 s)"
datatype
com = SKIP
| Assign vname aexp ("_ ::= _" [1000, 61] 61)
| Seq com com ("_;;/ _" [60, 61] 60)
| If bexp com com ("(IF _/ THEN _/ ELSE _)" [0, 0, 61] 61)
| While bexp com ("(WHILE _/ DO _)" [0, 61] 61)
inductive
big_step :: "com \<times> state \<Rightarrow> state \<Rightarrow> bool" (infix "\<Rightarrow>" 55)
where
Skip: "(SKIP,s) \<Rightarrow> s" |
Assign: "(x ::= a,s) \<Rightarrow> s(x := aval a s)" |
Seq: "\<lbrakk> (c\<^sub>1,s\<^sub>1) \<Rightarrow> s\<^sub>2; (c\<^sub>2,s\<^sub>2) \<Rightarrow> s\<^sub>3 \<rbrakk> \<Longrightarrow> (c\<^sub>1;;c\<^sub>2, s\<^sub>1) \<Rightarrow> s\<^sub>3" |
IfTrue: "\<lbrakk> bval b s; (c\<^sub>1,s) \<Rightarrow> t \<rbrakk> \<Longrightarrow> (IF b THEN c\<^sub>1 ELSE c\<^sub>2, s) \<Rightarrow> t" |
IfFalse: "\<lbrakk> \<not>bval b s; (c\<^sub>2,s) \<Rightarrow> t \<rbrakk> \<Longrightarrow> (IF b THEN c\<^sub>1 ELSE c\<^sub>2, s) \<Rightarrow> t" |
WhileFalse: "\<not>bval b s \<Longrightarrow> (WHILE b DO c,s) \<Rightarrow> s" |
WhileTrue:
"\<lbrakk> bval b s\<^sub>1; (c,s\<^sub>1) \<Rightarrow> s\<^sub>2; (WHILE b DO c, s\<^sub>2) \<Rightarrow> s\<^sub>3 \<rbrakk>
\<Longrightarrow> (WHILE b DO c, s\<^sub>1) \<Rightarrow> s\<^sub>3"
code_pred big_step .
declare big_step.intros [intro]
lemmas big_step_induct = big_step.induct[split_format(complete)]
thm big_step_induct
inductive_cases SkipE[elim!]: "(SKIP,s) \<Rightarrow> t"
thm SkipE
inductive_cases AssignE[elim!]: "(x ::= a,s) \<Rightarrow> t"
thm AssignE
inductive_cases SeqE[elim!]: "(c1;;c2,s1) \<Rightarrow> s3"
thm SeqE
inductive_cases IfE[elim!]: "(IF b THEN c1 ELSE c2,s) \<Rightarrow> t"
thm IfE
inductive_cases WhileE[elim]: "(WHILE b DO c,s) \<Rightarrow> t"
thm WhileE
theorem big_step_determ: "\<lbrakk> (c,s) \<Rightarrow> t; (c,s) \<Rightarrow> u \<rbrakk> \<Longrightarrow> u = t"
by (induction arbitrary: u rule: big_step.induct) blast+
abbreviation
equiv_c :: "com \<Rightarrow> com \<Rightarrow> bool" (infix "\<sim>" 50) where
"c \<sim> c' \<equiv> (\<forall>s t. (c,s) \<Rightarrow> t = (c',s) \<Rightarrow> t)"
lemma unfold_while:
"(WHILE b DO c) \<sim> (IF b THEN c;; WHILE b DO c ELSE SKIP)" (is "?w \<sim> ?iw")
proof -
have "(?iw, s) \<Rightarrow> t" if assm: "(?w, s) \<Rightarrow> t" for s t
proof -
from assm show ?thesis
proof cases
case WhileFalse
thus ?thesis by blast
next
case WhileTrue
from \<open>bval b s\<close> \<open>(?w, s) \<Rightarrow> t\<close> obtain s' where
"(c, s) \<Rightarrow> s'" and "(?w, s') \<Rightarrow> t" by auto
hence "(c;; ?w, s) \<Rightarrow> t" by (rule Seq)
with \<open>bval b s\<close> show ?thesis by (rule IfTrue)
qed
qed
moreover
have "(?w, s) \<Rightarrow> t" if assm: "(?iw, s) \<Rightarrow> t" for s t
proof -
from assm show ?thesis
proof cases
case IfFalse
hence "s = t" using \<open>(?iw, s) \<Rightarrow> t\<close> by blast
thus ?thesis using \<open>\<not>bval b s\<close> by blast
next
case IfTrue
from \<open>(c;; ?w, s) \<Rightarrow> t\<close> obtain s' where
"(c, s) \<Rightarrow> s'" and "(?w, s') \<Rightarrow> t" by auto
with \<open>bval b s\<close> show ?thesis by (rule WhileTrue)
qed
qed
ultimately
show ?thesis by blast
qed
paragraph "Hoare"
type_synonym assn = "state \<Rightarrow> bool"
abbreviation state_subst :: "state \<Rightarrow> aexp \<Rightarrow> vname \<Rightarrow> state"
("_[_'/_]" [1000,0,0] 999)
where "s[a/x] == s(x := aval a s)"
paragraph "Partial correctness"
definition
hoare_valid :: "assn \<Rightarrow> com \<Rightarrow> assn \<Rightarrow> bool" ("\<Turnstile> {(1_)}/ (_)/ {(1_)}" 50) where
"\<Turnstile> {P}c{Q} = (\<forall>s t. P s \<and> (c,s) \<Rightarrow> t \<longrightarrow> Q t)"
inductive
hoare :: "assn \<Rightarrow> com \<Rightarrow> assn \<Rightarrow> bool" ("\<turnstile> ({(1_)}/ (_)/ {(1_)})" 50)
where
Skip: "\<turnstile> {P} SKIP {P}" |
Assign: "\<turnstile> {\<lambda>s. P(s[a/x])} x::=a {P}" |
Seq: "\<lbrakk> \<turnstile> {P} c\<^sub>1 {Q}; \<turnstile> {Q} c\<^sub>2 {R} \<rbrakk>
\<Longrightarrow> \<turnstile> {P} c\<^sub>1;;c\<^sub>2 {R}" |
If: "\<lbrakk> \<turnstile> {\<lambda>s. P s \<and> bval b s} c\<^sub>1 {Q}; \<turnstile> {\<lambda>s. P s \<and> \<not> bval b s} c\<^sub>2 {Q} \<rbrakk>
\<Longrightarrow> \<turnstile> {P} IF b THEN c\<^sub>1 ELSE c\<^sub>2 {Q}" |
While: "\<turnstile> {\<lambda>s. P s \<and> bval b s} c {P} \<Longrightarrow>
\<turnstile> {P} WHILE b DO c {\<lambda>s. P s \<and> \<not> bval b s}" |
conseq: "\<lbrakk> \<forall>s. P' s \<longrightarrow> P s; \<turnstile> {P} c {Q}; \<forall>s. Q s \<longrightarrow> Q' s \<rbrakk>
\<Longrightarrow> \<turnstile> {P'} c {Q'}"
lemmas [simp] = hoare.Skip hoare.Assign hoare.Seq If
lemmas [intro!] = hoare.Skip hoare.Assign hoare.Seq hoare.If
lemma strengthen_pre:
"\<lbrakk> \<forall>s. P' s \<longrightarrow> P s; \<turnstile> {P} c {Q} \<rbrakk> \<Longrightarrow> \<turnstile> {P'} c {Q}"
by (blast intro: conseq)
lemma weaken_post:
"\<lbrakk> \<turnstile> {P} c {Q}; \<forall>s. Q s \<longrightarrow> Q' s \<rbrakk> \<Longrightarrow> \<turnstile> {P} c {Q'}"
by (blast intro: conseq)
lemma Assign': "\<forall>s. P s \<longrightarrow> Q(s[a/x]) \<Longrightarrow> \<turnstile> {P} x ::= a {Q}"
by (simp add: strengthen_pre[OF _ Assign])
lemma While':
assumes "\<turnstile> {\<lambda>s. P s \<and> bval b s} c {P}" and "\<forall>s. P s \<and> \<not> bval b s \<longrightarrow> Q s"
shows "\<turnstile> {P} WHILE b DO c {Q}"
by(rule weaken_post[OF While[OF assms(1)] assms(2)])
definition wp :: "com \<Rightarrow> assn \<Rightarrow> assn" where
"wp c Q = (\<lambda>s. \<forall>t. (c,s) \<Rightarrow> t \<longrightarrow> Q t)"
lemma wp_SKIP[simp]: "wp SKIP Q = Q"
by (rule ext) (auto simp: wp_def)
lemma wp_Ass[simp]: "wp (x::=a) Q = (\<lambda>s. Q(s[a/x]))"
by (rule ext) (auto simp: wp_def)
lemma wp_Seq[simp]: "wp (c\<^sub>1;;c\<^sub>2) Q = wp c\<^sub>1 (wp c\<^sub>2 Q)"
by (rule ext) (auto simp: wp_def)
lemma wp_If[simp]:
"wp (IF b THEN c\<^sub>1 ELSE c\<^sub>2) Q =
(\<lambda>s. if bval b s then wp c\<^sub>1 Q s else wp c\<^sub>2 Q s)"
by (rule ext) (auto simp: wp_def)
lemma wp_While_If:
"wp (WHILE b DO c) Q s =
wp (IF b THEN c;;WHILE b DO c ELSE SKIP) Q s"
unfolding wp_def by (metis unfold_while)
lemma wp_While_True[simp]: "bval b s \<Longrightarrow>
wp (WHILE b DO c) Q s = wp (c;; WHILE b DO c) Q s"
by(simp add: wp_While_If)
lemma wp_While_False[simp]: "\<not> bval b s \<Longrightarrow> wp (WHILE b DO c) Q s = Q s"
by(simp add: wp_While_If)
lemma wp_is_pre: "\<turnstile> {wp c Q} c {Q}"
proof(induction c arbitrary: Q)
case If thus ?case by(auto intro: hoare.conseq)
next
case (While b c)
let ?w = "WHILE b DO c"
show "\<turnstile> {wp ?w Q} ?w {Q}"
proof(rule While')
show "\<turnstile> {\<lambda>s. wp ?w Q s \<and> bval b s} c {wp ?w Q}"
proof(rule strengthen_pre[OF _ While.IH])
show "\<forall>s. wp ?w Q s \<and> bval b s \<longrightarrow> wp c (wp ?w Q) s" by auto
qed
show "\<forall>s. wp ?w Q s \<and> \<not> bval b s \<longrightarrow> Q s" by auto
qed
qed auto
lemma hoare_complete: assumes "\<Turnstile> {P}c{Q}" shows "\<turnstile> {P}c{Q}"
proof(rule strengthen_pre)
show "\<forall>s. P s \<longrightarrow> wp c Q s" using assms
by (auto simp: hoare_valid_def wp_def)
show "\<turnstile> {wp c Q} c {Q}" by(rule wp_is_pre)
qed
paragraph "Annotated commands"
datatype acom =
Askip ("SKIP") |
Aassign vname aexp ("(_ ::= _)" [1000, 61] 61) |
Aseq acom acom ("_;;/ _" [60, 61] 60) |
Aif bexp acom acom ("(IF _/ THEN _/ ELSE _)" [0, 0, 61] 61) |
Awhile assn bexp acom
("({_}/ WHILE _/ DO _)" [0, 0, 61] 61)
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 ACOM
fun strip :: "acom \<Rightarrow> com" where
"strip SKIP = com.SKIP" |
"strip (x ::= a) = com.Assign x a" |
"strip (C\<^sub>1;; C\<^sub>2) = com.Seq (strip C\<^sub>1) (strip C\<^sub>2)" |
"strip (IF b THEN C\<^sub>1 ELSE C\<^sub>2) = com.If b (strip C\<^sub>1) (strip C\<^sub>2)" |
"strip ({_} WHILE b DO C) = com.While b (strip C)"
paragraph "VCG for partial correctness"
fun pre :: "acom \<Rightarrow> assn \<Rightarrow> assn" where
"pre SKIP Q = Q" |
"pre (x ::= a) Q = (\<lambda>s. Q(s(x := aval a s)))" |
"pre (C\<^sub>1;; C\<^sub>2) Q = pre C\<^sub>1 (pre C\<^sub>2 Q)" |
"pre (IF b THEN C\<^sub>1 ELSE C\<^sub>2) Q =
(\<lambda>s. if bval b s then pre C\<^sub>1 Q s else pre C\<^sub>2 Q s)" |
"pre ({I} WHILE b DO C) Q = I"
fun vc :: "acom \<Rightarrow> assn \<Rightarrow> bool" where
"vc SKIP Q = True" |
"vc (x ::= a) Q = True" |
"vc (C\<^sub>1;; C\<^sub>2) Q = (vc C\<^sub>1 (pre C\<^sub>2 Q) \<and> vc C\<^sub>2 Q)" |
"vc (IF b THEN C\<^sub>1 ELSE C\<^sub>2) Q = (vc C\<^sub>1 Q \<and> vc C\<^sub>2 Q)" |
"vc ({I} WHILE b DO C) Q =
((\<forall>s. (I s \<and> bval b s \<longrightarrow> pre C I s) \<and>
(I s \<and> \<not> bval b s \<longrightarrow> Q s)) \<and>
vc C I)"
lemma vc_sound: "vc C Q \<Longrightarrow> \<turnstile> {pre C Q} strip C {Q}"
proof(induction C arbitrary: Q)
case (Awhile I b C)
show ?case
proof(simp, rule While')
from \<open>vc (Awhile I b C) Q\<close>
have vc: "vc C I" and IQ: "\<forall>s. I s \<and> \<not> bval b s \<longrightarrow> Q s" and
pre: "\<forall>s. I s \<and> bval b s \<longrightarrow> pre C I s" by simp_all
have "\<turnstile> {pre C I} strip C {I}" by(rule Awhile.IH[OF vc])
with pre show "\<turnstile> {\<lambda>s. I s \<and> bval b s} strip C {I}"
by(rule strengthen_pre)
show "\<forall>s. I s \<and> \<not>bval b s \<longrightarrow> Q s" by(rule IQ)
qed
qed (auto intro: conseq)
corollary vc_sound':
"\<lbrakk> vc C Q; \<forall>s. P s \<longrightarrow> pre C Q s \<rbrakk> \<Longrightarrow> \<turnstile> {P} strip C {Q}"
by (metis strengthen_pre vc_sound)
unbundle COM
paragraph "Program:"
definition neq :: "aexp \<Rightarrow> aexp \<Rightarrow> bexp" where
"neq a\<^sub>1 a\<^sub>2 \<equiv> Not (And (Not (Less a\<^sub>1 a\<^sub>2)) (Not (Less a\<^sub>2 a\<^sub>1)))"
lemma bval_neq_eq[simp]: "bval (neq a\<^sub>1 a\<^sub>2) s = (aval a\<^sub>1 s \<noteq> aval a\<^sub>2 s)"
unfolding neq_def by auto
definition "EGGT :: com \<equiv>
''old_r'' ::= V ''a'';;
''r'' ::= V ''b'';;
''old_s'' ::= N 1;;
''s'' ::= N 0;;
''old_t'' ::= N 0;;
''t'' ::= N 1;;
WHILE neq (V ''r'') (N 0) DO (
''quotient'' ::= Div (V ''old_r'') (V ''r'');;
''tmp'' ::= V ''old_r'';;
''old_r'' ::= V ''r'';;
''r'' ::= Minus (V ''tmp'') (Mul (V ''quotient'') (V ''r''));;
''tmp'' ::= V ''old_s'';;
''old_s'' ::= V ''s'';;
''s'' ::= Minus (V ''tmp'') (Mul (V ''quotient'') (V ''s''));;
''tmp'' ::= V ''old_t'';;
''old_t'' ::= V ''t'';;
''t'' ::= Minus (V ''tmp'') (Mul (V ''quotient'') (V ''t''))
)"
end
theory Submission
imports Defs
begin
unbundle ACOM
definition AEGGT_annot :: "state \<Rightarrow> acom" where
lemma AEGGT_annot_strip: "strip (AEGGT_annot s\<^sub>0) = EGGT"
sorry
theorem EGGT_correct: "\<turnstile>
{\<lambda>s. s = s\<^sub>0 \<and> s\<^sub>0 ''a'' > 0 \<and> s\<^sub>0 ''b'' > 0}
EGGT
{\<lambda>s. s ''old_r'' = gcd (s\<^sub>0 ''a'') (s\<^sub>0 ''b'')
\<and> gcd (s\<^sub>0 ''a'') (s\<^sub>0 ''b'') = s\<^sub>0 ''a'' * s ''old_s'' + s\<^sub>0 ''b'' * s ''old_t'' }"
sorry
end
theory Check
imports Submission
begin
lemma AEGGT_annot_strip: "strip (AEGGT_annot s\<^sub>0) = EGGT"
by (rule Submission.AEGGT_annot_strip)
theorem EGGT_correct: "\<turnstile>
{\<lambda>s. s = s\<^sub>0 \<and> s\<^sub>0 ''a'' > 0 \<and> s\<^sub>0 ''b'' > 0}
EGGT
{\<lambda>s. s ''old_r'' = gcd (s\<^sub>0 ''a'') (s\<^sub>0 ''b'')
\<and> gcd (s\<^sub>0 ''a'') (s\<^sub>0 ''b'') = s\<^sub>0 ''a'' * s ''old_s'' + s\<^sub>0 ''b'' * s ''old_t'' }"
by (rule Submission.EGGT_correct)
end