[Prev][Next][Index]
Re: How do I put proof obs onto operator args?
Thanks for the quick response!
I'm specifying the Galileo tape drive in larch/LSL, as part of an
investigation into the use of practical formal specifications in real projects
where cost uppers aren't appropriate. As part of the specification, I
have functions like op_xxx(sv) == set_state(sv,xxx) to map
the state vector to that that is appropriate for entry into some state,
and I wanted to specify constraints such as those states that can enter
into a given state. I can do it by validating such as
op_xxx(sv) == set_state(P(sv),xxx))
and adding a member to the statevec sv tuple that indicates that something
invalid happened, then prove that nothing invalid happens.
That seems a bit convolved, though. I was looking for something more
obvious. Your conditional equations seem to be what I'm looking for.
Anything published yet? When will LP et al know about them?
Thanks!
> From horning@src.dec.com Tue Mar 8 12:40 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, 08 Mar 94 11:55:50 -0800
> from kirk@zipcode.Jpl.Nasa.Gov (Kirk Reinholtz)
> Date: Tue, 08 Mar 94 12:31:54 -0800
> From: horning@src.dec.com
> X-Mts: smtp
>
> Kirk,
>
> I am investigating the mailer problem.
>
> LSL 2.3 deals only with total functions, so I don't see any obvious way to
> impose the style of proof obligation you are requesting. (Maybe if I knew
> why you wanted to impose it, I could suggest some other way of getting the
> same effect.)
>
> We are planning the inclusion of conditional equations in a future version
> of LSL. This would let you say something like
>
> P(t) :: op(t) == t_set(...);
>
> Then, in order to use the equation to reduce op(t), you would need to prove
> P(t). Is this what you had in mind?
>
> Jim H.
>
>