SE Tools at WMCS

From SEWiki

The department supports a few tools, but most others have been installed in Dr. Coppit's account. To access these tools, you will need to add ~coppit/bin to your path. You are probably using tcsh as your shell. If so, open your ~/.tcshrc configuration file in your favorite text editor, and add the following line:

setenv PATH ${PATH}:/home/f85/coppit/bin

Then start a new shell and type echo $PATH to make sure that your change worked.

For tools that use X Windows, you don't have to be in the lab to use the tool if you have X Windows running correctly on your machine, along with ssh. Just ssh to a CS machine with the -X or -Y flag, so that ssh will forward the X11 port, allowing X applications to display locally. (-Y is needed for Mac OS X Tiger, since -X results in random X protocol errors.)

1 PVS
- 1.1 Running PVS from the CS Machines
- 1.2 Installing PVS at Home
2 Alloy Analyzer
3 Java PathFinder
4 ESC/Java 2
5 Blackbox Prototype
6 Valgrind
7 JUnit
8 Violet
9 Eclipse

[edit]

PVS

PVS is built upon the Emacs editor. For most people, the graphical XEmacs is preferred, since it provides a "PVS" menu in case you forget the key sequence that you want.

[edit]

Running PVS from the CS Machines

Create a directory to store your PVS files, which we will call your work directory. PVS will create another directory called pvsbin to store related binaries. This directory will be created as a subdirectory.
Optionally, modify your ~/.pvsemacs file to automatically load libraries you need that I've installed in /home/f85/coppit/software/pvs/lib. For example:

;;;(load-prelude-library "ProofLite") ;;;(load-prelude-library "Field") ;;;(load-prelude-library "Manip")
Start PVS by running pvs. You should see XEmacs with the PVS logo instead of the usual Emacs logo.

These are the basic commands needed to use PVS. Some other common key bindings are also available. To cycle through the previous commands in the PVS buffer, type M-P. To display your current proof in a tree diagram, type M-x x-show-current-proof. PVS uses common Emacs commands for text editing, like C-x C-s to save, C-x C-c to exit the program, and C-g to exit a prompt. If you cannot remember a particular key binding, you can always use the toolbar.

If PVS takes a long time on a command, you can interrupt it with C-c C-c. This will dump you to a prompt for Lisp. Type (restore) to get back to your previous sequent. You can also reset PVS when your cursor is in the *pvs* buffer with M-x reset-pvs.

You can step through a proof using either the M-x step-proof or the M-x x-step-proof commands. The command TAB 1 executes one proof step. The command ESC n TAB 1 executes n proof steps. Repositioning the cursor in the Proofwindow affects which step will be executed next. Therefore, use C-x o to switch between bufferes rather than using mouse clicks.

From within the prover, you issue commands like (split), (flatten), and (grind). To quit the prover, issue the (quit) command. Remember that all prover commands are in parentheses.

[edit]

Installing PVS at Home

There is a prototype version of PVS for Solaris, Linux and Mac on the SRI FTP server. To install on a Mac, first make sure you have Emacs installed separately. This version works okay, except for the x-show-proof command. (I didn't have good luck with other versions like Aquamacs.)

Once Emacs is installed, unpack the system and powerpc tarballs into a subdirectory in of /Applications, such as /Applications/PVS_3.3_Beta. Be careful of spaces in the path. Then open a terminal, change to the directory, and run bin/relocate. Then edit the "pvs" script, adding something like:

PVSPATH=/Applications/PVS_3.3_Beta
PVSEMACS=/Applications/Emacs.app/Contents/MacOS/Emacs

Start pvs by running /Applications/PVS_3.3_Beta/pvs.

[edit]

Alloy Analyzer

The Alloy Analyzer is written in Java and is available in most common platforms, if you want to install it on your own machine. The instructions here relate to setting up the Alloy Analyzer on the departmental computers.

Create a directory to store your Alloy files, which we will call your work directory.
To run the Alloy Analyzer, change to your work directory and run

java -jar alloy.jar &

This will open up the environment.
The first time you use the tool, you will have to change the default path. Go to File → Preferences. A window titled Options will appear. There are two changes that have to be made here.
1. The first change is in the Default model directory. Change the file from "Models" to ".".
2. The second change is in the Path for resolving relative module names. Change this to "." as well.
Then click save followed by ok. This will save your preferences. These preferences are stored in in alloy.cfg file in your home directory.

To type check the document, simply click the Build icon. If there are no errors, the following message is seen in the messages box.

Compiling <MODEL>.als ...
Compilation successful.

To "prove" your model, the Alloy Analyzer provides a list of provable items. This list is found in the drop box to the left of the Build icon. Choose a statement to prove and then click the Execute icon. If there are no counterexamples, the following Message will appear.

No counterexample found: <ASSERT> may be valid. (00:00)

If there is a counterexample, a state diagram depicting the counterexample will be shown. Depending on the counterexample, this state diagram can sometimes be rather complicated. You can click on a particular arrow to highlight its path to help you visualize. In addition, there are several icons above. They are Viz, Tree, Text, Msgs, Layout. Clicking on the Tree or Text icons will show different ways of explaining the state diagrams. These come in handy when trying to figure out the counterexample.

If the counterexamples are large, you can also try to find a smaller counterexample by setting a smaller scope in the "check" statement of the model.

[edit]

Java PathFinder

You will also need to augment your CLASSPATH environment variable for the JPF libraries. You are probably using tcsh as your shell. If so, open your ~/.tcshrc configuration file in your favorite text editor, and add the following lines:

setenv CLASSPATH "" foreach i (/home/f85/coppit/software/javapathfinder/lib/*.jar) setenv CLASSPATH ${CLASSPATH}:$i end

Start a new shell and type echo $CLASSPATH to make sure that your change worked.
JPF is not compatible with Java 1.5. When you compile your code, use the -source and -target flags like so:

javac -source 1.4 -target 1.4 file.java
After your file is compiled, check it using JPF by running

jpf CLASSNAME

[edit]

ESC/Java 2

After setting up your path to include ~coppit/bin, just run escj Program.java.

[edit]

Blackbox Prototype

After setting up your path to include ~coppit/bin, just run blackbox. Since this is an X application, be sure you set up X tunneling correctly if you are working remotely.

[edit]