PVS‎ > ‎exercises‎ > ‎


Goal of exercise on euclidian division

See how

  • types can be used to specify program correction;
  • proof obligations stem from specification;
  • PVS pre-compiles well founded induction, from the type specification of a recursive function.

Step by step

  • Restore euclid theory and proofs as usual from ~gloess/pvs/5.0.euclid.26oct2011.euclid.dmp.txt into your new ~login/pvs/euclid/ context;
  • then follow indications given in comments:
    • look at definitions present in euclid theory (nat1, m, qr?, quotient_remainder, quotient_remainder2) and quotient_remainder2_correct theorem (whose proof is given);
    • analyze each proof obligation (TCC): where does it come from?
Sous-pages (1) : quotient_remainder_TCC2