Re: How do I put proof obs onto operator args?

Could you perhaps send me an example of a state-oriented specification
as you discussed below? I'd sure like to see how the "big boys" do it!


I wrote each state as operator composition on the state vector (the
state vector in a tuple, naturally), so the state machine is a (as yet
unspecified) machine that repeatedly applies the appropriate state
operator to the state vector. It worked, but I was thinking that I'd
have to use some sort of recursive notation to express the mechanism
that cycles the machine.

Anyway, again, thanks for your help with this. The LSL/LCL orientation
towards real-world application with mechanized support seems the way to

> From horning@src.dec.com Tue Mar  8 16:33 PST 1994
> Return-Path: <horning@src.dec.com@zipcode.jpl.nasa.gov>
> To: kirk@zipcode.Jpl.Nasa.Gov (Kirk Reinholtz)
> Cc: horning@Pa.dec.com
> Subject: Re: How do I put proof obs onto operator args?
> In-Reply-To: Message of Tue, 8 Mar 1994 13:59:24 +0800
> Date: Tue, 08 Mar 94 16:26:52 -0800
> From: horning@src.dec.com
> X-Mts: smtp
> Kirk,
> What we have tended to do in cases like this is to define the values and
> operators of the state space in LSL, but to define state transitions
> (operations) in an interface language in the form of REQUIRES, MODIFIES,
> and ENSURES clauses.  The constraints on correct invocation of an operation
> appear in its REQUIRES clause (precondition).  The state variables it is
> allowed to modify appear in the MODIFIES clause, and the relation between
> the states before and after (a correct invocation of) the operation appear
> in the ENSURES clause (with the values of variables in the post state
> denoted by priming the variables).
> We have found this distinction between operators and operations to be quite
> useful in a variety of applications, and I would urge you to try it, even
> using a quite informally designed interface language suitable to your
> application.  To recapitulate:
> - operators are functions (defined using LSL), and the notions of pre- and
> post-state, precondition, etc. don't make sense for an operator;
> - operations are state transitions (specified in an interface language),
> and are the proper place to specify errors and their consequences.
> For more information on conditional equations, contact Steve Garland
> <garland@lcs.mit.edu> about the planned beta release of the new set of
> Larch tools, including a new LP that accepts the new LSL syntax.
> Jim H.