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

[PVS-Help] Induction hypothesis vs. specification

Hi!

Please consider following program:

mult: THEORY
  BEGIN
    x, y, z: VAR nat

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

    mult_ok: LEMMA FORALL (x, y): mult(x, y, 0) = x * y
    mult_ok2: LEMMA FORALL (x, y, z): mult(x, y, z) = x * y + z

  END mult

"mult_ok2" can be easily proved by induction, but I wonder if it is possible
to prove "mult_ok". The thing I would need is to give PVS a hint by defining
the induction hypothesis. Possible? If yes, how?

Another question: Is there a repository of simple PVS examples (especially
loops)?

Thanks,

Ingo