博士

やっほー、ロボ子！今日も面白いITニュースを見つけてきたのじゃ！

ロボ子

こんにちは、博士。今日はどんなニュースですか？

博士

今日はね、SMTソルバーを使ったプログラム検証の話！プロジェクトHoleyとか、IMPのHoare論理検証器とかが出てくるぞ。

ロボ子

SMTソルバーですか。バックエンドで使えるんですね。プロジェクトHoleyは、Pythonのプログラミングパズルを解くんですか？

博士

そうそう！記号的な式の段階的実行とSMTを組み合わせるらしいぞ。賢い！

ロボ子

IMPっていうのは、単純な命令型言語のことですか？

博士

その通り！IMPの言語仕様は、算術式とかブール式とか、文とか、色々あるんだぞ。例えば、算術式にはNum(n)とかVar(x)とかがある。

ロボ子

文には、SkipとかAssignとかがあるんですね。ループには不変条件が必要なんですね。

博士

そう！ループが検証条件を生成するんだ。Hoareトリプル{P} S {Q}を検証するプロセスは、まずwpVc(S, Q)を計算して、メインのVC（P => wp）を生成する。

ロボ子

そして、すべてのVCを収集して、SMT-LIBに変換して充足可能性をチェックするんですね。

博士

その通り！例えば、最大値を求めるプログラムの検証プロセスが紹介されているぞ。if (x < y) then m := y else m := xみたいな。

ロボ子

事前条件がtrueで、事後条件が((m = x || m = y) && (x <= m && y <= m))ですね。

博士

そうそう！検証条件はSMTソルバーで検証できるんだ。実行方法はsbt runらしいぞ。

ロボ子

検証器の出力は、生成されたVCの数とか、SMT-LIBスクリプトなんですね。

博士

構成的検証っていうのは、各構成要素に明確なWPルールがあるってことだぞ。ループ不変条件はwhileループに必要で、VCを生成する。

ロボ子

SMT統合は、VCを自動解決のためにSMT-LIBに変換することですね。勉強になります。

博士

つまりだ！この技術を使えば、プログラムのバグを自動で見つけられる可能性が広がるってことじゃ！

ロボ子

それはすごいですね！ソフトウェアの信頼性が向上しますね。

博士

じゃあ、ロボ子。今日はこの辺で終わりにするかの。最後に一つ、SMTソルバーって、まるでプログラムの探偵みたいじゃない？

ロボ子

確かにそうですね！でも、博士はいつもお茶目なことを言いますね。