We will use an on-line text I have written, found at the
page on this site.
- Proof checker for Floyd-Hoare program logic:
We will develop correctness proofs for programs
with a checker tool
that I have written:
- The checker runs on top of Python.
Installing Python to learn how
to check for Python on your machine, install it if needed, and later
use it to develop software.
Download the checker tool to your computer:
cis301.zip. It holds the checker.
installation guide to learn how to
install the checker.
If it is impossible for you to unzip cis301.zip,
here is the link to the cis301 folder.
Download from here as a last resort.
- Next, read the
to using the checker. This should be enough to get you started.
There's more, if you're curious:
Here is the README file
that is contained in the zip file.
There is also a
DOC.txt file that defines precisely
the language understood by the checker.
The DOC file also includes a series of progressively more fiendish
examples that the checker will analyze and approve.
Python is a nice complement to Java, C#, etc., because it is a dynamically
typed and structured language rather than a static one,
and it naturally supports recursive programming.
We will do at least one exercise with it.
If you have never programmed in Python before, you can relax ---
language. But it has powerful dynamic data structures (lists and
Here are some samples of Python code.
(Here is a zipped folder of the samples.)
Try these with your implementation.
Some other materials:
a terse language summary and
terse notes on lists and dictionaries,
the two most important data structures in Python. Here is
a complete tutorial, from
the days when I taught CIS200.
* pythontutor.com runs a Python script one line at a time and shows you the run-time stack-heap configurations that result.
* The language's website is at
where you will find a useful
library reference page.
* This nice on-line book,
The Python Standard Libary,
shows you how to use Python to do clever systems hacking and gluing,
the sort of stuff that is not normally taught in courses but is hugely useful in
- Symbolic-logic proof checker:
When we study Chapters 5 and 6 of the on-line text,
we will use a tool developed in-house by Mr. Brian Mulanda,
Dr. Rod Howell, and Mr. James Thompson for checking logic proofs. The tool runs on top of Java.
If you have Java installed on your computer (very likely), then
you can download the tool to your Desktop and double-click
to start it:
At the end of the course, we will look at the Prolog
There is a good, easy-to-install implementation at