[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: A couple of basic PVS questions
> 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: email@example.com