Preconditions

If you tried verifying Book with the class invariant added, Perfect Developer will have generated a warning something like this:

C:\...\Book.pd (23,3): Warning! Unable to prove: Class invariant satisfied (defined at C:\...\Book.pd (12,22)), cannot prove: ~(#self'.authors = 0) (see C:\...\Book_unproven.htm#1).

By the way, if you right-click on the error message and select "Go to proof/unproven information", the system will open a file containing more details of the failed proof attempt - assuming that you didn't change the project settings to suppress this file. The information in this file may be helpful in pinpointing the exact nature of the problem - sometimes it even includes a suggested fix!

The reason for this warning is that the class invariant says that an empty authors set isn't allowed. Every constructor for the class must satisfy this invariant no matter what parameters it is called with. However, the original constructor we declared initializes authors directly from the corresponding parameter, but places no restriction on what values we may pass to it.

We can impose such a restriction by declaring a precondition for the constructor 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}
    pre #authors ~= 0;

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

The keyword pre is followed by one or more (comma-separated) Boolean expressions, representing conditions that must be satisfied whenever the constructor is called. If the constructor has a postcondition, the precondition must be inserted before the postcondition. Note that the semicolon in the above example is not part of the precondition syntax; its job is to separate the entire constructor declaration from any other declarations that follow it - so the constructor postcondition would follow the precondition directly, without an intervening semicolon.

Try adding the precondition as illustrated above to your class declaration for Book and check that verification now completes successfully. Also try adding the following, outside the class declaration:

const anotherBook ^= Book{"Anonymous Poems", set of string{}};

and see what happens when you attempt to verify the file.

It isn't only constructors that may have preconditions - functions may have them too. Function preconditions may refer to the attributes (i.e. variables) of the class as well as to the parameters. A function precondition must be declared before the ^= symbol or satisfy keyword. So, if for some reason we decided to permit the hasAuthor query to be made only on those books with a title beginning with the word "The" and a space, we could use the following:

function hasAuthor(author: string): bool
pre title.begins("The ")
^= author in authors;

When writing preconditions for functions, it is good style to avoid referring to attributes and member functions which the caller cannot access. The hasAuthor function is an interface function and the only member its precondition refers to is title - which we redeclared as an interface function - so this style guideline is satisfied.

As an exercise, try adding class invariants and corresponding constructor preconditions to express the following:

The title cannot be the empty string;
There are at most 5 authors to a book;
None of the authors may be the empty string.

Use Perfect Developer to verify your solution.

Next: The 'toString' method