products - Perfect Developer

How it works: a brief overview

Unlike traditional software development using a standard programming language such as Ada, C++ or Java, the Perfect Developer tool allows you to express precisely specifications and user requirements, as well as code, using its specification language, Perfect. A Perfect source file describes not only the data you want to store and the program steps you want to carry out, but also describes what the data represents, the specifications that the program steps are there to satisfy and the requirements that the system or component must meet.

Advanced automated reasoning technology is used to relate the specifications to the requirements, and the program steps to the specifications, generating correctness proofs where possible and highlighting any areas where correctness is in doubt.

Quite often, you don't need to describe the program steps, since Perfect Developer can generate them automatically. Whichever is the case, Perfect Developer produces an equivalent C++, C# or Java program ready for compilation. SPARK Ada code generation is under development (in 2010).

For more detail, take a look at this step-by-step guide to software development.