博士

ロボ子、AmazonがAIツールを発表したみたいじゃな。形式仕様って言葉が出てきたけど、従来のプログラムとどう違うのか、ちょっと解説してみようかの。

ロボ子

形式仕様ですか。最近、FizzBee、P、PlusCal、TLA+といったツールもよく耳にしますね。プログラムとはどう違うんでしょう？

博士

良い質問じゃな！プログラムは命令のリスト、形式仕様は動作の集合と考えると分かりやすいぞ。記事にもそう書いてある。

ロボ子

動作の集合、ですか。具体的にはどういうことでしょう？

博士

ソフトウェアには、単一の入力を受け取って単一の出力を生成するタイプと、長期にわたって入出力を繰り返すタイプがあるじゃろ？ HarelとPnueliはそれぞれtransformational、reactiveと呼んだそうじゃ。

ロボ子

コンパイラはtransformational、航空機のフライト制御ソフトウェアはreactiveの例ですね。サービスもreactiveシステムの好例とのこと。

博士

その通り！カウンターを例に考えてみよう。`inc()`、`get()`、`reset()`の操作があるとする。形式仕様では、これらの操作によって起こりうる全ての動作を記述するのじゃ。

ロボ子

システムの実行履歴を「behavior」と呼ぶんでしたね。形式仕様は、与えられたbehaviorが正しいかどうかを判断する役割を持つ、と。

博士

そうじゃ！仕様は、正しいbehaviorをすべて含む集合として考えることができる。形式仕様言語は、無限のbehavior集合を明示的に列挙せずに定義する手段を提供するのじゃ。

ロボ子

TLA+では、仕様はInit（初期状態）とNext（状態遷移）の2つの部分で構成されて、behaviorを生成するんですね。

博士

その通り！形式仕様における非決定性（nondeterminism）は、正しいbehaviorの拡張方法が複数存在することを意味する。例えば、カウンターが複数のクライアントから同時にアクセスされる場合じゃな。

ロボ子

なるほど。形式仕様は、システムの正しさについて推論するために構築されるんですね。

博士

そうじゃ！仕様が正しいことを検証するために、「correctness properties」を定義して、モデル検査ツールで検証するのじゃ。propertyもbehaviorの集合であり、仕様がpropertyを満たすかをチェックすることで、仕様の正しさを検証できる。

ロボ子

形式仕様を書く際には、behaviorの集合として考えることが重要なんですね。なんだか難しそうですが、奥が深そうですね。

博士

難しく考えずに、色々なシステムの動きをbehaviorとして捉えてみると面白いぞ。例えば、ロボ子が私にコーヒーを淹れるというbehaviorは…

ロボ子

博士、またコーヒーの話ですか… 形式仕様で考えると、コーヒー豆の種類、水の温度、抽出時間など、様々な要素が絡み合って、無限のbehaviorが…

博士

そうそう！そして、私が「もっと甘く！」とか「濃いめ！」とか言い出すことで、さらにbehaviorが複雑になるのじゃ！

ロボ子

もう、博士ったら！ 形式仕様は奥が深いですが、博士のわがままも底なしですね…

博士

まあ、形式仕様も私のコーヒーの好みも、突き詰めれば無限の可能性を秘めている、ということで…一件落着！