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

*To*: pvs-help@csl.sri.com*Subject*: Phonebook example from WIFT'95 paper not working?*From*: Byron Cook <byron@cse.ogi.edu>*Date*: Mon, 27 Jul 1998 12:19:18 -0700 (PDT)

Hi, I'm just starting " A Tutorial Intro. to PVS" from WIFT;95, and PVS's response to the second example is not what the paper promises. On page 11, relating to CONJECTURE DelAdd2, the paper says that "(grind :theories ("phone_1")) strategy proves this". however, PVS Version 2.1 (patch level 2.417) says: DelAdd2 : |------- {1} FORALL (bk: B), (nm: N), (pn: P): FindPhone(bk, nm) = n0 => DelPhone(AddPhone(bk, nm, pn), nm) =bk Rule? (grind :theories ("phone_1")) FindAx rewrites FindPhone(bk, nm) to bk(nm) Addax rewrites AddPhone(bk, nm, pn) to bk WITH [(nm) := pn] Delax rewrites DelPhone(bk WITH [(nm) := pn], nm) to bk WITH [(nm) := n0] Trying repeated skolemization, instantiation, and if-lifting, this simplifies to: DelAdd2 : {-1} bk!1(nm!1) = n0 |------- {1} bk!1 WITH [(nm!1) := n0] = bk!1 Rule? Help, What do I do now? thanks.... ------------------------------------- btw, here is my phone_1.pvs file: phone_1 : THEORY BEGIN N : TYPE P : TYPE B : TYPE = [N -> P] n0: P emptybook : B emptyax: AXIOM FORALL (nm: N) : emptybook(nm) = n0 FindPhone : [B, N -> P] FindAx : AXIOM FORALL (bk:B) (nm: N): FindPhone(bk,nm) = bk(nm) AddPhone : [B,N,P->B] Addax : AXIOM FORALL (bk:B),(nm:N),(pn:P): AddPhone(bk,nm,pn) = bk WITH [(nm) := pn] FindAdd: CONJECTURE FORALL (bk:B), (nm:N), (pn:P): FindPhone(AddPhone(bk,nm,pn),nm) = pn DelPhone : [B, N -> B] Delax : AXIOM FORALL (bk:B),(nm:N): DelPhone (bk,nm) = bk WITH [(nm) := n0] DelAdd2: CONJECTURE FORALL (bk:B),(nm:N),(pn:P) : FindPhone(bk,nm) = n0 => DelPhone(AddPhone(bk,nm,pn),nm) = bk END phone_1 - Byron

- Prev by Date:
**Re: Phonebook example from WIFT'95 paper not working?** - Next by Date:
**duplicate declarations deemed ambiguous** - Prev by thread:
**Re: Phonebook example from WIFT'95 paper not working?** - Next by thread:
**What's the context for TCC proofs?** - Index(es):