Perfect Developer Support FAQ (historic)

This FAQ was provided only as a guide to help new users of Perfect Developer. We divided the FAQ into sections for ease of use. Please feel free to send suggestions for questions you would like answered in this FAQ, by filling in one of our contact forms.

With the release of Escher Verification Studio Version 6.0, we are starting to use a forum as well, or perhaps instead. This forum is intended for questions about both Escher C Verfier and Perfect Developer. However, these FAQs may still be helpful.

Installation questions

I am using Windows, but the installation did not start automatically when I inserted the CD. How do I start it manually?

Using Windows Explorer, browse the CD to the 'Win32\Escher' directory and double-click on the 'Setup.exe' file.

Can I install multiple copies of Perfect Developer under Windows?

The simple answer is no. When you install Perfect Developer, it sets up entries in the system registry. The next time you run the installation, it looks for these entries and if found, it assumes you are attempting to perform an upgrade. If you are using a very early version of the CD, it will be possible to install multiple copies, but all copies will use the same registry settings (those of the last installation performed).

Questions about using Perfect Developer

I find the output from previous jobs confusing when examining the output from my build. Is there any way I can clear the window before I start another job?

Yes. You can either do it manually, by left-clicking the 'Clear' button in the application's main window, or you can make this automatic by checking the appropriate box in the 'Configure/Miscellaneous' dialog box.

If I try to perform other operations while Perfect Developer is performing verification, I find the system to be slow/unresponsive. Is there any way I can improve this situation?

Perfect Developer uses the default operating system priority but sometimes you may wish to reduce the processor time available to Perfect Developer to increase the responsiveness to other applications. To reduce the priority of the various tasks initiated from the Project Manager, check the appropriate box in the 'Configure/Job priority' dialog box and all jobs of that type will always be run at low priority.

Questions about verification

When trying to verify my project I receive repeated warning messages of the form "Warning! Exceeded memory limit" but my computer system exceeds your minimum requirement. How can I resolve this problem?

Perfect Developer provides an option to limit the amount of memory available to it. If this limit is set too low for a given project, then the validator will run out of memory and fail to prove the obligation that caused the limit to be hit. To fix this, go to the 'Verification' or 'Validation' tab in the project settings property page and specify a larger figure in the 'Memory Limit (Mb)' field. If the value is set too high, some Microsoft operating systems will incorrectly terminate Perfect Developer instead of simply refusing the memory request.

I am trying to verify a specification I have written, but Perfect Developer is failing to prove some verification conditions that I believe to be provable. Are there any settings I should be aware of that may be limiting the prover's ability to do its job?

Yes. There are three settings on the 'Verification' or 'Validation' tab of the Project Settings. The first is "Time limit #1" which defaults to 'None' (meaning infinity) and should not normally be changed. For more complex verification conditions, increasing the figure in 'Time limit #2' may help the situation. Finally, the 'Boredom limit' may be increased. The 'boredom' time limit specifies how long the prover should go on working on a proof attempt before checking if any progress has been made. Essentially, the prover checks at intervals specified by this limit and if no progress has been made since the last time it checked, it gives up on that proof attempt. All three of these limits are specified in seconds, but note that 'None' signals infinity. If increasing these limits does not help, there may be missing information needed to prove something about the program, and the 'unproven' output file should be examined to determine what the problem is.

When attempting to verify my project, the tool appears to be doing nothing for a long time. Is the system idle/stalled at this point?

This is a rather difficult question to answer, but there are a couple of simple things to check. Firstly, if the Perfect Developer project does not have has its 'quiet level' set to 'Noisy' then the progress of the validator will not be displayed until validation is complete. Setting to 'Noisy' will cause the progress to be displayed in real time, on the status bar of the ProJect Manager window. Activity is indicated if the statistics are changing or the activity indicator on the far right of the status bar is revolving. The 'quiet level' setting may be found in the 'Miscellaneous' tab of the project settings property page. If the statistics are being displayed but no activity indicator is even apparent, then this suggests that the validator has stalled (just taking a very long time in fact) in phase one. This can occur if the prover is working on a very complex literal expression, and it may be prudent to provide 'Time limit #1' with a value lower than its current setting (this defaults to 'None' which means that phase one will never time out). This would mean that the prover would definitely fail that obligation, but at least it would allow remaining obligations to be attempted.

Questions on using the example project

Perfect Developer has successfully installed under Windows and I want to start experimenting. I noticed an option to install examples during installation. Where are they located, and how do I use them?

If selected for installation, examples are installed in various subfolders of a folder called 'Examples' in your chosen installation directory. The 'HelloWorld' example includes a both a Perfect Developer project file (Hello.pdp) and a Microsoft Visual C++ 2005 project file (HelloWorld.vcproj) that can also be opened by later versions of Microsoft Visual C++ including Express Editions. To generate an executable program using C++, first open the Perfect Developer project file (you can either start the Perfect Developer project manager using the icon in the start menu and then open the project from within the project manager, or simply double-click on the 'Hello.pdp' file from Windows Explorer). Select the "C++ configuration" and click on the 'Build' tool (or select the 'Build' menu item from the 'Project' menu). To compile the generated C++ files, open the MSVC++ project by double-clicking on the 'HelloWorld.vcproj' file in the 'cplusplus' subfolder, and compile to an executable in the usual way. Please see the User Guide (available from the start menu under 'Documentation' for more information on using the Perfect Developer project manager.

Last updated 18 February 2013