Quelle Hoare_Total_EX2.thy Sprache: Isabelle

(* Author: Tobias Nipkow *)

subsubsection "Hoare Logic for Total Correctness With Logical Variables"

theory Hoare_Total_EX2
imports Hoare
begin

text\<open>This is the standard set of rules that you find in many publications.
In the while-rule, a logical variable is needed to remember the pre-value
of the variant (an expression that decreases by one with each iteration).
In this theory, logical variables are modeled explicitly.
A simpler (but not quite as flexible) approach is found in theory \<open>Hoare_Total_EX\<close>:
pre and post-condition are connected via a universally quantified HOL variable.\<close>

type_synonym lvname = string
type_synonym assn2 = "(lvname \ nat) \ state \ bool"

definition hoare_tvalid :: "assn2 \ com \ assn2 \ bool"
  (\<open>\<Turnstile>\<^sub>t {(1_)}/ (_)/ {(1_)}\<close> 50) where
"\\<^sub>t {P}c{Q} \ (\l s. P l s \ (\t. (c,s) \ t \ Q l t))"

inductive
  hoaret :: "assn2 \ com \ assn2 \ bool" (\\\<^sub>t ({(1_)}/ (_)/ {(1_)})\ 50)
where

Skip:  "\\<^sub>t {P} SKIP {P}" |

Assign:  "\\<^sub>t {\l s. P l (s[a/x])} x::=a {P}" |

Seq: "\ \\<^sub>t {P\<^sub>1} c\<^sub>1 {P\<^sub>2}; \\<^sub>t {P\<^sub>2} c\<^sub>2 {P\<^sub>3} \ \ \\<^sub>t {P\<^sub>1} c\<^sub>1;;c\<^sub>2 {P\<^sub>3}" |

If: "\ \\<^sub>t {\l s. P l s \ bval b s} c\<^sub>1 {Q}; \\<^sub>t {\l s. P l s \ \ bval b s} c\<^sub>2 {Q} \
  \<Longrightarrow> \<turnstile>\<^sub>t {P} IF b THEN c\<^sub>1 ELSE c\<^sub>2 {Q}" |

While:
  "\ \\<^sub>t {\l. P (l(x := Suc(l(x))))} c {P};
     \<forall>l s. l x > 0 \<and> P l s \<longrightarrow> bval b s;
     \<forall>l s. l x = 0 \<and> P l s \<longrightarrow> \<not> bval b s \<rbrakk>
   \<Longrightarrow> \<turnstile>\<^sub>t {\<lambda>l s. \<exists>n. P (l(x:=n)) s} WHILE b DO c {\<lambda>l s. P (l(x := 0)) s}" |

conseq: "\ \l s. P' l s \ P l s; \\<^sub>t {P}c{Q}; \l s. Q l s \ Q' l s \ \
           \<turnstile>\<^sub>t {P'}c{Q'}"

text\<open>Building in the consequence rule:\<close>

lemma strengthen_pre:
  "\ \l s. P' l s \ P l s; \\<^sub>t {P} c {Q} \ \ \\<^sub>t {P'} c {Q}"
by (metis conseq)

lemma weaken_post:
  "\ \\<^sub>t {P} c {Q}; \l s. Q l s \ Q' l s \ \ \\<^sub>t {P} c {Q'}"
by (metis conseq)

lemma Assign': "\l s. P l s \ Q l (s[a/x]) \ \\<^sub>t {P} x ::= a {Q}"
by (simp add: strengthen_pre[OF _ Assign])

text\<open>The soundness theorem:\<close>

theorem hoaret_sound: "\\<^sub>t {P}c{Q} \ \\<^sub>t {P}c{Q}"
proof(unfold hoare_tvalid_def, induction rule: hoaret.induct)
  case (While P x c b)
  have "\ l x = n; P l s \ \ \t. (WHILE b DO c, s) \ t \ P (l(x := 0)) t" for n l s
  proof(induction "n" arbitrary: l s)
    case 0 thus ?case using While.hyps(3) WhileFalse
      by (metis fun_upd_triv)
  next
    case Suc
    thus ?case using While.IH While.hyps(2) WhileTrue
      by (metis fun_upd_same fun_upd_triv fun_upd_upd zero_less_Suc)
  qed
  thus ?case by fastforce
next
  case If thus ?case by auto blast
qed fastforce+

definition wpt :: "com \ assn2 \ assn2" (\wp\<^sub>t\) where
"wp\<^sub>t c Q = (\l s. \t. (c,s) \ t \ Q l t)"

lemma [simp]: "wp\<^sub>t SKIP Q = Q"
by(auto intro!: ext simp: wpt_def)

lemma [simp]: "wp\<^sub>t (x ::= e) Q = (\l s. Q l (s(x := aval e s)))"
by(auto intro!: ext simp: wpt_def)

lemma wpt_Seq[simp]: "wp\<^sub>t (c\<^sub>1;;c\<^sub>2) Q = wp\<^sub>t c\<^sub>1 (wp\<^sub>t c\<^sub>2 Q)"
by (auto simp: wpt_def fun_eq_iff)

lemma [simp]:
"wp\<^sub>t (IF b THEN c\<^sub>1 ELSE c\<^sub>2) Q = (\l s. wp\<^sub>t (if bval b s then c\<^sub>1 else c\<^sub>2) Q l s)"
by (auto simp: wpt_def fun_eq_iff)

text\<open>Function \<open>wpw\<close> computes the weakest precondition of a While-loop
that is unfolded a fixed number of times.\<close>

fun wpw :: "bexp \ com \ nat \ assn2 \ assn2" where
"wpw b c 0 Q l s = (\ bval b s \ Q l s)" |
"wpw b c (Suc n) Q l s = (bval b s \ (\s'. (c,s) \ s' \ wpw b c n Q l s'))"

lemma WHILE_Its:
  "(WHILE b DO c,s) \ t \ Q l t \ \n. wpw b c n Q l s"
proof(induction "WHILE b DO c" s t arbitrary: l rule: big_step_induct)
  case WhileFalse thus ?case using wpw.simps(1) by blast
next
  case WhileTrue show ?case
    using wpw.simps(2) WhileTrue(1,2) WhileTrue(5)[OF WhileTrue(6)] by blast
qed

definition support :: "assn2 \ string set" where
"support P = {x. \l1 l2 s. (\y. y \ x \ l1 y = l2 y) \ P l1 s \ P l2 s}"

lemma support_wpt: "support (wp\<^sub>t c Q) \ support Q"
by(simp add: support_def wpt_def) blast

lemma support_wpw0: "support (wpw b c n Q) \ support Q"
proof(induction n)
  case 0 show ?case by (simp add: support_def) blast
next
  case Suc
  have 1: "support (\l s. A s \ B l s) \ support B" for A B
    by(auto simp: support_def)
  have 2: "support (\l s. \s'. A s s' \ B l s') \ support B" for A B
    by(auto simp: support_def) blast+
  from Suc 1 2 show ?case by simp (meson order_trans)
qed

lemma support_wpw_Un:
  "support (%l. wpw b c (l x) Q l) \ insert x (UN n. support(wpw b c n Q))"
using support_wpw0[of b c _ Q]
apply(auto simp add: support_def subset_iff)
apply metis
apply metis
done

lemma support_wpw: "support (%l. wpw b c (l x) Q l) \ insert x (support Q)"
using support_wpw0[of b c _ Q] support_wpw_Un[of b c _ Q]
by blast

lemma assn2_lupd: "x \ support Q \ Q (l(x:=n)) = Q l"
by(simp add: support_def fun_upd_other fun_eq_iff)
  (metis (no_types, lifting) fun_upd_def)

abbreviation "new Q \ SOME x. x \ support Q"

lemma wpw_lupd: "x \ support Q \ wpw b c n Q (l(x := u)) = wpw b c n Q l"
by(induction n) (auto simp: assn2_lupd fun_eq_iff)

lemma wpt_is_pre: "finite(support Q) \ \\<^sub>t {wp\<^sub>t c Q} c {Q}"
proof (induction c arbitrary: Q)
  case SKIP show ?case by (auto intro:hoaret.Skip)
next
  case Assign show ?case by (auto intro:hoaret.Assign)
next
  case (Seq c1 c2) show ?case
    by (auto intro:hoaret.Seq Seq finite_subset[OF support_wpt])
next
  case If thus ?case by (auto intro:hoaret.If hoaret.conseq)
next
  case (While b c)
  let ?x = "new Q"
  have "\x. x \ support Q" using While.prems infinite_UNIV_listI
    using ex_new_if_finite by blast
  hence [simp]: "?x \ support Q" by (rule someI_ex)
  let ?w = "WHILE b DO c"
  have fsup: "finite (support (\l. wpw b c (l x) Q l))" for x
    using finite_subset[OF support_wpw] While.prems by simp
  have c1: "\l s. wp\<^sub>t ?w Q l s \ (\n. wpw b c n Q l s)"
    unfolding wpt_def by (metis WHILE_Its)
  have c2: "\l s. l ?x = 0 \ wpw b c (l ?x) Q l s \ \ bval b s"
    by (simp cong: conj_cong)
  have w2: "\l s. 0 < l ?x \ wpw b c (l ?x) Q l s \ bval b s"
    by (auto simp: gr0_conv_Suc cong: conj_cong)
  have 1: "\l s. wpw b c (Suc(l ?x)) Q l s \
                  (\<exists>t. (c, s) \<Rightarrow> t \<and> wpw b c (l ?x) Q l t)"
    by simp
  have *: "\\<^sub>t {\l. wpw b c (Suc (l ?x)) Q l} c {\l. wpw b c (l ?x) Q l}"
    by(rule strengthen_pre[OF 1
          While.IH[of "\l. wpw b c (l ?x) Q l", unfolded wpt_def, OF fsup]])
  show ?case
  apply(rule conseq[OF _ hoaret.While[OF _ w2 c2]])
    apply (simp_all add: c1 * assn2_lupd wpw_lupd del: wpw.simps(2))
  done
qed

theorem hoaret_complete: "finite(support Q) \ \\<^sub>t {P}c{Q} \ \\<^sub>t {P}c{Q}"
apply(rule strengthen_pre[OF _ wpt_is_pre])
apply(auto simp: hoare_tvalid_def wpt_def)
done

text \<open>Two examples:\<close>

lemma "\\<^sub>t
{\<lambda>l s. l ''x'' = nat(s ''x'')}
WHILE Less (N 0) (V ''x'') DO ''x'' ::= Plus (V ''x'') (N (-1))
{\<lambda>l s. s ''x'' \<le> 0}"
apply(rule conseq)
prefer 2
apply(rule While[where P = "\l s. l ''x'' = nat(s ''x'')" and x = "''x''"])
   apply(rule Assign')
   apply auto
done

lemma "\\<^sub>t
{\<lambda>l s. l ''x'' = nat(s ''x'')}
WHILE Less (N 0) (V ''x'')
DO (''x'' ::= Plus (V ''x'') (N (-1));;
    (''y'' ::= V ''x'';;
     WHILE Less (N 0) (V ''y'') DO ''y'' ::= Plus (V ''y'') (N (-1))))
{\<lambda>l s. s ''x'' \<le> 0}"
apply(rule conseq)
prefer 2
apply(rule While[where P = "\l s. l ''x'' = nat(s ''x'')" and x = "''x''"])
   defer
   apply auto
apply(rule Seq)
prefer 2
apply(rule Seq)
  prefer 2
  apply(rule weaken_post)
   apply(rule_tac P = "\l s. l ''x'' = nat(s ''x'') \ l ''y'' = nat(s ''y'')" and x = "''y''" in While)
     apply(rule Assign')
     apply auto[4]
apply(rule Assign)
apply(rule Assign')
apply auto
done

end

quality93%

¤ Dauer der Verarbeitung: 0.4 Sekunden ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.