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.