# 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

```