Control object in Larch/C
If you define the value space for the control object appropriately,
e.g., to include a special return address, ABORT, for an aborted
procedure then in the post-condition you can write:
foo = ...
requires control^ = "return address of invocation" (as said in the footnote)
ensures if "bad state" then control' = ABORT
The point of the footnote is that control is just another kind
of object whose value may change.