Theory WeakOrderDependence

Up to index of Isabelle/HOL/Jinja/Slicing

theory WeakOrderDependence
imports DataDependence
header {* \isaheader{Weak Order Dependence} *}

theory WeakOrderDependence imports "../Basic/CFG" DataDependence begin

text {* Weak order dependence is just defined as a static control dependence *}

subsection{* Definition and some lemmas *}

definition (in CFG) weak_order_dependence :: "'node => 'node => 'node => bool"
("_ -->wod _,_")
where wod_def:"n -->wod n1,n2 ≡ ((n1 ≠ n2) ∧
(∃as. (n -as->* n1) ∧ (n2 ∉ set (sourcenodes as))) ∧
(∃as. (n -as->* n2) ∧ (n1 ∉ set (sourcenodes as))) ∧
(∃a. (valid_edge a) ∧ (n = sourcenode a) ∧
((∃as. (targetnode a -as->* n1) ∧
(∀as'. (targetnode a -as'->* n2) --> n1 ∈ set(sourcenodes as'))) ∨
(∃as. (targetnode a -as->* n2) ∧
(∀as'. (targetnode a -as'->* n1) --> n2 ∈ set(sourcenodes as'))))))"





inductive_set (in CFG_wf) wod_backward_slice :: "'node set => 'node set"
for S :: "'node set"
where refl:"[|valid_node n; n ∈ S|] ==> n ∈ wod_backward_slice S"

| cd_closed:
"[|n' -->wod n1,n2; n1 ∈ wod_backward_slice S; n2 ∈ wod_backward_slice S|]
==> n' ∈ wod_backward_slice S"


| dd_closed:"[|n' influences V in n''; n'' ∈ wod_backward_slice S|]
==> n' ∈ wod_backward_slice S"



lemma (in CFG_wf)
wod_backward_slice_valid_node:"n ∈ wod_backward_slice S ==> valid_node n"
by(induct rule:wod_backward_slice.induct,
auto dest:path_valid_node simp:wod_def data_dependence_def)


end