Theory Voblint_Analysis_Parity.Parity_Exec

theory Parity_Exec
  imports
    Parity_Transfer
begin

section ‹Parity 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 parity_ops› and
  ‹generic_enter_st_for parity_ops›, and their agreement with the abstract transfer is
  ‹parity_tf.tf_st_for_commute› and ‹parity_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 ‹PEven›, a local ‹PTop›.›

abbreviation cinit_parity_st :: "parity default_st" where
  "cinit_parity_st ≡ initial_default_st PTop PEven"

end