我正在教授一门关于 FOL 和程序验证的课程，灵感来自 Mordechai Ben-Ari，计算机科学的数学逻辑，Springer，1993-2012 年。我想通过让学生使用 Python 编程来说明概念。
对于 FOL，我使用的是 NLTK，它具有出色的 FOL 包。
但是我还没有找到用于程序验证的Python包：插入前置条件和后置条件逻辑公式，查找循环不变量，逐步验证Python程序等。换句话说，在Python中使用Hoare逻辑框架并用于Python程式。
你知道这个任务的任何包吗？
问问题
941 次
1 回答
1
你打算教一个关于程序验证的 MOOC 吗？或者它会是一个带有显示代码屏幕的普通教室吗？您可以使用白板吗？
如果你愿意使用额外的工具，那么由 Philip Guo 教授开发的 Online Python Tutor ( http://www.pythontutor.com/ ) 是一个很好的工具。该工具可让您逐步执行程序，显示程序“状态”（变量及其具体值）。据我所知，它不允许您直接指定/推断前置/后置条件或循环不变量。因此，我可以看到一个案例，您作为一名教师，在板上写下前置/后置条件，逐步执行程序并通过使用 pythonutor 显示变量的具体值来解释条件确实成立的类。几乎类似的方法可用于显示循环不变量。
话虽如此，pythontutor 正在迅速流行起来，向创建者询问其他功能可能会成功！
于 2014-02-10T18:53:12.097 回答