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