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

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



=========
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