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

A couple of basic PVS questions

I've just begun to learn how to use PVS.  I've gone through Butler's
tutorial (BUTLER), and also the "Less Elementary" tutorial by Rushby and
Stringer-Calvert (R/SC).  I have a few very basic questions, and I think
that if they can be answered, it would help me get a firmer grasp of how
PVS works... 

While going through Butler's tutorial, I tried a few slight variations on 
the definitions and specs in Basic_Defs.pvs.  In particular,

1. I specified a separate type

	seating : TYPE = {x: [row, position] | x = x}

2.  then instead of using the spec. for seat_assignment in BUTLER and
R/SC, I specified it in terms of my type, seating (but otherwise the spec
is just as in BUTLER and R/SC: 

	seat_assignment : TYPE = [# seat : seating, pass : passenger #]

(in fact everywhere, subsequently, that BUTLER used [row, position], I 
used my type, seating.

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? 

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

	seating : TYPE = {x : [row, position] | TRUE}

This time when I typechecked, a TCC *was* generated:

	% Existence TCC ... for aircraft: FUNCTION[flight -> plane]
	  % untried
	aircraft_TCC: OBLIGATION (EXISTS (x: [flight -> plane]): TRUE);

I assume that this arose as a result of my using 'TRUE' as the condition
to ensure that seating is the set of all [row, position] pairs, instead of
'x = x'.  But 'TRUE' and 'x=x' should be equivalent (for declared var,
'x'). Then why does the spec for seating with 'TRUE' as condition yield a
TCC, when the same spec with 'x=x' did not?