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.