What it's all about

Perfect Developer is a 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. "Formal methods" tend to be mathematician-friendly, which is just fine if you love maths; not so good otherwise. The great thing about Perfect Developer is that you don't need to be a mathematician to use it.

To use Perfect Developer, you construct a model. You use Perfect Developer's own language, Perfect, to write your specifications. You specify the model and the requirements. Then either you refine the specification to code or you let Perfect Developer do it for you. You never write code except as a refinement to the specification.

To prove that the software is correct, Perfect Developer attempts to verify the model against the requirements. Any refinement you did is verified against the model.

Verification is performed by generating proof obligations. Proof obligations are also called verification conditions. Proving these obligations is an automated process.

If you are not familiar with object oriented development ...

... then we suggest you read Introduction to Object-Oriented Development before continuing.

... but if you can do O-O development in your sleep ...

... then have a look at the differences in Perfect.

Next:  Verified Design by Contract