[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
-
Delivery-Date: Tue, 08 Mar 94 12:32:01 -0800
-
In-Reply-To: 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.