Installing and Using the CIS301 proof checker

The CIS301 proof checker helps you write and check correctness proofs like the ones presented in the CIS301 lecture notes. The checker is meant to be ``lightweight'' in that it is small, works with text files, and is used with an edit window and a web browser.

To use the checker, you must have the Python language installed on your computer. If you have a Mac, you already have Python; if you have installed Cygwin on Windows, you already have Python. Many Windows machines already have Python as well. (See the end of this note to learn about installing Python.)

Installing the Checker

From the CIS301 web page, download the zip-file, cis301.zip. Uncompress (unzip) the file, and extract from within it a copy of the folder, cis301. Save the cis301 folder on your computer in the place where you keep your coursework folders (e.g., your My Documents folder, if you are a Windows user).

Within the cis301 folder, you will find a folder, Checker, that holds the proof checker, two folders of example programs to check (Ex and Exw), and README and DOC files.

Using the Checker

You can start the checker by double-clicking on its icon or by running it from within a command window:

The simplest way to start the checker is to enter (open) the Checker folder and double-click on Check.py. (You can do this if Check.py is displayed with an S-like or snake-like icon, which stands for Python programs.) Double-clicking starts the checker, which will ask you for the filename to check. (Note: if Check.py is not displayed with the snake icon, it likely means that you must install Python. Please skip to the bottom of this note to learn how.)

When you start Check.py, you will see a window appear on your display, asking which file you wish to check. You can use any of the examples in the folder Exw (or Ex) to try. Here is a sample dialog, where some person named ``schmidt'' installed the checker and asked it to analyze the program, Exw/while.py:

+-------
|  Command-line usage: python Check.py [-args] FILENAME.py
   where  args  can be any or all of
      v : verbose mode: insert deduced asserts as comments in output
      a : include all possible asserts in proof output as premises
      x : insert header and assert code in output file for execution
      n : do not generate html file for viewing
      d : display internal data structures for debugging

   Entering interactive mode. (Press Enter to quit.)

   Current path is   C:\Documents and Settings\schmidt\cis301

   Type filename (relative to current path) to check:  Exw/while.py
   Type options (any or none of  vaxnd): v

     ... the analysis will be displayed here and also saved in two files  ...

|  Press  Enter  to repeat with this file; Press  q  to quit: 
+------

The analysis creates two files, both saved where the input file lived: whileA.py, the input file annotated with the results of the checks; whileA.py.html, an html-formatted, multi-color version of whileA.py that you can view in your web browser. (The latter is useful when you are developing a proof in stages.)

For repeated use of the checker, you should make a shortcut icon and place it on your Desktop:

In Windows XP, to generate a shortcut, open the Checker folder, right-click on Check.py, and select ``Create Shortcut''. Then, move the shortcut icon to where you will find it most convenient to use, e.g., your Desktop.
To use the checker, double click on its shortcut. This will generate an interactive session, where you are asked the name of the file that you wish analyzed and any execution options.

While you are developing and checking a program, you can use an edit window to type your program and a web browser to view the results. You can also repeat the analysis on the same file over and over; this is useful for developing a program and its correctness proof in stages.

You should study the README.txt file that is included within the cis301 folder for advice about where to make a folder that holds the programs you write and check. There is also a beginner's guide you should read before you write any programs/proofs of your own.

Using the checker from the command window

Unix and Linux users often like using a command window to edit and run programs. You can also do this with a Windows machine.

Try opening a command window and typing python. If you get the ``not found'' message, please read the web page, Using Python from a command window to learn how to set the Path variable on a Windows machine. (If you are using Linux, update the PATH variable within your startup script, e.g., .bashrc, so that it includes the path to the folder where python is installed).

Once you have the Path variable set, you can use the checker like this: cd to cis301, and type this at the command line:

python Checker/Check.py

This starts the session. If you prefer to use command-line arguments, you may do so, like this:

python Checker/Check.py -v Ex/while.py

Then, by pressing the up-arrow key on your keyboard, you can repeat the analysis over and over....

It is a bit of a nuisance to always start from the cis301 folder and always type the python Checker/Check.py part. If you are a Unix/Linux user, you can write an alias command like this one and place it in your startup script (.bashrc):

alias run301='python /home/Myname/Mystuff/cis301/Checker/Check.py'

where /home/Myname/Mystuff/cis301/Checker/Check.py is the complete path to the checker. Then, you can start the checker from the command window like this:

run301 -v Ex/while.py

Installing Python if you do not have it

Say that you double-click on Check.py and it does not start. It is likely that your computer lacks Python.

To see if your computer has Python installed, you can try these tricks:

On a windows machine:
In your My Documents folder (or Desktop), use Notepad to make a file named Hello.py and place in the file the single line,
```
raw_input("hello")
```
Then, try double clicking on the file's icon to start the program. If it starts and prints hello, you have python installed correctly on your machine.
Or, from the Start menu, use Search to search all files and folders for the file, python.exe. If the search command finds it, it will show you where.
On a Linux machine (or MacOS that lets you start a Unix command window): Type the command, which python
If Python is installed correctly, you will see the directory path to it.

Important: your computer must have Python 2.4 or newer up to but not including Python 3.0. (This is normally not a problem --- most machines have 2.6 these days.)

If you must install Python, you will find it easy: Go to http://www.activestate.com/activepython/downloads. Download either Version 2.6.5 or 2.7.0. Do not download Version 3.1, which is incompatible with the checker tool.

Try your implementation by using Notepad to make a file named Hello.py and place in the file the single line,

raw_input("hello")

Then, try double clicking on the file's icon to start the program. If it starts and prints hello, you are good to go. (Or, try starting the program from a command window, like this: python Hello.py)