Python中的程序驗證

Question

我正在教授關於FOL和程序驗證的課程，這本書的靈感來自Mordechai Ben-Ari，計算機科學的數學邏輯，Springer，1993-2012。我想通過讓學生用Python編程來說明概念。

對於FOL我使用NLTK，它有一個很好的FOL包。

但我還沒有找到一個Python包程序驗證：將先決條件和後置條件邏輯公式，發現循環不變，驗證由步驟，等等。換句話說Python程序步驟，使用霍爾邏輯Python內部的框架和Python程序。

你知道這個任務的任何包嗎？

Answer 1

你打算教MOOC程序驗證嗎？或者它會成爲一個有顯示代碼的屏幕的普通教室？你會有白板嗎？

如果您願意使用其他工具，那麼由Philip Guo教授開發的Online Python Tutor（http://www.pythontutor.com/）是一款出色的工具。該工具可讓您逐步執行程序，顯示程序「狀態」（變量及其具體值）。據我所知，它不能直接讓你指定/推斷前/後條件或循環不變量。所以，我可以看到一個案例作爲一個老師，寫在板上的前/後條件，逐步通過程序，並通過使用蟒蛇導師顯示具體的變量值顯示條件確實成立真實的。幾乎類似的方法可用於顯示循環不變量。

話雖如此，pythontutor正在迅速流行起來，並詢問創作者有關附加功能可能只是做伎倆！