[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[PVS] Newbie PVS question (Re: plz. answer this)
Thank you for sending me a question directly about PVS. I'm not entirely sure
why you thing I'm the right person to be asking these things, beyond that my
name pops up on the mail archives. I'm CCing my answer to the pvs list, which
is probably where your question should have gone in the first place (list
admins? is there still a pvs-users list?). Always pleased to see a new PVS
On Saturday 09 April 2005 17:07, you wrote:
> Dear Dr. Groot,
Nope, not yet. Thesis is yet to be done.
> I have started working in PVS recently. i was
> verifying airline reservation system from Ricky Butler's tutorial. I
> could not prove the following TCC.
I assume you mean the one at
> aircraft_TCC1: OBLIGATION EXISTS (x: [flight -> plane]): TRUE;
> Could u tell me how to prove the above TCC without declaring NONEMPTY_TYPE?
> Awaiting for your early reply.
Looking at the PVS code, I see
flight: TYPE+ % Flight identifier
plane: TYPE+ % Aircraft type
aircraft: function[flight -> plane]
This already _has_ the NONEMPTY_TYPE hidden in the + (TYPE+ and NONEMPTY_TYPE
are synonyms). The theory does not generate a TCC for me at all. Note that
you _must_ have the NONEMPTY_TYPE for the range of the function for the
function to exist (by definition). Supposing you do need to prove such a TCC,
the general approach is to define (in the theory) an object of the range type
(my terminology may be rusty here, I've been doing too much Ruby and too
little PVS recently), and then using that as a constant in a function
definition. Something like this:
some_plane : plane % A plane that exists
aircraft: function [flight->plane]
Now to prove your TCC:
EXISTS (x: [flight -> plane]): TRUE;
instantiate this with a specific function; the easiest one to write down is
the constant function that yields as value some_plane:
(inst 1 "lambda (x:flight) : some_plane")
That ought to do the trick.
Hope that helps,
Automata / PVS / Tools /
GPG: FEA2 A3FE Adriaan de Groot