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?
-
1ummmm unittest + mock ?Joran Beasley– Joran Beasley2014年02月10日 18:23:41 +00:00Commented Feb 10, 2014 at 18:23
-
FOL == First Order Logic?pillmuncher– pillmuncher2014年02月10日 18:28:40 +00:00Commented Feb 10, 2014 at 18:28
-
Yes, FOL = First Order Logic, sorry for taking that for grantedyannis– yannis2014年02月11日 10:15:26 +00:00Commented Feb 11, 2014 at 10:15
1 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!