[Prev][Next][Index]
Re: How do I put proof obs onto operator args?

To: kirk@zipcode.Jpl.Nasa.Gov (Kirk Reinholtz)

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

From: horning

Date: Tue, 08 Mar 94 12:31:54 0800

Cc: horning

DeliveryDate: Tue, 08 Mar 94 12:32:01 0800

InReplyTo: Message of Tue, 08 Mar 94 11:55:50 0800 from kirk@zipcode.Jpl.Nasa.Gov (Kirk Reinholtz)
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.