Beginner's guide to using the CIS301 proof checker

First, read the Installing and Using the CIS301 proof checker page to learn how to download, install, and start the proof checker.

This little web page means to give some simple advice and examples for using the checker. There are many examples that you can later study that are enclosed with the checker package.

The proof checker operates on a subset of the Python language, including integers, arrays, functions, assignments, conditionals, and while loops. If you try more than this, the checker will not handle it (and it will tell you so before it crashes). The checker is designed to analyze a Python program and check the correctness of any proofs you have embedded into the program. You will see many many examples of such proofs in Chapters 2,3, and 4 of the CIS301 lecture notes. Indeed, you can copy the any example from the lecture notes into a file and ask the checker to check it. So, it is a good idea to copy and test the examples in the lecture notes as you see them. (If you find any errors/problems, let me know!)

Getting started

Let's begin by checking a program that has no proofs in it at all: Within the cis301 folder, make a new folder named Exs. Within Exs, make a file named assign0.py that holds this text:

x = readInt()
sum = 0
i = 0
sum = sum + x
i = i + 1

Now, check it: double-click on the icon for Check.py and when the checker asks for the file name, type Exs/assign0.py. When the checker asks for ``options'', just hit Enter. The checker will display this log:

+--------------
| x = readInt()
  sum = 0
  i = 0
  sum = sum + x
  i = i + 1

  All assertions verified.  (-:

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

If you look inside folder Exs, you will see a new html file, assign0A.py.htm.

For the example we did, assign0A.py.html files looks just like assign0.py. Let's try again. This time, start the checker, tell it to analyze Exs/assign0.py, but when the checker asks for options, type v (for verbose). This makes the checker tell you the logical information it extracts from the program while it is reading it. If you do this and you then look at assign0A.py.htm in your web browser, you will see these annotations:



x = readInt()
#PREMISES FOR ATTACHED PROOF, IF ANY: 
# True
#PREMISES FOR NEXT LINE: 
sum = 0
#PREMISES FOR ATTACHED PROOF, IF ANY: 
# (sum == 0)
#PREMISES FOR NEXT LINE: 
# (sum == 0)
i = 0
#PREMISES FOR ATTACHED PROOF, IF ANY: 
# (i == 0)
# (sum == 0)
#PREMISES FOR NEXT LINE: 
# (i == 0)
# (sum == 0)
sum = sum + x
#PREMISES FOR ATTACHED PROOF, IF ANY: 
# (sum == (sum_old + x))
# (i == 0)
# (sum_old == 0)
#PREMISES FOR NEXT LINE: 
# (i == 0)
i = i + 1
#PREMISES FOR ATTACHED PROOF, IF ANY: 
# (i == (i_old + 1))
# (i_old == 0)
#PREMISES FOR NEXT LINE:

As best as it could, the checker showed you the logical properties that hold true (knowlege flow) within the program. If you want more properties than this, you must insert (``attach'') proof steps into the program.

Writing a proof

Here is the example with attached proof steps:

x = readInt()
sum = 0
i = 0
"""{ 1. sum == 0   premise
     2. i == 0     premise
     3.  sum == x * i   algebra 1 2  }"""
sum = sum + x
"""{ 1.  sum == sum_old  + x   premise
     2.  sum_old  == x * i     premise
     3.  sum == (x*i) + x      subst 2 1
}"""
i = i + 1
"""{ 1. i == i_old + 1      premise
     2. sum == (x * i_old) + x   premise
    3. sum == x * i             algebra 1 2
}"""

Proofs are enclosed within """{ }""". (Triple-quoted strings work like multi-line comments in python.) There is one proof step per line. Each proof step begins with a number followed by the proposition, followed by the justification.

A premise is an already-known-true fact, which follows from the logic laws for Python (e.g., the assignment law in the above example). If you check the program with the v option, the checker will show you the premises you may use in any proof you attach to the program.

Any fact proved on the last line of a previous embedded proof is also a premise for the next command that follows. (For example, the first embedded proof above proved sum == x * i on its last line. This proposition becomes a premise that can be used with the command that follows, namely, sum = sum + x. By the Python assignment law, this generates two premises for the next, attached proof, sum == sum_old + x and sum_old == x * i.)

We use algebra to generate new knowledge from premises; there are two ways:

algebra, followed by line numbers, which asks the checker to combine the facts indicated by the line numbers to do linear algebra to prove the result.
subst m n tells the checker to substitute the equality stated on line m into the proposition on line n.

If you check the above example (using the v option), here is what you get:




x = readInt()
#PREMISES FOR ATTACHED PROOF, IF ANY: 
# True
#PREMISES FOR NEXT LINE: 
sum = 0
#PREMISES FOR ATTACHED PROOF, IF ANY: 
# (sum == 0)
#PREMISES FOR NEXT LINE: 
# (sum == 0)
i = 0
#PREMISES FOR ATTACHED PROOF, IF ANY: 
# (i == 0)
# (sum == 0)
"""{ 1.OK sum == 0   premise
     2.OK i == 0     premise
     3.OK  sum == x * i   algebra 1 2  }"""
#PREMISES FOR NEXT LINE: 
# (sum == (x * i))
sum = sum + x
#PREMISES FOR ATTACHED PROOF, IF ANY: 
# (sum == (sum_old + x))
# (sum_old == (x * i))
"""{ 1.OK  sum == sum_old  + x   premise
     2.OK  sum_old  == x * i     premise
     3.OK  sum == (x*i) + x      subst 2 1
}"""
#PREMISES FOR NEXT LINE: 
# (sum == ((x * i) + x))
i = i + 1
#PREMISES FOR ATTACHED PROOF, IF ANY: 
# (i == (i_old + 1))
# (sum == ((x * i_old) + x))
"""{ 1.OK i == i_old + 1      premise
     2.OK sum == (x * i_old) + x   premise
    3.OK sum == x * i             algebra 1 2
}"""
#PREMISES FOR NEXT LINE: 
# (sum == (x * i))

The checker annotates your proofs to show that it validated your claims.

Say that something goes wrong in the proof, for example, when we check this faulty program:

x = readInt()
sum = 0
"""{ 1. sum == 1   premise
     2. i == 0     premise
     3.  sum == x * i   algebra 1 2  }"""
sum = sum + x
"""{ 1.  sum == sum_old  + x   premise
     2.  sum == sum_old  * x   algebra 1
}"""

We will see these warnings in the displayed log:

+---------------
| x = readInt()
  sum = 0
  """{ 1. sum == 1   premise
       2. i == 0     premise
       3.  sum == x * i   algebra 1 2  }"""
  WARNING: evall couldn't find var i in the store
  WARNING: evall couldn't find var i in the store
  sum = sum + x
  UNABLE TO VERIFY (sum == 1)
  UNABLE TO VERIFY (i == 0)
  """{ 1.  sum == sum_old  + x   premise
       2.  sum == sum_old  * x   algebra 1
  }"""

  UNABLE TO VERIFY (sum == (sum_old * x))

| Only partial success; please see output file.
+----------------

and when we read the annotated file, we see that the checker marked our mistakes and tried to repair them by adding assert commands that would check our claims when the program is executed later:


x = readInt()
#PREMISES FOR ATTACHED PROOF, IF ANY: 
# True
#PREMISES FOR NEXT LINE: 
sum = 0
#PREMISES FOR ATTACHED PROOF, IF ANY: 
# (sum == 0)
assert (sum == 1)  # UNABLE TO VERIFY
assert (i == 0)  # UNABLE TO VERIFY
"""{ 1.?? sum == 1   premise
     2.?? i == 0     premise
     3.OK  sum == x * i   algebra 1 2  }"""
#PREMISES FOR NEXT LINE: 
# (sum == (x * i))
sum_old = sum
sum = sum + x
#PREMISES FOR ATTACHED PROOF, IF ANY: 
# (sum == (sum_old + x))
# (sum_old == (x * i))
assert (sum == (sum_old * x))  # UNABLE TO VERIFY
"""{ 1.OK  sum == sum_old  + x   premise
     2.??  sum == sum_old  * x   algebra 1
}"""
#PREMISES FOR NEXT LINE:

IMPORTANT: Finally, here are some warnings about the programs and proofs you may write:

watch out --- if you make a serious spelling/syntax error in your program or proof, the checker will quit on the spot, as gracefully as it can, because it is not a parser/spelling checker! For example:

sum = 0
"""{ 1. sum = 0   premise }"""
sum = sum + x

contains a syntax error in Line 1 (it uses = rather than ==); when we check this, we see in the displayed log:

+-----------
| sum = 0
  """{ 1. sum = 0   premise }"""
  PARSE ERROR invalid justification or malformed assertion at token: = ('0', 'premise', '}"""')

  Due to internal error,  Analyze.py  must terminate.  Sorry.

  Please verify that the filename (and its path) are correct,
| and if so, please inspect your program for syntax errors.
+----------

It is important that you fully parenthesize nested arithmetic and logical expressions. That is, write
```
x = 2 + (3 * 4)
```
and not x = 2 + 3 * 4. And similarly, write
```
1.  (x == 2 or x == 3) or x == 4    premise
```
and not x == 2 or x == 3 or x == 4. The checker does not apply default precedences!
The checker does not know how to reason about division or modulo or fractional numbers (just yet), so don't use these.
The checker cannot handle strings just yet (except within print commands).
The checker's algebra solver does poorly with polynomials (this is why it is called a linear solver), so do not expect to use the algebra justification to prove all numerical facts. For example, the checker is unable to validate
```
x = readInt()
assert x > 1
"""{ 1. x > 1   premise
     2. x * x > x   algebra 1
}"""
```
because it has trouble comparing quadratic terms with linear ones. (It does better with equality expressions, however.) Often, you can carefully apply the subst justification to prove what you want when you work with quadratics.
Python uses indentation rather than { } brackets to remember the commands within a conditional or loop. For this reason, you must indent evenly when you write sequences of assignments. The checker also requires that you indent the first line of an embedded proof to match the indentation of the command that precedes it. Please see the examples in the CIS301 lecture notes and the DOC.txt file for correct indentation style.

Other options for checking proofs

Here are the options you can use for checking a proof:

v : verbose mode. As we saw, this makes the checker insert as comments in the output file the logical propositions that hold true because of the programming laws for Python. Use this option when you are developing your proofs.
a : all possible asserts. The proof checker retains all possible premises generated from all previous commands and proofs, for as long as it can. This can be useful when you wish to insert only few embedded proofs and wish to have available as many premises as possible for each embedded proof. On the other hand, the number of premises can grow too large to be truly useful. Try this option and see if you like it.
If you want a proof to compute more than one fact at the end of a proof, there are two ways to do this: use either the andi justification or use the return justification. Both are documented in examples in the Lecture notes and in the DOC.txt file that comes with the checker.
x : generate output python file for execution. If you are serious about executing your checked program, then use this option, and it will generate a python executable with header code, asserts, and corrections. The checker is not a true development tool at this point, but the x option makes the checker behave like Spec# and JML, two industrial-strength tools (for C# and Java, respectively) that operate in this way.
d : display internal data structures for debugging. This option is primarily for fixing coding errors within the checker itself, but you are welcome to try this if you are bored.

More examples and details

Read the CIS301 lecture notes for more examples to try. There is a precise listing of the Python language subset and the proof rules supported by the checker in the DOC.txt file that comes with the checker. That same file also contains a sequence of progressively more difficult examples that show the checker's capabilities. Finally, there are two folders that come with the checker, Ex and Exw, that are full of examples to study and check.

The checker is still under development (it was built in three intense weeks in Nov.-Dec. 2008), so please email programs/proofs that generate unexplained crashes to das@ksu.edu.