Software Refinement with Perfect Developer

4. Algorithm Refinement

The source code and proof output obtained for the source code found in section 4. Algorithm Refinement of the paper "Software Refinement with Perfect Developer".

AlgorithmRefinement.pd: A selection of functions that demonstrate a sort specification and its subsequent algorithm refinement to an insertion sort algorithm
Proof Output: Proofs from Source Code file
Unproven Output: Details of the unproven obligations

http://www.cs.nuim.ie/toolap/pd/RefinementPD/Algorithm.html - Updated 27/06/2005