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

*To*: Jonathan Ostroff <jonathan@xxxxxxxx>*Subject*: Re: [PVS-Help] PVS type checks a theory but hangs with M-x tcp (proving the theory)*From*: Sam Owre <owre@xxxxxxxxxxx>*Date*: Wed, 07 Oct 2015 21:26:23 -0700*Cc*: pvs-help@xxxxxxxxxxx, Simon Hudon <simon@xxxxxxxxxxxx>*Comments*: In-reply-to Jonathan Ostroff <jonathan@xxxxxxxx> message dated "Fri, 18 Sep 2015 13:46:19 -0400."*In-reply-to*: <FD5CFDF9-93FD-47D6-B4B1-C7A138EF7533@yorku.ca>*List-archive*: <http://mls.csl.sri.com/pipermail/pvs-help>*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*: <https://mls.csl.sri.com/cgi-bin/mailman/listinfo/pvs-help>, <mailto:pvs-help-request@csl.sri.com?subject=subscribe>*List-unsubscribe*: <https://mls.csl.sri.com/cgi-bin/mailman/options/pvs-help>, <mailto:pvs-help-request@csl.sri.com?subject=unsubscribe>*References*: <FD5CFDF9-93FD-47D6-B4B1-C7A138EF7533@yorku.ca>*Sender*: pvs-help-bounces+archive=csl.sri.com@xxxxxxxxxxx

Hi Jonathan, Sorry for taking so long to get back to you. It turns out that you can use M-x pvs-interrupt-subjob (C-c C-c) to interrupt, then go to the end of the *pvs* buffer, which should be sitting on a break: Error: Received signal number 2 (Interrupt) [condition type: interrupt-signal] Restart actions (select using :continue): 0: continue computation 1: Return to Top Level (an "abort" restart). 2: Abort entirely from this (lisp) process. [1c] pvs(55): You can then type *ps* to find out what TCC was being proved that caused it to loop. The one that is causing the problem is the definition of sum. The PVS prover has a simple heuristic for expanding recursive definitions: it assumes there is a top-level IF, whose condition is closely related to the termination measure. Then it tries to determine the truth of the condition. If it is unknown, the definition is not expanded. Otherwise the definition is expanded to it's THEN or ELSE branch, and the prover continues. When I interrupted and looked at the backtrace, I saw ->(auto-rewrite* sum(i - 94) X ...) Clearly sum is being expanded indefinitely. If you put the IF on the outside, then tcp finishes: sum (i: nat) : RECURSIVE nat = IF i = 0 THEN odd(i) + 0 ELSE odd(i) + sum(i-1) ENDIF MEASURE i I'm looking into adding a timeout to the tcp command, as well as discussing with Shankar better heuristics for dealing with recursive definitions. Cheers, Sam Jonathan Ostroff <jonathan@xxxxxxxx> wrote: > ========= > simple : THEORY > > BEGIN > % needed for preconditions as TCC, which signals a client problem > pre : DATATYPE > BEGIN > pre : pre? > END pre > > provided (p : bool) : TYPE = { x : pre | p } > > odd (i: nat): nat = 2*i + 1 > > sum (i: nat) : RECURSIVE nat = > odd(i) + (IF i = 0 THEN 0 ELSE sum(i-1) ENDIF) > MEASURE i > > root (i: nat, a: nat)(p : provided(sum(i) <= a)) : RECURSIVE nat = > IF sum(i+1) <= a THEN root(i+1,a)(pre) > ELSE i > ENDIF > MEASURE a - sum(i) > > END simple > ============= > > PVS type checks the above theory but hangs with M-x tcp, i.e. when we try to typecheck the theory? > > Is this a bug? > > Is there a workaround? > > We are using the DATATYPE “pre” to add preconditions to function to be discharged as a TC. > > Thanks > > Jonathan Ostroff

**References**:**[PVS-Help] PVS type checks a theory but hangs with M-x tcp (proving the theory)***From:*Jonathan Ostroff

- Prev by Date:
**[PVS-Help] PVS type checks a theory but hangs with M-x tcp (proving the theory)** - Next by Date:
**Re: [PVS-Help] PVS does not generate a disjointness TCC for embedded COND** - Previous by thread:
**[PVS-Help] PVS type checks a theory but hangs with M-x tcp (proving the theory)** - Next by thread:
**Re: [PVS-Help] PVS does not generate a disjointness TCC for embedded COND** - Index(es):