Theory Voblint_Analysis_Interval.Interval_Exec

theory Interval_Exec
  imports
    Interval_Domain
begin

section ‹Interval on the executable carrier›

text ‹
  The executable step and procedure entry are \<^theory>‹Voblint_Nonrelational.Nonrelational_Ops›'s
  generic constructions at the bundle, ‹generic_tf_st_for ivl_ops› and
  ‹generic_enter_st_for ivl_ops›, and their agreement with the abstract transfer is
  ‹ivl_tf.tf_st_for_commute› and ‹ivl_tf.enter_st_for_commute›: nothing about them
  is the domain's to state.
›

text ‹The state a run starts in: a declared global holds ‹[0,0]›, a local is unbounded.›

abbreviation cinit_ivl_st :: "ivl default_st" where
  "cinit_ivl_st ≡ initial_default_st (Ivl MinInf PlusInf) (Ivl (Fin 0) (Fin 0))"

end