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