Installing Simplify

Applies to

• Spec# 1.0.5030 for Microsoft Visual Studio .NET 2003
• Spec# 1.0.5113 for Microsoft Visual Studio 2005 Beta 2

Summary

The Spec# Program Verifier internally uses an automatic theorem prover called Simplify. However, Simplify is not included in the Spec# release. Before you can use the Spec# Program Verifier, you need to install Simplify. Simplify is available as part of the ESC/Java release made available by HP Labs via the HP Labs Downloads web site.

To install Simplify

1. Download the ESC/Java release from HP Labs and save it to a file. (On the Downloads page, look for HP Java Programming Toolkits.)
2. If the file name ends in .tar.tar, change it to .tar.Z.
3. Using a tool such as WinZip, extract the Escjava.tar.Z archive to a location on your computer.
4. Locate the file Simplify-1.5.4.exe.win in the folder Escjava/release/master/bin of the extracted archive, and copy it to folder C:\Program Files\Microsoft\Spec#\bin (assuming you installed Spec# in C:\Program Files\Microsoft\Spec#).
5. In folder C:\Program Files\Microsoft\Spec#\bin, rename Simplify-1.5.4.exe.win to Simplify.exe.