Software Development with Perfect Developer

Perfect Developer is a tool that supports verified design by contract and the refinement process through the object oriented programming language Perfect. The tool has been launched by Escher Technologies and has been met with great interest in research and industry, being the focus of a number of projectsTU Wien, Imperial College and RefineNet. The Perfect language is one that support both specification and implementation notation, giving developers one language to develop in from specification to final implementation.

Software Refinement with Perfect Developer

Software Refinement with Perfect Developer: Our paper for SEFM 2005

The source code and proof output of the examples used in the text of the paper are provided on the following pages:

Language: A trivial class that illustrates the syntax and structure of Perfect, the language supported by Perfect Developer
Algorithm Refinement: An illustration of algorithm refinement of a sort function by insertion sort
Data Refinement - Attribute Introduction: An illustration of attribute introduction with a list of integers
Data Refinement - Type Transformation: An illustration of type transformation by refining a set to a sequence
Delta Refinement - Class Extension: An illustration of class extension with the well known Point & ColourPoint example
Delta Refinement - Specification Adaptation: An illustration of specification adaptation with a square root function

Perfect Language

Introducing the Perfect Language: Our paper that gives a tutorial for Perfect

The source code and proof output of the examples used in the text of the paper are provided on the following pages:

NumberString: A class that illustrates the syntax and structure of Perfect by showing a refinement of Strings that represent numbers into integers
Proof Output: Proofs from Source Code file
Unproven Output: Details of the unproven obligations

Other Experiments with Perfect Developer

Case Studies

Harbour Management: A Harbour Management System that keeps track of ships docking
DbC University: A University that allows double honours students to change subjects
Election: An Irish electoral voting system
Library Database: A Library Database system based on Kemmerer's Problem
Resource Manager: An attempt to approximate concurrency and define a reactive system

Experiments

Refinement: A suite of Refinement examples
Vegetarian: A vegetarian program that illustrates the problem of inheritance specialization
Covariance and Contravariance: An illustration of the issue of covariance and contravariance within Perfect
Dynamic Signature: An illustration of the dynamic binding signature of Perfect
Generics: A non-empty sequence description that illustrates the language of Generics
Higher Order Functions: An attempt to increase the range of higher order functions in Perfect
File Handling: An attempt to develop a better file handling mechanism in Perfect
Wrapper: An illustration of the problems that may arise from using Wrapper Classes
Interesting Unproven obligations: Illustrates some assertions that were suprisingly unproven by Perfect Developer
Ownership Domains: Illustrates how PD handles the breaking of invariants in software

Data Structures

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