Program verification in Python

Question

I'm teaching a course on FOL and program verification inspired by the book Mordechai Ben-Ari, Mathematical Logic for Computer Science, Springer, 1993-2012. I would like to illustrate notions by having the students program in Python.

For FOL I am using NLTK, which has an excellent FOL package.

But I haven't found yet a Python package for program verification: inserting precondition and postcondition logical formulas, find loop invariants, verifying a Python program step by step, etc. In other words, to use a Hoare logic framework inside Python and for Python programs.

Do you know of any package for this task?

Answer 1

Are you going to teach an MOOC on program verification? Or is it going to be a regular classroom with a screen for displaying code? Will you have a white-board at your disposal?

If you are willing to use additional tools, then Online Python Tutor, developed by Prof. Philip Guo (http://www.pythontutor.com/) is an excellent tool. The tool lets you step through the program execution, showing program 'state' (variables and their concrete values). As for as I know, it does not directly allow you to specify/infer pre/post conditions or loop invariants. So, I can see a case where you, as a teacher, write pre/post conditions on a board, step through the program and explain the class that the conditions indeed hold true by showing concrete values of variables using python tutor. Almost similar approach can be used for showing loop invariants.

Having said this, pythontutor is rapidly getting popular and asking the creator about additional features might just do the trick!