ch:dijkstra-monads: finite verification conditions

Problem and result. Interpret return, bind, get, put, raise, and catch as finite predicate transformers over integer states. Constructing transformers only from those clauses preserves monotonicity on the finite postcondition language. The result validates increment and the exceptional branch and rejects an overstated postcondition.

Representation. The companion represents a finite computation by an operation tag and evaluates its transformer against decidable postconditions. Symbolic formula trees would expose a reusable verification-condition language but would also need a separate solver and proof-producing simplifier. Direct finite evaluation keeps the acceptance decision trusted only to Kappa’s checked function and makes state threading observable.

First complete version. Implement return and state bind, then get and put. Sequence two increments from state three. The complete transformer must inspect the second increment at state four and produce state five; this gives a useful end-to-end VC before exceptions are added.

Remaining cases. Add raise with the failing state, then catch with the handler entered at that state. Finally compare inferred and advertised finite postconditions in the orientation of WP-Sub. This follows the chapter order: generated operations, sequencing, exception propagation, and specification weakening.

A failing version. Pass the original state rather than the updated state through bind. The mutant fails increment, bind threading, and direct put/get. A second mutant propagates a caught failure instead of evaluating its handler and fails the catch oracle while leaving the unhandled exception case intact.

Acceptance test. Require the vc valid, exception post valid, and vc rejected results, the state-threading, catch, and put/get lines, and an empty audit. The two mutations must fail the named tests as recorded in subappendix E.9. That executable record alone stores their source identities.

Mathematical boundary. The interpreter illustrates generated predicate transformers and the verification-condition direction in WP-Sub. It does not prove theorem 104.4, theorem 104.7, establish solver soundness, or cover infinite state spaces.