Verifying Specifications

So far we've focused on how to structure a class and how to write method specifications. We've introduced you to the principle of using preconditions to specify what needs to hold when a method is called, and we've show you how to use the verification facility of Perfect Developer to make sure that the specification doesn't involve for 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 since we don't have any control over such things as compilers, linkers and other tools involved in building the executable program; also, you may need to avoid a few situations listed on the website here for which verification is currently incomplete.

But a crash-proof program isn't much good if it doesn't actually do what it is supposed to. For example, what if we made a mistake in specifying the "+" operator in class Money? If we're writing this class for a banking or accountancy application and we make a mistake, then either our client or its customers (depending on the nature of the error) are likely to be very unhappy!

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 specifications as such; it checks whether code that purports to implement the specifications behaves - for the test data - in accordance with those specifications.

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

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

instead of testing with a finite set of test 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 behavior 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 specifications against expected behavior using Perfect Developer:

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

The post-assertions and property declarations are placed in the Perfect source alongside the specifications, so you don't need to take any special measures to ensure that declaration of expected behavior 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. If an expected behaviour doesn't fit in any one class, it can be declared as a global property.

Next: Post-assertions