Goal of exercise on euclidian division
- 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?
- DO NOT IMMEDIATELY LOOK at explanation for quotient_remainder_TCC2 (most interesting) subtype TCC for PVS 5.0!
- DO NOT IMMEDIATELY LOOK at quotient_remainder_TCC2 proof given in PVS 5.0 solution dump: