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 10 kB

Quelle Live.thy Sprache: Isabelle

(* Author: Tobias Nipkow *)

section "Live Variable Analysis"

theory Live imports Vars Big_Step
begin

subsection "Liveness Analysis"

fun L :: "com \ vname set \ vname set" where
"L SKIP X = X" |
"L (x ::= a) X = vars a \ (X - {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 = vars b \ X \ L c X"

value "show (L (''y'' ::= V ''z'';; ''x'' ::= Plus (V ''y'') (V ''z'')) {''x''})"

value "show (L (WHILE Less (V ''x'') (V ''x'') DO ''y'' ::= V ''z'') {''x''})"

fun "kill" :: "com \ vname set" where
"kill SKIP = {}" |
"kill (x ::= a) = {x}" |
"kill (c\<^sub>1;; c\<^sub>2) = kill c\<^sub>1 \ kill c\<^sub>2" |
"kill (IF b THEN c\<^sub>1 ELSE c\<^sub>2) = kill c\<^sub>1 \ kill c\<^sub>2" |
"kill (WHILE b DO c) = {}"

fun gen :: "com \ vname set" where
"gen SKIP = {}" |
"gen (x ::= a) = vars a" |
"gen (c\<^sub>1;; c\<^sub>2) = gen c\<^sub>1 \ (gen c\<^sub>2 - kill c\<^sub>1)" |
"gen (IF b THEN c\<^sub>1 ELSE c\<^sub>2) = vars b \ gen c\<^sub>1 \ gen c\<^sub>2" |
"gen (WHILE b DO c) = vars b \ gen c"

lemma L_gen_kill: "L c X = gen c \ (X - kill c)"
by(induct c arbitrary:X) auto

lemma L_While_pfp: "L c (L (WHILE b DO c) X) \ L (WHILE b DO c) X"
by(auto simp add:L_gen_kill)

lemma L_While_lpfp:
  "vars b \ X \ L c P \ P \ L (WHILE b DO c) X \ P"
by(simp add: L_gen_kill)

lemma L_While_vars: "vars b \ L (WHILE b DO c) X"
by auto

lemma L_While_X: "X \ L (WHILE b DO c) X"
by auto

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

subsection "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" "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 by(metis WhileFalse.prems L_While_X big_step.WhileFalse subsetD)
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

subsection "Program Optimization"

text\<open>Burying assignments to dead variables:\<close>
fun bury :: "com \ vname set \ com" where
"bury SKIP X = SKIP" |
"bury (x ::= a) X = (if x \ X then x ::= a else SKIP)" |
"bury (c\<^sub>1;; c\<^sub>2) X = (bury c\<^sub>1 (L c\<^sub>2 X);; bury c\<^sub>2 X)" |
"bury (IF b THEN c\<^sub>1 ELSE c\<^sub>2) X = IF b THEN bury c\<^sub>1 X ELSE bury c\<^sub>2 X" |
"bury (WHILE b DO c) X = WHILE b DO bury c (L (WHILE b DO c) X)"

text\<open>We could prove the analogous lemma to @{thm[source]L_correct}, and the
proof would be very similar. However, we phrase it as a semantics
preservation property:\<close>

theorem bury_correct:
  "(c,s) \ s' \ s = t on L c X \
  \<exists> t'. (bury c X,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: "(bury c1 (L c2 X), t1) \ t2" and s2t2: "s2 = t2 on L c2 X"
    by simp blast
  from Seq.IH(2)[OF s2t2] obtain t3 where
    t23: "(bury c2 X, 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" "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
    "(bury c1 X, 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
    "(bury c2 X, 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
    by simp (metis L_While_X WhileFalse.prems big_step.WhileFalse subsetD)
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
    "(bury c (L ?w X), t1) \ t2" "s2 = t2 on L ?w X" by auto
  from WhileTrue.IH(2)[OF this(2)] obtain t3
    where "(bury ?w X,t2) \ t3" "s3 = t3 on X"
    by auto
  with \<open>bval b t1\<close> \<open>(bury c (L ?w X), t1) \<Rightarrow> t2\<close> show ?case by auto
qed

corollary final_bury_correct: "(c,s) \ s' \ (bury c UNIV,s) \ s'"
using bury_correct[of c s s' UNIV]
by (auto simp: fun_eq_iff[symmetric])

text\<open>Now the opposite direction.\<close>

lemma SKIP_bury[simp]:
  "SKIP = bury c X \ c = SKIP | (\x a. c = x::=a & x \ X)"
by (cases c) auto

lemma Assign_bury[simp]: "x::=a = bury c X \ c = x::=a \ x \ X"
by (cases c) auto

lemma Seq_bury[simp]: "bc\<^sub>1;;bc\<^sub>2 = bury c X \
  (\<exists>c\<^sub>1 c\<^sub>2. c = c\<^sub>1;;c\<^sub>2 & bc\<^sub>2 = bury c\<^sub>2 X & bc\<^sub>1 = bury c\<^sub>1 (L c\<^sub>2 X))"
by (cases c) auto

lemma If_bury[simp]: "IF b THEN bc1 ELSE bc2 = bury c X \
  (\<exists>c1 c2. c = IF b THEN c1 ELSE c2 &
     bc1 = bury c1 X & bc2 = bury c2 X)"
by (cases c) auto

lemma While_bury[simp]: "WHILE b DO bc' = bury c X \
  (\<exists>c'. c = WHILE b DO c' & bc' = bury c' (L (WHILE b DO c') X))"
by (cases c) auto

theorem bury_correct2:
  "(bury c X,s) \ s' \ s = t on L c X \
  \<exists> t'. (c,t) \<Rightarrow> t' & s' = t' on X"
proof (induction "bury c X" s s' arbitrary: c 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 bc1 s1 s2 bc2 s3 c X t1)
  then obtain c1 c2 where c: "c = c1;;c2"
    and bc2: "bc2 = bury c2 X" and bc1: "bc1 = bury c1 (L c2 X)" by auto
  note IH = Seq.hyps(2,4)
  from IH(1)[OF bc1, of t1] Seq.prems c obtain t2 where
    t12: "(c1, t1) \ t2" and s2t2: "s2 = t2 on L c2 X" by auto
  from IH(2)[OF bc2 s2t2] obtain t3 where
    t23: "(c2, t2) \ t3" and s3t3: "s3 = t3 on X"
    by auto
  show ?case using c t12 t23 s3t3 by auto
next
  case (IfTrue b s bc1 s' bc2)
  then obtain c1 c2 where c: "c = IF b THEN c1 ELSE c2"
    and bc1: "bc1 = bury c1 X" and bc2: "bc2 = bury c2 X" by auto
  have "s = t on vars b" "s = t on L c1 X" using IfTrue.prems c by auto
  from bval_eq_if_eq_on_vars[OF this(1)] IfTrue(1) have "bval b t" by simp
  note IH = IfTrue.hyps(3)
  from IH[OF bc1 \<open>s = t on L c1 X\<close>] obtain t' where
    "(c1, t) \ t'" "s' =t' on X" by auto
  thus ?case using c \<open>bval b t\<close> by auto
next
  case (IfFalse b s bc2 s' bc1)
  then obtain c1 c2 where c: "c = IF b THEN c1 ELSE c2"
    and bc1: "bc1 = bury c1 X" and bc2: "bc2 = bury c2 X" by auto
  have "s = t on vars b" "s = t on L c2 X" using IfFalse.prems c by auto
  from bval_eq_if_eq_on_vars[OF this(1)] IfFalse(1) have "~bval b t" by simp
  note IH = IfFalse.hyps(3)
  from IH[OF bc2 \<open>s = t on L c2 X\<close>] obtain t' where
    "(c2, t) \ t'" "s' =t' on X" by auto
  thus ?case using c \<open>~bval b t\<close> by auto
next
  case (WhileFalse b s c)
  hence "~ bval b t"
    by auto (metis L_While_vars bval_eq_if_eq_on_vars rev_subsetD)
  thus ?case using WhileFalse
    by auto (metis L_While_X big_step.WhileFalse subsetD)
next
  case (WhileTrue b s1 bc' s2 s3 w X t1)
  then obtain c' where w: "w = WHILE b DO c'"
    and bc': "bc' = bury c' (L (WHILE b DO c') X)" by auto
  from \<open>bval b s1\<close> WhileTrue.prems w have "bval b t1"
    by auto (metis L_While_vars bval_eq_if_eq_on_vars subsetD)
  note IH = WhileTrue.hyps(3,5)
  have "s1 = t1 on L c' (L w X)"
    using L_While_pfp WhileTrue.prems w by blast
  with IH(1)[OF bc', of t1] w obtain t2 where
    "(c', t1) \ t2" "s2 = t2 on L w X" by auto
  from IH(2)[OF WhileTrue.hyps(6), of t2] w 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> w show ?case by auto
qed

corollary final_bury_correct2: "(bury c UNIV,s) \ s' \ (c,s) \ s'"
using bury_correct2[of c UNIV]
by (auto simp: fun_eq_iff[symmetric])

corollary bury_sim: "bury c UNIV \ c"
by(metis final_bury_correct final_bury_correct2)

end

quality100%

¤ Dauer der Verarbeitung: 0.13 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.