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

Re: A couple of basic PVS questions

Mark ---

> Question 1.  These were the only changes I made to basic_defs.pvs.  Yet,
> whereas BUTLER ended up with a TCC to discharge, when I typechecked my
> version, no TCCs arose.  Why this difference? 

The version of basic_defs.pvs that does *not* generate a TCC is the one
from Rushby and Stringer-Calvert's report. Note that it declares `plane'
as a non empty type, whereas in Butler's version it is just `TYPE' and
can therefore be empty.

In the case where the type is possibly empty, you have to prove for the

	aircraft : function[flight -> plane]

that there exists such a function, as declaring such a function where one
might not exist is unsound. This requires it's range type to be non-empty,
and so the TCC is generated.

Check pages 11 and 12 of Rushby/SC for a more detailed description.

> Question 2.  A related question:  I later tried specifying my type, 
> seating, by putting ...

I show the TCC being generated in both cases, if `plane' can be empty.
I think you've updated Butler's original version in one case, and the
Rushby/SC version for the other case.

Hope this helps,


Dr Dave Stringer-Calvert, Software Engineer, Computer Science Laboratory,
SRI International, 333 Ravenswood Avenue, Menlo Park, CA 94025-3493, USA.
Phone: (650) 859-3291    Fax: (650) 859-2844   Email: dave_sc@csl.sri.com