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.
