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

[PVS-Help] Proving invariant properties in PVS



* 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