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)
    modifies control
    ensures  if "bad state" then control' = ABORT
             else ...

The point of the footnote is that control is just another kind
of object whose value may change.

Jeannette Wing