Time to try it out!

Before we go any further, if you have a copy of Perfect Developer already installed (either independently or as part of Escher Verification Studio, then we suggest you try building and verifying the Book class as it now stands.

Follow these instructions:

1. Start Perfect Developer.

2. From the File menu select New project. Browse to whatever directory you would like to use to store the project, enter a suitable project name (e.g. Books) and click Save.

3. From the Project menu select Create file. Enter Book as the filename, leave the other boxes alone and click OK. Perfect Developer will create the file Book.pd, generate a skeleton for class Book in it, and open the file in whatever editor you selected. Under Windows this will be Notepad, if you have not yet used the Set Editor facility in the Options menu.

4. Paste the following text into the abstract section:

   var title: string,
       authors: set of string;
   
   

5. Paste the following text into the interface section, deleting the default constructor declaration that is already there:

   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};
   
   

6. Still within the editor, from the File menu select Save, then exit the editor (or simply switch to the Perfect Developer window).

The Files window within Perfect Developer will now show a single file, namely Book.pd. At this stage there are several things you can do; we suggest the following:

From the Project menu select Settings, then change whatever settings you may consider appropriate (for example, in the Code Generation tab you may wish to change the output language from C++ to Java).

From the Build menu select Build to generate code and watch the Results window. You can also generate code for a single file by right-clicking on the filename in the Files window and selecting Build. If any error messages are generated, double clicking on them will take you into the editor (if the editor allows and the facility is configured correctly, it will take you to the exact line and column of the error). Error messages should be self-explanatory, but if you can't understand the message and you think the file looks ok, try retyping the offending line. Perhaps a strange character has been pasted across and isn't showing in the editor?.

Once the file is building without errors, from the Build menu select Verify. You can also verify a single file by right-clicking on the filename in the Files window and selecting Verify.

You should see one verification warning message in the Results window. Can you understand the reason for it?

Next:  Class invariants