The source code and proof output obtained for the source code found in section 6.2 Specification Adaptation of the paper "Software Refinement with Perfect Developer".
SpecificationAdaptation.pd: A class that defines the contract of a square root function is adapted to a better contract