CMP.13:1 - Problem frame
Use this when computing every relevant state or execution is unaffordable, but the question needs only some of their properties. You want to calculate with ranges, classes, relations or other summaries and determine what their answers establish about the original computation. Use it also when such a calculation reports an impossible path or loses a distinction needed for the answer.
The reader can describe the admitted inputs, elementary transitions and requested observation. Examples include asking which outcomes a rule system permits, whether a procedure can reach a failing state, or which dependencies can affect a returned value. The method constructs another computation over descriptions of possibilities, then relates its result to the question.
The first useful result is an effective abstract operation or small abstract execution with a justified conclusion about the original process. Extending that result across loops or interacting components requires the corresponding closure or composition argument. A finite reachability example can be done by hand; building an analyzer for a programming language requires its semantics and suitable algorithms for its representations.
Use direct computation when it already answers the question affordably. If the required change is a numerical error allowance, CMP.8 supplies that construction. If the problem is whether the original process describes the intended subject, return to that modeling question: a sound calculation about the process retains its subject assumptions.