形式手法の基礎

あるゲームで、2 人のプレイヤーが同じ瞬間に最後のチケットを取れるとします。1000 回テストしても動きます。ところがバグは出来事のある特定の順番で起き、1001 回目に現れます。形式手法はケースを試しません。機械にすべてのケースを調べさせます。

• 性質: システムについて、いつも成り立つべき主張。
• ソルバー: ルールに合う値を見つけるプログラム。
• モデル検査器: モデルが到達できるすべての状態を試すプログラム。
• 不変条件: すべての状態で成り立つべき性質。
• 反例: 性質が偽であることを示す実行。
• モデル: 細部を省いた、システムの小さな説明。

Z3 はソルバーです。ルールを渡すと、例といっしょに sat (充足可能: 合う値がある) と答えるか、unsat (合う値がない) と答えます。最初のコマンドはバージョンを表示します。2 つ目は、3 より大きく 6 より小さい数 x を求め、Z3 は sat と答えて x を 4 とします。3 つ目は、5 より大きく 3 より小さい数を求め、Z3 は unsat と答えます。こうして証明します。主張を証明するには、それが成り立たないケースを求めて unsat を得ます。

SPIN は Promela で書いたモデルを検査します。あなたのラボにもあり、2 人の作業者が共有のカウンターに 1 を足し、ロックはまだ何もしません。spinrun は検査器を作り、作業者が取りうるすべての順番に対して実行します。assertion violated (inside==1) と errors: 1 を表示し、トレースを残します。2 つ目のコマンドはそのトレースを 1 歩ずつ再生します。どちらかが出る前に、両方の作業者が inside = (inside+1) を実行しています。

TLA+ はシステムを状態とステップで記述し、TLC がそれを検査します。ラボの Lock.tla には 2 つのプロセスがあり、それぞれ idle、wait、cs (クリティカルセクションの中) のどれかです。この不変条件は、両方が同時に待っていることはない、と言っています。これは正しいロックにとっても偽で、TLC は Invariant NotBothWaiting is violated と、両方のプロセスが wait になる 3 状態の反例を表示します。ラボ本来の課題は別の不変条件です。

Alloy は物と物の関係を記述し、主張を壊す小さな例を探します。ここでは物は人で、関係は誰が誰の友人かです。alloy はファイルの 2 つのコマンドを実行します。check Symmetric は SAT を表示します。Alloy が反例を見つけたのです。一方が相手を友人と数え、相手は数えない 2 人で、Person$1->Person$0 と表示されます。run Meet も SAT を表示し、見るための例が見つかったことを示します。check では、SAT は主張が偽ということです。