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

Re: [PVS-Help] TCC Question (Stack followup)



Here's a simpler spec that demonstrates my question more clearly:

   tcc_test: THEORY
   BEGIN

   multiple_add_sub(x:nat, y:nat): RECURSIVE nat =
     IF y = 0 THEN
       x
     ELSE
       multiple_add_sub(x+1, y-1) - 1
     ENDIF
   MEASURE y

   END tcc_test

I can't prove the third TCC:

     |-------
   {1}   FORALL (x, y: nat, v: [{z: [nat, nat] | z`2 < y} -> nat]):
           NOT y = 0 IMPLIES v(x + 1, y - 1) - 1 >= 0

If "v" was "multiple_push_pop", I could expand it, and treat the cases.

David

_____________________________________________________________________
David Coppit                           david@coppit.org
The College of William and Mary        http://coppit.org/

"They have computers, and they may have other weapons of mass destruction."
Former Attorney General Janet Reno, speaking at LLNL of modern criminals