Theory Slicing.BasicDefs

chapter ‹The Framework›

theory BasicDefs imports AuxLemmas begin

text ‹
  As slicing is a program analysis that can be completely based on the
  information given in the CFG, we want to provide a framework which
  allows us to formalize and prove properties of slicing regardless of
  the actual programming language. So the starting point for the formalization 
  is the definition of an abstract CFG, i.e.\ without considering features 
  specific for certain languages. By doing so we ensure that our framework 
  is as generic as possible since all proofs hold for every language whose 
  CFG conforms to this abstract CFG.  This abstract CFG can be used as a 
  basis for static intraprocedural slicing as well as for dynamic slicing, 
  if in the dynamic case all method calls are inlined (i.e., abstract CFG 
  paths conform to traces).
›

section ‹Basic Definitions›

subsection‹Edge kinds›

datatype 'state edge_kind = Update "'state ⇒ 'state"           ("⇑_")
                          | Predicate "'state ⇒ bool"      ("'(_')⇩√")


subsection ‹Transfer and predicate functions›

fun transfer :: "'state edge_kind ⇒ 'state ⇒ 'state"
where "transfer (⇑f) s = f s"
  | "transfer (P)⇩√ s   = s"

fun transfers :: "'state edge_kind list ⇒ 'state ⇒ 'state"
where "transfers [] s   = s"
  | "transfers (e#es) s = transfers es (transfer e s)"

fun pred :: "'state edge_kind ⇒ 'state ⇒ bool"
where "pred (⇑f) s = True"
  | "pred (P)⇩√ s   = (P s)"

fun preds :: "'state edge_kind list ⇒ 'state ⇒ bool"
where "preds [] s   = True"
  | "preds (e#es) s = (pred e s ∧ preds es (transfer e s))"



lemma transfers_split:
  "(transfers (ets@ets') s) = (transfers ets' (transfers ets s))"
by(induct ets arbitrary:s) auto

lemma preds_split:
  "(preds (ets@ets') s) = (preds ets s ∧ preds ets' (transfers ets s))"
by(induct ets arbitrary:s) auto


lemma transfers_id_no_influence:
  "transfers [et ← ets. et ≠ ⇑id] s = transfers ets s"
by(induct ets arbitrary:s,auto)

lemma preds_True_no_influence:
  "preds [et ← ets. et ≠ (λs. True)⇩√] s = preds ets s"
by(induct ets arbitrary:s,auto)

end