Theory Voblint_Analysis_Congruence.Congruence_Exec

theory Congruence_Exec
  imports
    Congruence_Transfer
begin

section ‹Congruence 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 congruence_ops› and
  ‹generic_enter_st_for congruence_ops›, and their agreement with the abstract transfer is
  ‹congruence_tf.tf_st_for_commute› and ‹congruence_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 the single integer ‹0›, every
  local is unconstrained.
›

abbreviation cinit_congruence_st :: "congruence default_st" where
  "cinit_congruence_st ≡ initial_default_st top (congruence_of_int 0)"

end