Commercial advantages

Perfect Developer is an easy-to-use software development tool for producing software that is mathematically proven to be correct.

Although the developers of safety-critical software have for some years been building software systems that can be mathematically shown to be correct, the techniques used have been difficult to learn and too time-consuming to be applied to less critical software. With Perfect Developer, this has changed.

Fast confirmation of user requirements: Perfect Developer can be used to produce a functioning prototype quickly. At an early stage in the development process, a model of the system can be demonstrated to users to check that their requirements have been correctly captured. This means that misunderstandings with users can be rectified promptly, before large development costs have been incurred.

High productivity: The advanced automated reasoning used in the Perfect Developer prover means that continual user intervention is not needed. Further, the automatic refinement capabilities greatly decrease the amount of manual refinement that has to be carried out.

Much less debugging: Correct and continued use of Perfect Developer will substantially reduce the amount of testing and debugging activity needed, leading to lower costs and shorter time-to-market.

Ease of use: Perfect Developer is easier to use than other formal methods tools, because it does not require all its users to have advanced mathematical skills. The Perfect Developer tool has its own specification language, called Perfect, which has the look and feel of popular object-orientated languages.

Automatic correct code generation: Final code can be generated in C++ or Java, allowing integration with other components written in those languages. Additionally, we provide support for partial SPARK Ada code generation.

Perfect Developer strongly supports object-oriented development, but this is not mandated.

Models can be imported from leading UML tools, if desired.

Next: Overview of development