[Prev][Next][Index]

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

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.