Verifying specifications

Verification is performed by generating proof obligations, or verification conditions, as they are also called. With Perfect Developer, proving these obligations is an automated process. You set the process going and leave it to itself.

In the basic tutorials, we explain how to structure a class and how to write method specifications. We introduce you to the principle of using preconditions to specify what needs to hold when a method is called, and we show you how to use the verification facility of Perfect Developer to make sure that the specification doesn't involve something untoward, such as dividing by zero or indexing off the end of a sequence.

This means that if you have written a program specification entirely in Perfect and verified it without errors, you can be fairly sure that if you go on to generate code and run the program, it won't crash. We can't absolutely promise that it won't crash, as tools such as compilers, linkers and others involved in building the executable program are outside our control.

So how do we ensure that we got the specification right? Traditional techniques for checking specifications include peer review and testing. Of course, testing doesn't check the specification as such; it checks whether code that purports to implement the specification behaves - for the test data provided - in accordance with that specification.

With Perfect Developer you can verify a specification against its expected behaviour. If you are able to express all the known user requirements as expected behaviour, and successfully verify the specification against it, you will have gone a long way towards showing that the specification meets the requirements.

Verifying specifications against expected behaviour is better than testing in the following respects:

instead of testing with a necessarily finite set of data, you can verify against an infinite (or very large) range of possible data;

you can verify a specification that hasn't been implemented yet, so it can be done much earlier in the development process;

you don't have to construct a test harness - you just express the expected behaviour along with the specifications;

but does have one disadvantage:

verifying a specification does not detect errors in the other steps (design, implement, compile, link etc.). The design and implementation steps can be verified by Perfect Developer, but you will still need testing to verify that the compile and link steps have not introduced errors (at least, until compilers and linkers are developed using Perfect Developer!).

Software development practice has shown that the earlier an error is introduced and the later it is detected, the more expensive it is to rectify. This means that a specification error that is not detected until testing (which is only possible when all the other steps have been completed) is a very expensive error indeed. It's much better to verify the specification early on.

To verify a specification against expected behaviour using Perfect Developer:

Declare the expected behaviour using post-assertions and property declarations;
Run 'Verify'.

The post-assertions and property declarations are placed in the Perfect source alongside the specification, so you don't need to take any special measures to ensure that declaration of expected behaviour remains part of the project.

When should you use post-assertions, and when should you use property declarations? As a general guide:

Behaviour that is associated primarily with calls to one particular method should be declared as a post-assertion attached to that method;

Other sorts of expected behaviour should be declared as a property of the class concerned; or, if it doesn't fit in any one class, as a global property.

Next: Verification problems