Software Refinement with Perfect Developer

5.1 Attribute Introduction

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

AttributeIntroduction.pd: A class that illustrates a list of numbers that calculates the sum of the list is data refined to reduce computation cost by including a sumOfList attribute
Proof Output: Proofs from Source Code file

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