不変式ベースのプログラミング

不変式ベースプログラミング^{[ 1 ]}は、実際のプログラム文の前に仕様と不変条件を記述するプログラミング手法です。プログラミングプロセス中に不変条件を記述することには、いくつかの利点があります。プログラマは実際に実装する前にプログラムの動作に関する意図を明示的に示す必要があり、不変条件は実行中に動的に評価され、一般的なプログラミングエラーを検出できます。さらに、十分に強力であれば、不変条件を使用して、プログラム文の形式意味に基づいてプログラムの正しさを証明することができます。一般に、非自明なプログラムを完全に検証するには、強力な形式証明システムに接続されたプログラミング言語と仕様言語の組み合わせが必要です。この場合、証明の高度な自動化も可能です。

for既存のプログラミング言語のほとんどでは、ループ、whileループ文、if文といった制御フローブロックが主要な構成構造となっています。このような言語は、不変条件を記述する前に制御フローについてプログラマが決定を下す必要があるため、不変条件優先プログラミングには適さない可能性があります。さらに、ほとんどのプログラミング言語は量指定子演算子を欠いており、高階プロパティを表現できないことが多いため、仕様記述や不変条件の記述が適切にサポートされていません。

プログラムとその証明を開発するというアイデアは、EW Dijkstraに端を発しています。プログラム文の前に不変式を実際に記述するというアイデアは、MH van Emden、 JC Reynolds、RJ Backによって様々な形で検討されてきました。