[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[PVS] Newbie PVS question (Re: plz. answer this)



Dear Manoj,

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 
user, though.

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 
http://shemesh.larc.nasa.gov/fm/ftp/larc/PVS-tutorial/


> 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,
[ade]


-- 
Automata / PVS / Tools / 
    GPG: FEA2 A3FE Adriaan de Groot