Theory Distance

chapter ‹Static Intraprocedural Slicing›

theory Distance imports "../Basic/CFG" begin

text ‹
  Static Slicing analyses a CFG prior to execution. Whereas dynamic
  slicing can provide better results for certain inputs (i.e.\ trace and
  initial state), static slicing is more conservative but provides
  results independent of inputs. 

  Correctness for static slicing is
  defined differently than correctness of dynamic slicing by a weak
  simulation between nodes and states when traversing the original and
  the sliced graph. The weak simulation property demands that if a
  (node,state) tuples $(n_1,s_1)$ simulates $(n_2,s_2)$
  and making an observable move in the original graph leads from 
  $(n_1,s_1)$ to $(n_1',s_1')$, this tuple simulates a 
  tuple $(n_2,s_2)$ which is the result of making an
  observable move in the sliced graph beginning in $(n_2',s_2')$.

  We also show how a ``dynamic slicing style'' correctness criterion for 
  static slicing of a given trace and initial state could look like.

  This formalization of static intraprocedural slicing is instantiable
  with three different kinds of control dependences: standard control,
  weak control and weak order dependence. The correctness proof for
  slicing is independent of the control dependence used, it bases only
  on one property every control dependence definition hass to fulfill.
›

section ‹Distance of Paths›

context CFG begin

inductive distance :: "'node ⇒ 'node ⇒ nat ⇒ bool"
where distanceI: 
  "⟦n -as→* n'; length as = x; ∀as'. n -as'→* n' ⟶ x ≤ length as'⟧
  ⟹ distance n n' x"


lemma every_path_distance:
  assumes "n -as→* n'"
  obtains x where "distance n n' x" and "x ≤ length as"
proof -
  have "∃x. distance n n' x ∧ x ≤ length as"
  proof(cases "∃as'. n -as'→* n' ∧ 
                     (∀asx. n -asx→* n' ⟶ length as' ≤ length asx)")
    case True
    then obtain as' 
      where "n -as'→* n' ∧ (∀asx. n -asx→* n' ⟶ length as' ≤ length asx)" 
      by blast
    hence "n -as'→* n'" and all:"∀asx. n -asx→* n' ⟶ length as' ≤ length asx"
      by simp_all
    hence "distance n n' (length as')" by(fastforce intro:distanceI)
    from ‹n -as→* n'› all have "length as' ≤ length as" by fastforce
    with ‹distance n n' (length as')› show ?thesis by blast
  next
    case False
    hence all:"∀as'. n -as'→* n' ⟶ (∃asx. n -asx→* n' ∧ length as' > length asx)"
      by fastforce
    have "wf (measure length)" by simp
    from ‹n -as→* n'› have "as ∈ {as. n -as→* n'}" by simp
    with ‹wf (measure length)› obtain as' where "as' ∈ {as. n -as→* n'}" 
      and notin:"⋀as''. (as'',as') ∈ (measure length) ⟹ as'' ∉ {as. n -as→* n'}"
      by(erule wfE_min)
    from ‹as' ∈ {as. n -as→* n'}› have "n -as'→* n'" by simp
    with all obtain asx where "n -asx→* n'"
      and "length as' > length asx"
      by blast
    with notin have  "asx ∉ {as. n -as→* n'}" by simp
    hence "¬ n -asx→* n'" by simp
    with ‹n -asx→* n'› have False by simp
    thus ?thesis by simp
  qed
  with that show ?thesis by blast
qed


lemma distance_det:
  "⟦distance n n' x; distance n n' x'⟧ ⟹ x = x'"
apply(erule distance.cases)+ apply clarsimp
apply(erule_tac x="asa" in allE) apply(erule_tac x="as" in allE)
by simp


lemma only_one_SOME_dist_edge:
  assumes valid:"valid_edge a" and dist:"distance (targetnode a) n' x"
  shows "∃!a'. sourcenode a = sourcenode a' ∧ distance (targetnode a') n' x ∧
               valid_edge a' ∧
               targetnode a' = (SOME nx. ∃a'. sourcenode a = sourcenode a' ∧
                                              distance (targetnode a') n' x ∧
                                              valid_edge a' ∧ targetnode a' = nx)"
proof(rule ex_ex1I)
  show "∃a'. sourcenode a = sourcenode a' ∧ 
             distance (targetnode a') n' x ∧ valid_edge a' ∧
             targetnode a' = (SOME nx. ∃a'. sourcenode a = sourcenode a' ∧ 
                                            distance (targetnode a') n' x ∧
                                            valid_edge a' ∧ targetnode a' = nx)"
  proof -
    have "(∃a'. sourcenode a = sourcenode a' ∧ 
                distance (targetnode a') n' x ∧ valid_edge a' ∧ 
                targetnode a' = (SOME nx. ∃a'. sourcenode a = sourcenode a' ∧
                                               distance (targetnode a') n' x ∧
                                               valid_edge a' ∧ targetnode a' = nx)) =
      (∃nx. ∃a'. sourcenode a = sourcenode a' ∧ distance (targetnode a') n' x ∧ 
                 valid_edge a' ∧ targetnode a' = nx)"
      apply(unfold some_eq_ex[of "λnx. ∃a'. sourcenode a = sourcenode a' ∧ 
                distance (targetnode a') n' x ∧valid_edge a' ∧  targetnode a' = nx"])
      by simp
    also have "…" using valid dist by blast
    finally show ?thesis .
  qed
next
  fix a' ax
  assume "sourcenode a = sourcenode a' ∧ 
    distance (targetnode a') n' x ∧ valid_edge a' ∧
    targetnode a' = (SOME nx. ∃a'. sourcenode a = sourcenode a' ∧ 
                                   distance (targetnode a') n' x ∧ 
                                   valid_edge a' ∧ targetnode a' = nx)"
    and "sourcenode a = sourcenode ax ∧ 
    distance (targetnode ax) n' x ∧ valid_edge ax ∧
    targetnode ax = (SOME nx. ∃a'. sourcenode a = sourcenode a' ∧
                                   distance (targetnode a') n' x ∧ 
                                   valid_edge a' ∧ targetnode a' = nx)"
  thus "a' = ax" by(fastforce intro!:edge_det)
qed


lemma distance_successor_distance:
  assumes "distance n n' x" and "x ≠ 0" 
  obtains a where "valid_edge a" and "n = sourcenode a" 
  and "distance (targetnode a) n' (x - 1)"
  and "targetnode a = (SOME nx. ∃a'. sourcenode a = sourcenode a' ∧ 
                                     distance (targetnode a') n' (x - 1) ∧
                                     valid_edge a' ∧ targetnode a' = nx)"
proof -
  have "∃a. valid_edge a ∧ n = sourcenode a ∧ distance (targetnode a) n' (x - 1) ∧
    targetnode a = (SOME nx. ∃a'. sourcenode a = sourcenode a' ∧ 
                                  distance (targetnode a') n' (x - 1) ∧
                                  valid_edge a' ∧ targetnode a' = nx)"
  proof(rule ccontr)
    assume "¬ (∃a. valid_edge a ∧ n = sourcenode a ∧ 
                   distance (targetnode a) n' (x - 1) ∧ 
                   targetnode a = (SOME nx. ∃a'. sourcenode a = sourcenode a' ∧ 
                                                 distance (targetnode a') n' (x - 1) ∧
                                                 valid_edge a' ∧ targetnode a' = nx))"
    hence imp:"∀a. valid_edge a ∧ n = sourcenode a ∧
                   targetnode a = (SOME nx. ∃a'. sourcenode a = sourcenode a' ∧
                                                 distance (targetnode a') n' (x - 1) ∧
                                                 valid_edge a' ∧ targetnode a' = nx)
                 ⟶ ¬ distance (targetnode a) n' (x - 1)" by blast
    from ‹distance n n' x› obtain as where "n -as→* n'" and "x = length as"
      and "∀as'. n -as'→* n' ⟶ x ≤ length as'"
      by(auto elim:distance.cases)
    thus False using imp
    proof(induct rule:path.induct)
      case (empty_path n)
      from ‹x = length []› ‹x ≠ 0› show False by simp
    next
      case (Cons_path n'' as n' a n)
      note imp = ‹∀a. valid_edge a ∧ n = sourcenode a ∧
                      targetnode a = (SOME nx. ∃a'. sourcenode a = sourcenode a' ∧
                                                 distance (targetnode a') n' (x - 1) ∧
                                                 valid_edge a' ∧ targetnode a' = nx)
                    ⟶ ¬ distance (targetnode a) n' (x - 1)›
      note all = ‹∀as'. n -as'→* n' ⟶ x ≤ length as'›
      from ‹n'' -as→* n'› obtain y where "distance n'' n' y"
        and "y ≤ length as" by(erule every_path_distance)
      from ‹distance n'' n' y› obtain as' where "n'' -as'→* n'"
        and "y = length as'"
        by(auto elim:distance.cases)
      show False
      proof(cases "y < length as")
        case True
        from ‹valid_edge a› ‹sourcenode a = n› ‹targetnode a = n''› ‹n'' -as'→* n'›
        have "n -a#as'→* n'" by -(rule path.Cons_path)
        with all have "x ≤ length (a#as')" by blast
        with ‹x = length (a#as)› True ‹y = length as'› show False by simp
      next
        case False
        with ‹y ≤ length as› ‹x = length (a#as)› have "y = x - 1" by simp
        from ‹targetnode a = n''› ‹distance n'' n' y›
        have "distance (targetnode a) n' y" by simp
        with ‹valid_edge a›
        obtain a' where "sourcenode a = sourcenode a'"
          and "distance (targetnode a') n' y" and "valid_edge a'"
          and "targetnode a' = (SOME nx. ∃a'. sourcenode a = sourcenode a' ∧
                                              distance (targetnode a') n' y ∧
                                              valid_edge a' ∧ targetnode a' = nx)"
          by(auto dest:only_one_SOME_dist_edge)
        with imp ‹sourcenode a = n› ‹y = x - 1› show False by fastforce
      qed
    qed
  qed
  with that show ?thesis by blast
qed

end

end