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

Re: [PVS-Help] PVS type checks a theory but hangs with M-x tcp (proving the theory)



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