I teach a FOL and program verification course inspired by Mordechai Ben-Ari's book, Mathematical Logic for Computer Science, Springer, 1993-2012. I would like to illustrate the concepts by having a student program in Python.
For FOL, I use NLTK, which has a great FOL package.
But I have not yet found a Python package for checking the program: inserting the logical formulas of the precondition and postconfiguration, searching for loop invariants, step-by-step execution of the Python program, etc. In other words, using the Hoare logical structure inside Python and for Python programs.
Do you know of any package for this task?
source
share