# Theory WeakOrderDependence

section ‹Weak Order Dependence›

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