CMP.13:4.2 - Derive computable operations on the summaries

For an original operation f and abstract input a, construct f#(a) so that it covers every allowed result of applying f to an input represented by a. If post(X) collects the one-step successors of states in X, the condition is:

post(gamma(a)) ⊆ gamma(post#(a)).

This is the soundness direction: the abstract step may add possibilities, but it must retain every original successor. Handle branch restrictions, failure and the actual arithmetic under the same interpretation. For example, an interval operation justified over unbounded integers needs revision for wraparound arithmetic.

Provide a way to combine incoming possibilities. An abstract join of a and b covers gamma(a) ∪ gamma(b); it may include additional states. Implement the comparison used to recognize that a new result is already covered. Choose a representation whose operations and comparisons are affordable; an arbitrary logical formula may express the wanted property while making those operations difficult to compute.

A constructive starting point is to apply the original operation conceptually to the represented inputs, identify the property of all resulting outputs, and derive a formula for that property. The derived formula performs the abstract calculation without enumerating those inputs. Independent ranges, relations between variables and partitions by selected conditions provide different choices. Use the stronger choice where the receiving question needs the distinction it retains.