Class Invariants

If you tried out Perfect Developer on the Book class and you used the first definition we gave for anyAuthor, you should have seen a message like the following when you tried to verify the project:

C:\...\Book.pd (19,8): Warning! Unable to prove: Operand of 'any' or 'that' is non-empty in context of class Book [C:\...\Book.pd (7,7)], cannot prove: 0 < #self.authors (see C:\...\Book_unproven.htm#1).

If your editor supports a "goto specified row/column" function and you have configured Perfect Developer accordingly, you can double-click on the error message in the Results window. The Perfect source file to which the message relates will be opened in the editor and the cursor will be positioned at the place in the source to which the message refers. Try it!

Do you see the problem? We have specified that the function anyAuthor should return any author in the set ... but what if a Book object has no authors at all? Suppose we created a Book with the following expression:

Book{"Anonymous poems", set of string{}}

There is nothing in our Book class declaration to prohibit this!

Let's assume that we decide to solve the anyAuthor problem by insisting that every book has at least one author.

One way of doing this is to use a subtype declaration (remember those?) to declare a new type representing a non-empty sequence of strings, then declare the authors variable to be of that type.

Another way is to add a class invariant, like this:

class Book ^=
abstract
var title: string,
      authors: set of string;

invariant #authors ~= 0;

interface
function title;

function hasAuthor(author: string): bool
    ^= author in authors;

opaque function anyAuthor: string
    ^= any authors;

build{!title: string, !authors: set of string};

build{!title: string, author: string}
    post authors! = set of string{author};
end;

We declare a class invariant using the keyword invariant followed by one or more (comma-separated) Boolean expressions. The meaning is that each expression must be true for every instance of the class. Recall that the unary "#" operator is predefined for the built-in collection classes to return the number of elements in its operand. So the invariant expression reads "count of authors not-equal-to zero".

With this invariant added, the original verification error disappears because there will always be at least one author in the list. But does that mean that the class is now verifiable? Try adding the invariant and running Verify again to see!

Next: Preconditions