Perfect Developer
Perfect Developer (or PD for short) is a tool for modelling software systems, and providing
formal proofs of correctness. Optionally, code can be generated from the model, in a choice of languages.
Perfect Developer:
Unlike most other formal tools, Perfect Developer delivers high productivity
by generating a very high proportion
of software verification proofs without user intervention, using
state-of-the-art automated reasoning technology.
Don't just take our word for it!
Our tools can help YOU, too.
Here's how it works:
Unlike traditional software development using a standard programming
language such as 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. Where correctness is in doubt, this is
highlighted.
Quite often, you don't need to describe the program steps, since
Perfect Developer can generate them automatically. Optionally,
Perfect Developer produces an equivalent C++, C# or Java
program ready for compilation. SPARK Ada code generation is under development.
For more detail, take a look at this
step-by-step guide to software development.
|
TOP
