|
We will use an on-line text I have written, found at the
Lectures
page on this site. The text isn't perfect, but I am saving you
$100 this way....
- Proof checker for Floyd-Hoare program logic:
We will develop correctness proofs for programs
with the assistance of a checker tool
that I have written:
- The checker runs on top of Python.
Please read
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.
Read the
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
beginner's guide
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:
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 rather than iterative.
For this reason, we will do at least one exercise with it.
If you have never programmed in Python before, you can relax ---
it looks like Visual Basic or Javascript or any other baby assignment
language. But it has powerful dynamic data structures (lists and
dictionaries).
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.
-
* The language's website is at
http://www.python.org/,
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
practice.
-
- 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:
-
Prolog:
At the end of the course, we will take a quick look at the Prolog
programming language.
There is a good, easy-to-install implementation at
www.swi-prolog.org.
|
