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

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



On Monday 03 October 2005 03:44 pm, David Coppit wrote:
> 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

This is a great example.  Let's change the definition slightly, let's make the 
return type an int instead of a nat.  That will eliminate any TCC's.  

Now let's try to prove the property of interest, namely:

gt0: LEMMA multiple_add_sub(x,y) >= 0

Go ahead, try it.  

Eventually, to prove this, you will have to prove more information about the 
return value from multiple_add_sub than it is greater than 0.  That is, you 
will have to prove something like:

gtx: LEMMA multiple_add_sub(x,y) >= x

With this result, gt0 is trivial, since x is a nat.

Now back to the version with TCCs.  Since the TCCs arise in the definition of 
multiple_add_sub, you cannot "expand" multiple_add_sub.  In the same way as 
trying to prove gt0, you will need more information about the return type. 

I hope this gives your more motivation for something like Bruno's suggestion.

Jeff