6

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?

Improve this question
3
  • 1
    ummmm unittest + mock ? Commented Feb 10, 2014 at 18:23
  • FOL == First Order Logic? Commented Feb 10, 2014 at 18:28
  • Yes, FOL = First Order Logic, sorry for taking that for granted Commented Feb 11, 2014 at 10:15

1 Answer 1

Reset to default
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!

Improve this answer
Sign up to request clarification or add additional context in comments.

Comments

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.