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

*To*: owre@xxxxxxxxxxx, rushby@xxxxxxxxxxx, shankar@xxxxxxxxxxx*Subject*: [PVS-Help] PVS-doubt about PVS-tutorial@WIFT'95*From*: "Gourinath Banda" <gourinath@xxxxxxxxxx>*Date*: Tue, 12 Jul 2011 12:40:40 +0530 (IST)*Cc*: pvs-sri@xxxxxxxxxxx, pvs-help@xxxxxxxxxxx*Importance*: Normal*In-Reply-To*: <46066.192.168.4.19.1310454434.squirrel@192.168.4.29>*List-Help*: <mailto:pvs-help-request@csl.sri.com?subject=help>*List-Id*: PVS-Help <pvs-help.csl.sri.com>*List-Post*: <mailto:pvs-help@csl.sri.com>*List-Subscribe*: <http://lists.csl.sri.com/mailman/listinfo/pvs-help>,<mailto:pvs-help-request@csl.sri.com?subject=subscribe>*List-Unsubscribe*: <http://lists.csl.sri.com/mailman/listinfo/pvs-help>,<mailto:pvs-help-request@csl.sri.com?subject=unsubscribe>*References*: <46066.192.168.4.19.1310454434.squirrel@192.168.4.29>*Reply-To*: gourinath@xxxxxxxxxx*Sender*: pvs-help-bounces+archive=csl.sri.com@xxxxxxxxxxx*User-Agent*: SquirrelMail/1.4.6

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

- Prev by Date:
**[PVS-Help] Induction Generalization** - Next by Date:
**[PVS-Help] Re: An error when pvs generates tcc's** - Prev by thread:
**Re: [PVS-Help] unprovable sequent proved** - Next by thread:
**[PVS-Help] Induction Generalization** - Index(es):