Development in more detail

Construction of a software system begins with creating a model of it. The Unified Modeling Language (UML), a graphical notation for describing the architecture of a software system and how it interacts with users or with other systems can be used, if you wish.

To begin specification and implementation of a system in Perfect, you need to produce a Perfect skeleton identifying the following:

1. the main classes of the system;
2. the names and signatures (parameter lists) of interface methods and constructors of those classes;
3. the requirements that the system must meet;
4. any type declarations needed to support the above.

There are many ways of identifying the candidate classes in a problem. For example, you can consider each noun in the problem description as a potential object or class. If you are not familiar with this process, we recommend you consult a good book on the subject.

If you perform initial modelling using UML, you can generate the Perfect main classes and their method signatures by importing the UML class diagrams; however, UML does not describe formal requirements, so you will need to add these.

So, to use Perfect Developer, you construct a model, using UML if that helps you.

You specify the model and the requirements, using Perfect Developer's own language, Perfect, to write your specification.

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 verification conditions (also called proof obligations). With Perfect Developer, proving these is an automated process. You set the process going and leave it to itself.

The prover proves (or informs you that it cannot prove) that the specification is correct according to the requirements that it has been given, and that the code is correct according to the specification. For a correct program, typical percentages of proof obligations successfully discharged are in the very high nineties.

Next:  Verifying specifications