博士

ロボ子、最近形式仕様に関する面白い記事を見つけたのじゃ。AmazonのAIツールがきっかけらしいぞ。

ロボ子

形式仕様ですか。従来のプログラムとは違うものなのですよね？

博士

そうじゃ！従来のプログラムは一連の動作を記述するものだけど、形式仕様はそうではないのじゃ。

ロボ子

記事では、FizzBee、P、PlusCal、Quint、TLA+といったツールが紹介されていますね。これらはプログラミング言語のような記法を使うのですね。

博士

その通り！HarelとPneuliという人が、ソフトウェアを「変換型」と「反応型」に分けたのは知ってるかの？

ロボ子

名前は聞いたことがあります。変換型は単一の入力から単一の出力を生成するタイプで、反応型は長期にわたって動作し、入力を継続的に受け取るタイプでしたっけ。

博士

よく覚えておるの！形式仕様は、特に反応型システムに適用されるのじゃ。

ロボ子

記事ではカウンタの例が挙げられていますね。`inc()`、`get()`、`reset()`の操作をサポートするカウンタ。

博士

そうじゃ。動作（execution history/trace）は、入力と出力のシーケンスで、形式仕様は、与えられた動作が正しいかどうかを判断するのじゃ。

ロボ子

つまり、形式仕様は正しい動作の集合として考えられるのですね。

博士

その通り！形式仕様言語を使うと、無限の動作集合を明示的に列挙せずに定義できるのじゃ。

ロボ子

TLA+では、形式仕様はInit（初期状態）とNext（状態遷移）のペアで構成されるとありますね。

博士

そうじゃ！そして、形式仕様における非決定性（nondeterminism）は、正しい動作が複数のパスで拡張できることを意味するのじゃ。

ロボ子

形式仕様は、システムの正当性を検証するために構築されるのですね。正当性特性（correctness properties）を定義し、モデル検査ツールでチェックすると。

博士

その通り！特性は動作の集合で、仕様が特性を満たすかどうかを検証することで、仕様の誤りを検出できるのじゃ。

ロボ子

形式仕様を書く際には、動作の集合として考えることが重要なのですね。

博士

よく理解しておるの。ところでロボ子、形式仕様を完璧に理解した記念に、ロボットのロボットによるロボットのための形式的なお茶会でも開くかのじゃ？

ロボ子

博士、それは一体どんな形式なのでしょうか…？