a program is represented as a call graph over operations. an observation_frame restricts which part of a concrete_state is relevant. each operation has an abstract_state_change summarizing the observable change from a before_observed_state to an after_observed_state. a classification_function maps each abstract_state_change to an operation_kind, enabling symbolic reasoning over call sequences.
program operation_set call_relation binding_environment storage_entity_set concrete_state observation_frame observed_entity_set observed_state abstract_state_change before_observed_state after_observed_state operation_classification operation_kind
entity_state_mapping :: storage_entity_set -> value observation_projection :: concrete_state -> observed_state operation_effect :: operation_identifier -> abstract_state_change classification_function :: observation_frame abstract_state_change -> operation_classification compose_effects :: abstract_state_change_list -> abstract_state_change
program defines operation_set as the finite set of operation_identifiers. defines call_relation as ordered pairs of operation_identifiers indicating call edges. defines binding_environment as a relation between name_identifiers and storage_entity_set. storage_entity_set defines the set of entities whose state may be changed by operations. concrete_state is the total state of all entities in storage_entity_set at a point in execution. entity_state_mapping associates each element of storage_entity_set with a value representing its current state in a concrete_state. observation_frame defines observed_entity_set as a subset of storage_entity_set. observed_state represents the state restricted to observed_entity_set. observation_projection maps a concrete_state to an observed_state determined by observed_entity_set in an observation_frame. abstract_state_change pairs a before_observed_state with an after_observed_state. operation_effect yields abstract_state_change for an operation as the pair of observed_states before and after that operation. operation_classification contains an operation_kind indicating how an operation changes observed_state. classification_function inspects abstract_state_change relative to observation_frame and assigns an operation_kind. compose_effects combines a list of abstract_state_change entries into a single abstract_state_change when composition is defined.
operation_kind in introduction elimination transformation identity