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.