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

Re: [PVS-Help] Proving invariant properties in PVS




Cesar:  We have on our to-do list a feature called RECURSIVE JUDGEMENT
that will work nicely for your example.  It will generate proof
obligations on the branches assuming the judgement holds for the recursive
calls.  

The induction strategy will still be useful since it will
save the effort of capturing the theorem in the type.  I'll write
such a strategy, while Sam takes care of recursive judgements.  

Cheers,
Shankar


> From:    "Cesar A. Munoz" <munoz@nianet.org>
> 
> * The simple question: Is there a way to use the definition of a
> recursive function as the induction scheme to prove an invariant
> property?
> 
> * For example, given this trivial function 
> 
>    f(n,m) : RECURSIVE nat=
>      if (n >= m) then n
>      else 2+f(n+2,m)
>      endif
>    MEASURE if (n >= m) then 0 else m-n endif
> 
> I want to prove
>    f_odd : LEMMA
>      odd?(n) IMPLIES
>      odd?(f(n,m))
> 
> using the definition of the function as the induction scheme, i.e.,
> 
> ( (odd?(n) AND n>=m implies odd?(n)) AND
>   (odd?(n) IMPLIES odd?(n+2)) AND
>   (odd?(n) AND odd?(f(n+2,m)) IMPLIES odd?(2+f(n+2,m))) 
>   IMPLIES
>   (odd?(n) IMPLIES odd?(f(n,m)) )
> 
> * Of course, I could write 
> 
>   f(n:(odd?),m): RECURSIVE (odd?) = ...
> 
> and one of the TCCs is similar to the induction scheme above. However,
> if I also want to prove
> 
>    f_even : LEMMA
>      even?(n) IMPLIES
>      even?(f(n,m))
> 
> or for that matter, any other invariant, I have to modify the type of my
> function "f" (and then the TCCs gets reordered, and some proofs are
> rewritten, etc, ...).
> 
> * I could probably manage to get what I need with (measure-induct+ ...)
> but I wonder if there is something similar to (rule-induct ...) for
> recursive functions. Does this make sense ?
> 
> Thanks,
> Cesar
> 
> 
> 
> -- 
> Cesar A. Munoz H., Senior Staff Scientist     mailto:munoz@nianet.org
> National Institute of Aerospace      mailto://C.A.Munoz@larc.nasa.gov
> 144 Research Drive                  http://research.nianet.org/~munoz
> Hampton, VA 23666, USA   Tel. +1 (757) 766 1539 Fax +1 (757) 766 1855
>