Theory SemanticsCFG

section ‹CFG and semantics conform›

theory SemanticsCFG imports CFG begin

locale CFG_semantics_wf = CFG sourcenode targetnode kind valid_edge Entry 
    get_proc get_return_edges procs Main
  for sourcenode :: "'edge ⇒ 'node" and targetnode :: "'edge ⇒ 'node"
  and kind :: "'edge ⇒ ('var,'val,'ret,'pname) edge_kind" 
  and valid_edge :: "'edge ⇒ bool"
  and Entry :: "'node" ("'('_Entry'_')")  and get_proc :: "'node ⇒ 'pname"
  and get_return_edges :: "'edge ⇒ 'edge set"
  and procs :: "('pname × 'var list × 'var list) list" and Main :: "'pname" +
  fixes sem::"'com ⇒ ('var ⇀ 'val) list ⇒ 'com ⇒ ('var ⇀ 'val) list ⇒ bool" 
    ("((1⟨_,/_⟩) ⇒/ (1⟨_,/_⟩))" [0,0,0,0] 81)
  fixes identifies::"'node ⇒ 'com ⇒ bool" ("_ ≜ _" [51,0] 80)
  assumes fundamental_property:
    "⟦n ≜ c; ⟨c,[cf]⟩ ⇒ ⟨c',s'⟩⟧ ⟹
      ∃n' as. n -as→⇩√* n' ∧ n' ≜ c' ∧ preds (kinds as) [(cf,undefined)] ∧
              transfers (kinds as) [(cf,undefined)] = cfs' ∧ map fst cfs' = s'"


end