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

[PVS-Help] PVS-doubt about PVS-tutorial@WIFT'95



Dear Authors of PVS Tutorial @WIFT'95 and PVS-Help volunteers,

I am writing this mail to the authors of "A tutorial introduction to PVS"
@WIFT'95.

I just began to learn PVS. While reading (and practising the phone-book
example) the above tutorial (which I downloaded from the URL
http://www.liacs.nl/~devink/fm2003/wift-tutorial.ps), I happened to see a
slightly different output from PVS (my version of PVS is 5.0).

I have a doubt. Its regarding the proof about "KnownAdd" conjecture. As
discussed in lines 9 and 10 on page 12 (excluding the boxes) of the
tutorial, with type for AddPhone function being [B,N,P -> B]  we cannot
prove the conjecture. However, even after changing the type to [B,N,GP ->
B], as suggested on lines -12 to -9, I am left with the same interaction
from PVS i.e same as when the type was [B,N,P -> B].

But when I changed "pn: P" to "pn: GP" in the FORALL quantifier, the proof
proceeds in a flash.

My questions:
1. Why the type checker did not raise an error when I passed "pn: P" to
AddPhone whose type signature is [B,N,GP -> B] ?

2. Assuming that GP is a restricted sub-type of P, with type of AddPhone
being [B,N,GP -> B] the proof should have proceeded without changing the
type in FORALL quantifier.

I agree that my mail might look too silly and wordy, but I request you to
give some constructive reply. As of now, I have not got LATEX on my
machine, so I may not give you the LATEX output proof.

Thanks in advance,
Dr. Gourinath Banda
PhD, MSEngg, BTech
Scientist Fellow,
Formal Verification,
Room No. 317,
National Aerospace Laboratories,
Bangalore,
INDIA

Direct Fixed Phone: +91 - 080 - 2508 6507
Mobile: +91 99 89 40 50 78