CMP.13:4 - Solution
Local mantra: choose the property; describe the represented possibilities; derive the abstract operations; compute a sufficient closure; interpret the answer; refine the distinction that blocks its use.
CMP.13:4.1 - Choose the observation and the direction of inference
Specify the original states, initial possibilities and transitions. Include the program location or phase when the same stored values permit different next steps there. Identify what the answer concerns: a reachable value, a path, termination, an interaction or another property. A set of reached states usually loses the order needed for a path question.
Choose what an abstract value represents. Write gamma(a) for the original possibilities represented by abstract value a. It can be a set of integer values, environments, graph states or complete traces. The concrete domain in this construction is the process being analyzed; it need not consist of physical objects.
For an overapproximation, every original possibility must remain among the represented ones. If the calculated possibilities exclude a bad outcome, that outcome is excluded from the original process. An included bad outcome may require reconstruction before it supports a counterexample. For an underapproximation, represented possibilities must be realizable: a retained witness can establish existence, while a missing witness leaves other executions unresolved. Choose the direction for the question and maintain it through the operations. The remaining steps develop the overapproximation branch.
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.
CMP.13:4.3 - Compute a result closed under the admitted transitions
For a finite graph of program points, associate an abstract state with each point. Initialize it from the admitted inputs. Recompute a successor when a predecessor summary changes and join its new contribution with the old one. CMP.3 supplies dependency scheduling and reuse. With finitely many points, monotone updates and an abstract order with no infinite increasing chain, a fair worklist reaches a stable result; the number and cost of updates still determine feasibility.
An infinite or very long increasing chain may need extrapolation. A widening combines successive approximations into a covering value and is chosen so the widening iteration stabilizes. For intervals, a bound that keeps moving outward can be replaced by an infinite bound. Apply such extrapolation where cyclic dependencies need it. Call context, retained relations and placement of widening can change precision, so a larger summary language alone does not guarantee a better computed answer.
Check the resulting closure. If I is the initial set and a the proposed result, the sufficient conditions are:
I ⊆ gamma(a) and post(gamma(a)) ⊆ gamma(a).
Every reachable state is then represented: induction on execution length uses the first condition for the start and the second for each step. An implemented abstract transformer can establish the second condition by showing its result is covered by a. Such an a is often called a post-fixpoint. A prematurely interrupted growing approximation need not contain every reachable state.
If the closure is too broad, use restrictions from guards, a more discriminating representation, or a narrowing operation with its own soundness conditions. A proposed smaller set is useful only while retaining the initial possibilities and closure. Directly checking these two conditions is often enough for a small construction. An all-executions termination or response-time claim needs a corresponding argument; a closed set of reached states alone supplies neither.
CMP.13:4.4 - Recover the conclusion and examine a reported witness
Apply the requested observation to the closed result. If its represented states all satisfy the property, use that conclusion with its original input and transition assumptions. If the result overlaps an unwanted outcome, determine whether the overlap changes the next action. It may already be sufficient to retain the unresolved alternative.
When an actual path matters, reconstruct consecutive original states, starting from an admitted initial state. For abstract path a0, a1, ..., ak, propagate:
X0 = I ∩ gamma(a0);
X(i+1) = post(Xi) ∩ gamma(a(i+1)).
If some Xi is empty, the abstract path is spurious: its steps cannot be joined into one original execution. If the last set is nonempty and these sets were computed without adding possibilities, retained predecessors can recover a concrete path. If this reconstruction is itself approximate, qualify its result with that approximation’s direction; a nonempty overapproximation still leaves feasibility unresolved.
Loops and infinite-path properties require their own path and recurrence conditions. A finite prefix reaching a bad state settles finite reachability; repeating an abstract cycle does not by itself produce an infinite original execution.
CMP.13:4.5 - Refine the lost distinction and continue from the affected computation
Locate where the reported execution or answer became impossible. Restore the distinction responsible: separate a merged state, retain a relation, distinguish a calling context, or make an abstract operation more precise. A false path through one merged class can suggest splitting its reachable dead ends from the states that supply its outgoing edge.
Recompute affected dependencies and reuse results whose inputs and interpretation remain valid. Confirm that the revised construction removes the particular spurious result and still covers all original behavior. Removing one false path may leave others.
Choose further refinement by what it can change in the receiving work. A coarse result that already answers the question is sufficient. A real counterexample changes the original construction or its allowed use; improving the analyzer cannot make that execution disappear. When refinement remains too costly or inconclusive, return the unresolved property and the condition under which another calculation or direct execution would help. C.11.DUA governs the worth of that additional work.