私は、Mordechai Ben-Ari 著『Mathematical Logic for Computer Science』、Springer、1993-2012 という本に触発されて、FOL とプログラム検証に関するコースを教えています。学生に Python でプログラムしてもらうことで、概念を説明したいと思います。
FOL には、優れた FOL パッケージを持つ NLTK を使用しています。
しかし、プログラム検証用の Python パッケージはまだ見つかりませんでした: 前提条件と事後条件の論理式を挿入し、ループ不変条件を見つけ、Python プログラムを段階的に検証します。つまり、Python 内および Python で Hoare 論理フレームワークを使用するプログラム。
このタスクのパッケージを知っていますか?
プログラムの検証について MOOC を教えますか? それとも、コードを表示する画面を備えた通常の教室になるのでしょうか? ホワイトボードは自由に使えますか？
追加のツールを使用する場合は、Philip Guo 教授 ( http://www.pythontutor.com/ ) によって開発された Online Python Tutor が優れたツールです。このツールを使用すると、プログラムの実行をステップ実行して、プログラムの「状態」(変数とその具体的な値) を表示できます。私が知っている限りでは、事前/事後条件またはループ不変条件を直接指定/推測することはできません。そのため、教師としてボードに事前/事後条件を書き、プログラムをステップ実行して、 python tutor を使用して変数の具体的な値を示すことで、条件が実際に成立することをクラスに説明するケースを見ることができます。ループの不変条件を示すために、ほぼ同様のアプローチを使用できます。
そうは言っても、pythontutor は急速に人気が高まっており、作成者に追加機能について尋ねるだけでうまくいくかもしれません!