形式仕様：命令を超えて、ソフトウェアの振る舞いを定義する

この記事では、形式仕様と従来のプログラムの違いを掘り下げています。プログラムは命令のリストですが、形式仕様は振る舞いの集合です。著者はカウンターの例を用いて、仕様がすべての正しい振る舞いをどのように定義し、集合論を利用して、ジェネレータ（InitとNext）を用いて無限の振る舞いの集合を記述するかを示しています。これは、プログラミングにおける非決定性の概念とは対照的です。形式仕様における非決定性は、振る舞いを拡張できる複数の方法を指しますが、プログラムにおける非決定性は、不確かなコードパスを指します。この記事は、形式仕様を振る舞いの集合として理解することの重要性を強調しており、これはデバッグとモデルチェッカーのエラーの解釈に不可欠です。