Quelle Abs_Int2.thy Sprache: Isabelle

(* Author: Tobias Nipkow *)

subsection "Backward Analysis of Expressions"

theory Abs_Int2
imports Abs_Int1
begin

instantiation prod :: (order,order) order
begin

definition "less_eq_prod p1 p2 = (fst p1 \ fst p2 \ snd p1 \ snd p2)"
definition "less_prod p1 p2 = (p1 \ p2 \ \ p2 \ (p1::'a*'b))"

instance
proof (standard, goal_cases)
  case 1 show ?case by(rule less_prod_def)
next
  case 2 show ?case by(simp add: less_eq_prod_def)
next
  case 3 thus ?case unfolding less_eq_prod_def by(metis order_trans)
next
  case 4 thus ?case by(simp add: less_eq_prod_def)(metis eq_iff surjective_pairing)
qed

end

subsubsection "Extended Framework"

subclass (in bounded_lattice) semilattice_sup_top ..

locale Val_lattice_gamma = Gamma_semilattice where \<gamma> = \<gamma>
  for \<gamma> :: "'av::bounded_lattice \<Rightarrow> val set" +
assumes inter_gamma_subset_gamma_inf:
  "\ a1 \ \ a2 \ \(a1 \ a2)"
and gamma_bot[simp]: "\ \ = {}"
begin

lemma in_gamma_inf: "x \ \ a1 \ x \ \ a2 \ x \ \(a1 \ a2)"
by (metis IntI inter_gamma_subset_gamma_inf subsetD)

lemma gamma_inf: "\(a1 \ a2) = \ a1 \ \ a2"
by(rule equalityI[OF _ inter_gamma_subset_gamma_inf])
  (metis inf_le1 inf_le2 le_inf_iff mono_gamma)

end

locale Val_inv = Val_lattice_gamma where \<gamma> = \<gamma>
   for \<gamma> :: "'av::bounded_lattice \<Rightarrow> val set" +
fixes test_num' :: "val \ 'av \ bool"
and inv_plus' :: "'av \<Rightarrow> 'av \<Rightarrow> 'av \<Rightarrow> 'av * 'av"
and inv_less' :: "bool \ 'av \ 'av \ 'av * 'av"
assumes test_num': "test_num' i a = (i \<in> \<gamma> a)"
and inv_plus': "inv_plus' a a1 a2 = (a\<^sub>1',a\<^sub>2') \<Longrightarrow>
  i1 \<in> \<gamma> a1 \<Longrightarrow> i2 \<in> \<gamma> a2 \<Longrightarrow> i1+i2 \<in> \<gamma> a \<Longrightarrow> i1 \<in> \<gamma> a\<^sub>1' \<and> i2 \<in> \<gamma> a\<^sub>2'"
and inv_less': "inv_less' (i1<i2) a1 a2 = (a\<^sub>1',a\<^sub>2') \<Longrightarrow>
  i1 \<in> \<gamma> a1 \<Longrightarrow> i2 \<in> \<gamma> a2 \<Longrightarrow> i1 \<in> \<gamma> a\<^sub>1' \<and> i2 \<in> \<gamma> a\<^sub>2'"

locale Abs_Int_inv = Val_inv where \<gamma> = \<gamma>
  for \<gamma> :: "'av::bounded_lattice \<Rightarrow> val set"
begin

lemma in_gamma_sup_UpI:
  "s \ \\<^sub>o S1 \ s \ \\<^sub>o S2 \ s \ \\<^sub>o(S1 \ S2)"
by (metis (opaque_lifting, no_types) sup_ge1 sup_ge2 mono_gamma_o subsetD)

fun aval'' :: "aexp \ 'av st option \ 'av" where
"aval'' e None = \" |
"aval'' e (Some S) = aval' e S"

lemma aval''_correct: "s \ \\<^sub>o S \ aval a s \ \(aval'' a S)"
by(cases S)(auto simp add: aval'_correct split: option.splits)

subsubsection "Backward analysis"

fun inv_aval' :: "aexp \ 'av \ 'av st option \ 'av st option" where
"inv_aval' (N n) a S = (if test_num' n a then S else None)" |
"inv_aval' (V x) a S = (case S of None \ None | Some S \
  let a' = fun S x \ a in
  if a' = \ then None else Some(update S x a'))" |
"inv_aval' (Plus e1 e2) a S =
(let (a1,a2) = inv_plus' a (aval'' e1 S) (aval'' e2 S)
  in inv_aval' e1 a1 (inv_aval' e2 a2 S))"

text\<open>The test for \<^const>\<open>bot\<close> in the \<^const>\<open>V\<close>-case is important: \<^const>\<open>bot\<close> indicates that a variable has no possible values, i.e.\ that the current
program point is unreachable. But then the abstract state should collapse to
\<^const>\<open>None\<close>. Put differently, we maintain the invariant that in an abstract
state of the form \<^term>\<open>Some s\<close>, all variables are mapped to non-\<^const>\<open>bot\<close> values. Otherwise the (pointwise) sup of two abstract states, one of
which contains \<^const>\<open>bot\<close> values, may produce too large a result, thus
making the analysis less precise.\<close>

fun inv_bval' :: "bexp \ bool \ 'av st option \ 'av st option" where
"inv_bval' (Bc v) res S = (if v=res then S else None)" |
"inv_bval' (Not b) res S = inv_bval' b (\ res) S" |
"inv_bval' (And b1 b2) res S =
  (if res then inv_bval' b1 True (inv_bval' b2 True S)
   else inv_bval' b1 False S \ inv_bval' b2 False S)" |
"inv_bval' (Less e1 e2) res S =
  (let (a1,a2) = inv_less' res (aval'' e1 S) (aval'' e2 S)
   in inv_aval' e1 a1 (inv_aval' e2 a2 S))"

lemma inv_aval'_correct: "s \ \\<^sub>o S \ aval e s \ \ a \ s \ \\<^sub>o (inv_aval' e a S)"
proof(induction e arbitrary: a S)
  case N thus ?case by simp (metis test_num')
next
  case (V x)
  obtain S' where "S = Some S'" and "s \<in> \<gamma>\<^sub>s S'" using \<open>s \<in> \<gamma>\<^sub>o S\<close>
    by(auto simp: in_gamma_option_iff)
  moreover hence "s x \ \ (fun S' x)"
    by(simp add: \<gamma>_st_def)
  moreover have "s x \ \ a" using V(2) by simp
  ultimately show ?case
    by(simp add: Let_def \<gamma>_st_def)
      (metis mono_gamma emptyE in_gamma_inf gamma_bot subset_empty)
next
  case (Plus e1 e2) thus ?case
    using inv_plus'[OF _ aval''_correct aval''_correct]
    by (auto split: prod.split)
qed

lemma inv_bval'_correct: "s \ \\<^sub>o S \ bv = bval b s \ s \ \\<^sub>o(inv_bval' b bv S)"
proof(induction b arbitrary: S bv)
  case Bc thus ?case by simp
next
  case (Not b) thus ?case by simp
next
  case (And b1 b2) thus ?case
    by simp (metis And(1) And(2) in_gamma_sup_UpI)
next
  case (Less e1 e2) thus ?case
    apply hypsubst_thin
    apply (auto split: prod.split)
    apply (metis (lifting) inv_aval'_correct aval''_correct inv_less')
    done
qed

definition "step' = Step
  (\<lambda>x e S. case S of None \<Rightarrow> None | Some S \<Rightarrow> Some(update S x (aval' e S)))
  (\<lambda>b S. inv_bval' b True S)"

definition AI :: "com \ 'av st option acom option" where
"AI c = pfp (step' \) (bot c)"

lemma strip_step'[simp]: "strip(step' S c) = strip c"
by(simp add: step'_def)

lemma top_on_inv_aval': "\ top_on_opt S X; vars e \ -X \ \ top_on_opt (inv_aval' e a S) X"
by(induction e arbitrary: a S) (auto simp: Let_def split: option.splits prod.split)

lemma top_on_inv_bval': "\top_on_opt S X; vars b \ -X\ \ top_on_opt (inv_bval' b r S) X"
by(induction b arbitrary: r S) (auto simp: top_on_inv_aval' top_on_sup split: prod.split)

lemma top_on_step': "top_on_acom C (- vars C) \ top_on_acom (step' \ C) (- vars C)"
unfolding step'_def
by(rule top_on_Step)
  (auto simp add: top_on_top top_on_inv_bval' split: option.split)

subsubsection "Correctness"

lemma step_step': "step (\\<^sub>o S) (\\<^sub>c C) \ \\<^sub>c (step' S C)"
unfolding step_def step'_def
by(rule gamma_Step_subcomm)
  (auto simp: intro!: aval'_correct inv_bval'_correct in_gamma_update split: option.splits)

lemma AI_correct: "AI c = Some C \ CS c \ \\<^sub>c C"
proof(simp add: CS_def AI_def)
  assume 1: "pfp (step' \) (bot c) = Some C"
  have pfp': "step' \<top> C \<le> C" by(rule pfp_pfp[OF 1])
  have 2: "step (\\<^sub>o \) (\\<^sub>c C) \ \\<^sub>c C" \ \transfer the pfp'\
  proof(rule order_trans)
    show "step (\\<^sub>o \) (\\<^sub>c C) \ \\<^sub>c (step' \ C)" by(rule step_step')
    show "... \ \\<^sub>c C" by (metis mono_gamma_c[OF pfp'])
  qed
  have 3: "strip (\\<^sub>c C) = c" by(simp add: strip_pfp[OF _ 1] step'_def)
  have "lfp c (step (\\<^sub>o \)) \ \\<^sub>c C"
    by(rule lfp_lowerbound[simplified,where f="step (\\<^sub>o \)", OF 3 2])
  thus "lfp c (step UNIV) \ \\<^sub>c C" by simp
qed

end

subsubsection "Monotonicity"

locale Abs_Int_inv_mono = Abs_Int_inv +
assumes mono_plus': "a1 \ b1 \ a2 \ b2 \ plus' a1 a2 \ plus' b1 b2"
and mono_inv_plus': "a1 \ b1 \ a2 \ b2 \ r \ r' \
  inv_plus' r a1 a2 \ inv_plus' r' b1 b2"
and mono_inv_less': "a1 \ b1 \ a2 \ b2 \
  inv_less' bv a1 a2 \ inv_less' bv b1 b2"
begin

lemma mono_aval':
  "S1 \ S2 \ aval' e S1 \ aval' e S2"
by(induction e) (auto simp: mono_plus' mono_fun)

lemma mono_aval'':
  "S1 \ S2 \ aval'' e S1 \ aval'' e S2"
apply(cases S1)
apply simp
apply(cases S2)
apply simp
by (simp add: mono_aval')

lemma mono_inv_aval': "r1 \ r2 \ S1 \ S2 \ inv_aval' e r1 S1 \ inv_aval' e r2 S2"
apply(induction e arbitrary: r1 r2 S1 S2)
   apply(auto simp: test_num' Let_def inf_mono split: option.splits prod.splits)
   apply (metis mono_gamma subsetD)
  apply (metis le_bot inf_mono le_st_iff)
apply (metis inf_mono mono_update le_st_iff)
apply(metis mono_aval'' mono_inv_plus'[simplified less_eq_prod_def] fst_conv snd_conv)
done

lemma mono_inv_bval': "S1 \ S2 \ inv_bval' b bv S1 \ inv_bval' b bv S2"
apply(induction b arbitrary: bv S1 S2)
   apply(simp)
  apply(simp)
apply simp
apply(metis order_trans[OF _ sup_ge1] order_trans[OF _ sup_ge2])
apply (simp split: prod.splits)
apply(metis mono_aval'' mono_inv_aval' mono_inv_less'[simplified less_eq_prod_def] fst_conv snd_conv)
done

theorem mono_step': "S1 \ S2 \ C1 \ C2 \ step' S1 C1 \ step' S2 C2"
unfolding step'_def
by(rule mono2_Step) (auto simp: mono_aval' mono_inv_bval' split: option.split)

lemma mono_step'_top: "C1 \ C2 \ step' \ C1 \ step' \ C2"
by (metis mono_step' order_refl)

end

end

quality100%

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

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.