Control object in Larch/C

To: nj2!cflatter!aoc.nrao.edu@uu3.psi.com
Subject: Control object in Larch/C
From: "Jeannette M. Wing" <wing@cs.cmu.edu>
Date: Fri, 2 Dec 94 09:52:34 EST
Cc: larch-interest@src.dec.com
Delivery-Date: Fri, 02 Dec 94 07:03:32 -0800
In-Reply-To: Chris Flatters's message of Thu, 01 Dec 94 18:56:35 EST <9411017863.AA786336995@njgate.chek.com>
Sender: Jeannette Wing <wing@VOILA.VENARI.CS.CMU.EDU>


Chris,

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

Follow-Up(s):

Re: Control in interface spec languages

From: leavens@cs.iastate.edu (Gary Leavens)