Theory Int_Exec

theory Int_Exec
  imports
    Int_Transfer
begin

section ‹The composite integer domain 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 (int_dom_ops mode)› and
  ‹generic_enter_st_for (int_dom_ops mode)›, and their agreement with the abstract transfer is
  ‹int_tf.tf_st_for_commute› and ‹int_tf.enter_st_for_commute›: nothing about them
  is the domain's to state. The mode is an argument like any other, chosen by public production reporting; it is orthogonal to equation generation and solver choice.
›

text ‹A declared global holds the abstraction of ‹0›, a local the whole-value element.›

abbreviation cinit_int_dom_st :: "int_dom default_st" where
  "cinit_int_dom_st ≡ initial_default_st top (int_dom_of_int 0)"

end