6.1 Class Extension
The source code and proof output obtained for the source code found in section 6.1 Class Extension of the paper "Software Refinement with Perfect Developer".
- ClassExtension.pd: A class that describes a 2-d Point with a refined distance function and an extended class that describes a 2-d point with colour information. The refinement is implicitly included
- Proof Output: Proofs from Source Code file
- Unproven Output: Details of the unproven obligations
http://www.cs.nuim.ie/toolap/pd/RefinementPD/Extension.html - Updated 27/06/2005