Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/sources/formale Sprachen/Isabelle/HOL/IMP/ (Beweissystem Isabelle Version 2025-1^©) Datei vom 16.11.2025 mit Größe 7 kB

Quelle Live_True.thy Sprache: Isabelle

(* Author: Tobias Nipkow *)

subsection "True Liveness Analysis"

theory Live_True
imports "HOL-Library.While_Combinator" Vars Big_Step
begin

subsubsection "Analysis"

fun L :: "com \ vname set \ vname set" where
"L SKIP X = X" |
"L (x ::= a) X = (if x \ X then vars a \ (X - {x}) else X)" |
"L (c\<^sub>1;; c\<^sub>2) X = L c\<^sub>1 (L c\<^sub>2 X)" |
"L (IF b THEN c\<^sub>1 ELSE c\<^sub>2) X = vars b \ L c\<^sub>1 X \ L c\<^sub>2 X" |
"L (WHILE b DO c) X = lfp(\Y. vars b \ X \ L c Y)"

lemma L_mono: "mono (L c)"
proof-
  have "X \ Y \ L c X \ L c Y" for X Y
  proof(induction c arbitrary: X Y)
    case (While b c)
    show ?case
    proof(simp, rule lfp_mono)
      fix Z show "vars b \ X \ L c Z \ vars b \ Y \ L c Z"
        using While by auto
    qed
  next
    case If thus ?case by(auto simp: subset_iff)
  qed auto
  thus ?thesis by(rule monoI)
qed

lemma mono_union_L:
  "mono (\Y. X \ L c Y)"
using L_mono unfolding mono_def by (metis (no_types) order_eq_iff set_eq_subset sup_mono)

lemma L_While_unfold:
  "L (WHILE b DO c) X = vars b \ X \ L c (L (WHILE b DO c) X)"
by(metis lfp_unfold[OF mono_union_L] L.simps(5))

lemma L_While_pfp: "L c (L (WHILE b DO c) X) \ L (WHILE b DO c) X"
using L_While_unfold by blast

lemma L_While_vars: "vars b \ L (WHILE b DO c) X"
using L_While_unfold by blast

lemma L_While_X: "X \ L (WHILE b DO c) X"
using L_While_unfold by blast

text\<open>Disable \<open>L WHILE\<close> equation and reason only with \<open>L WHILE\<close> constraints:\<close>
declare L.simps(5)[simp del]

subsubsection "Correctness"

theorem L_correct:
  "(c,s) \ s' \ s = t on L c X \
  \<exists> t'. (c,t) \<Rightarrow> t' & s' = t' on X"
proof (induction arbitrary: X t rule: big_step_induct)
  case Skip then show ?case by auto
next
  case Assign then show ?case
    by (auto simp: ball_Un)
next
  case (Seq c1 s1 s2 c2 s3 X t1)
  from Seq.IH(1) Seq.prems obtain t2 where
    t12: "(c1, t1) \ t2" and s2t2: "s2 = t2 on L c2 X"
    by simp blast
  from Seq.IH(2)[OF s2t2] obtain t3 where
    t23: "(c2, t2) \ t3" and s3t3: "s3 = t3 on X"
    by auto
  show ?case using t12 t23 s3t3 by auto
next
  case (IfTrue b s c1 s' c2)
  hence "s = t on vars b" and "s = t on L c1 X" by auto
  from  bval_eq_if_eq_on_vars[OF this(1)] IfTrue(1) have "bval b t" by simp
  from IfTrue.IH[OF \<open>s = t on L c1 X\<close>] obtain t' where
    "(c1, t) \ t'" "s' = t' on X" by auto
  thus ?case using \<open>bval b t\<close> by auto
next
  case (IfFalse b s c2 s' c1)
  hence "s = t on vars b" "s = t on L c2 X" by auto
  from  bval_eq_if_eq_on_vars[OF this(1)] IfFalse(1) have "~bval b t" by simp
  from IfFalse.IH[OF \<open>s = t on L c2 X\<close>] obtain t' where
    "(c2, t) \ t'" "s' = t' on X" by auto
  thus ?case using \<open>~bval b t\<close> by auto
next
  case (WhileFalse b s c)
  hence "~ bval b t"
    by (metis L_While_vars bval_eq_if_eq_on_vars subsetD)
  thus ?case using WhileFalse.prems L_While_X[of X b c] by auto
next
  case (WhileTrue b s1 c s2 s3 X t1)
  let ?w = "WHILE b DO c"
  from \<open>bval b s1\<close> WhileTrue.prems have "bval b t1"
    by (metis L_While_vars bval_eq_if_eq_on_vars subsetD)
  have "s1 = t1 on L c (L ?w X)" using  L_While_pfp WhileTrue.prems
    by (blast)
  from WhileTrue.IH(1)[OF this] obtain t2 where
    "(c, t1) \ t2" "s2 = t2 on L ?w X" by auto
  from WhileTrue.IH(2)[OF this(2)] obtain t3 where "(?w,t2) \ t3" "s3 = t3 on X"
    by auto
  with \<open>bval b t1\<close> \<open>(c, t1) \<Rightarrow> t2\<close> show ?case by auto
qed

subsubsection "Executability"

lemma L_subset_vars: "L c X \ rvars c \ X"
proof(induction c arbitrary: X)
  case (While b c)
  have "lfp(\Y. vars b \ X \ L c Y) \ vars b \ rvars c \ X"
    using While.IH[of "vars b \ rvars c \ X"]
    by (auto intro!: lfp_lowerbound)
  thus ?case by (simp add: L.simps(5))
qed auto

text\<open>Make \<^const>\<open>L\<close> executable by replacing \<^const>\<open>lfp\<close> with the \<^const>\<open>while\<close> combinator from theory \<^theory>\<open>HOL-Library.While_Combinator\<close>. The \<^const>\<open>while\<close>
combinator obeys the recursion equation
@{thm[display] While_Combinator.while_unfold[no_vars]}
and is thus executable.\<close>

lemma L_While: fixes b c X
assumes "finite X" defines "f == \Y. vars b \ X \ L c Y"
shows "L (WHILE b DO c) X = while (\Y. f Y \ Y) f {}" (is "_ = ?r")
proof -
  let ?V = "vars b \ rvars c \ X"
  have "lfp f = ?r"
  proof(rule lfp_while[where C = "?V"])
    show "mono f" by(simp add: f_def mono_union_L)
  next
    fix Y show "Y \ ?V \ f Y \ ?V"
      unfolding f_def using L_subset_vars[of c] by blast
  next
    show "finite ?V" using \<open>finite X\<close> by simp
  qed
  thus ?thesis by (simp add: f_def L.simps(5))
qed

lemma L_While_let: "finite X \ L (WHILE b DO c) X =
  (let f = (\<lambda>Y. vars b \<union> X \<union> L c Y)
   in while (\<lambda>Y. f Y \<noteq> Y) f {})"
by(simp add: L_While)

lemma L_While_set: "L (WHILE b DO c) (set xs) =
  (let f = (\<lambda>Y. vars b \<union> set xs \<union> L c Y)
   in while (\<lambda>Y. f Y \<noteq> Y) f {})"
by(rule L_While_let, simp)

text\<open>Replace the equation for \<open>L (WHILE \<dots>)\<close> by the executable @{thm[source] L_While_set}:\<close>
lemmas [code] = L.simps(1-4) L_While_set
text\<open>Sorry, this syntax is odd.\<close>

text\<open>A test:\<close>
lemma "(let b = Less (N 0) (V ''y''); c = ''y'' ::= V ''x'';; ''x'' ::= V ''z''
  in L (WHILE b DO c) {''y''}) = {''x'', ''y'', ''z''}"
by eval

subsubsection "Limiting the number of iterations"

text\<open>The final parameter is the default value:\<close>

fun iter :: "('a \ 'a) \ nat \ 'a \ 'a \ 'a" where
"iter f 0 p d = d" |
"iter f (Suc n) p d = (if f p = p then p else iter f n (f p) d)"

text\<open>A version of \<^const>\<open>L\<close> with a bounded number of iterations (here: 2)
in the WHILE case:\<close>

fun Lb :: "com \ vname set \ vname set" where
"Lb SKIP X = X" |
"Lb (x ::= a) X = (if x \ X then X - {x} \ vars a else X)" |
"Lb (c\<^sub>1;; c\<^sub>2) X = (Lb c\<^sub>1 \ Lb c\<^sub>2) X" |
"Lb (IF b THEN c\<^sub>1 ELSE c\<^sub>2) X = vars b \ Lb c\<^sub>1 X \ Lb c\<^sub>2 X" |
"Lb (WHILE b DO c) X = iter (\A. vars b \ X \ Lb c A) 2 {} (vars b \ rvars c \ X)"

text\<open>\<^const>\<open>Lb\<close> (and \<^const>\<open>iter\<close>) is not monotone!\<close>
lemma "let w = WHILE Bc False DO (''x'' ::= V ''y'';; ''z'' ::= V ''x'')
  in \<not> (Lb w {''z''} \<subseteq> Lb w {''y'',''z''})"
by eval

lemma lfp_subset_iter:
  "\ mono f; !!X. f X \ f' X; lfp f \ D \ \ lfp f \ iter f' n A D"
proof(induction n arbitrary: A)
  case 0 thus ?case by simp
next
  case Suc thus ?case by simp (metis lfp_lowerbound)
qed

lemma "L c X \ Lb c X"
proof(induction c arbitrary: X)
  case (While b c)
  let ?f  = "\A. vars b \ X \ L c A"
  let ?fb = "\A. vars b \ X \ Lb c A"
  show ?case
  proof (simp add: L.simps(5), rule lfp_subset_iter[OF mono_union_L])
    show "!!X. ?f X \ ?fb X" using While.IH by blast
    show "lfp ?f \ vars b \ rvars c \ X"
      by (metis (full_types) L.simps(5) L_subset_vars rvars.simps(5))
  qed
next
  case Seq thus ?case by simp (metis (full_types) L_mono monoD subset_trans)
qed auto

end

quality100%

¤ Dauer der Verarbeitung: 0.14 Sekunden (vorverarbeitet) ¤

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.