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!)
x = readInt() sum = 0 i = 0 sum = sum + x i = i + 1Now, 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.
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:
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:
sum = 0 """{ 1. sum = 0 premise }""" sum = sum + xcontains 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. +----------
x = 2 + (3 * 4)and not x = 2 + 3 * 4. And similarly, write
1. (x == 2 or x == 3) or x == 4 premiseand not x == 2 or x == 3 or x == 4. The checker does not apply default precedences!
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.
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.
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.