The source code and proof output obtained for the source code found in section **5.2 Type Transformation** of the paper "Software Refinement with Perfect Developer".

- TypeTransformation.pd: A class that describes a type transformation of a set attribute with a sequence attribute
- Proof Output: Proofs from Source Code file

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