Overview of development

To use Perfect Developer, you construct a model. If it helps you, you can start from a UML structural method.

You specify the model and the requirements, using Perfect Developer's own language, Perfect, to write your 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 (also called verification conditions). With Perfect Developer, proving these obligations is an automated process. You set the process going and leave it to itself.

Once the specification has been proved to be correct, either you refine the specification to code or you let Perfect Developer generate the code automatically.   You never write code except as a refinement to the specification.

Now you can compile and run your prototype, for the user's inspection and comments. You know with certainty that the prototype is correct according to the requirements stated, but users are notoriously poor at expressing their requirements at the first time of trying. The requirements originally given may need to be modified and the process repeated until the user accepts the prototype.

At this stage, you can consider manual refinements in the interests of system efficiency. We suggest profiling to determine where effort is best applied.   Of course, the manual refinements to the specification must be verified in their turn.

The system thus developed is to a considerable extent self-documenting.

Next:  Development in more detail