Invariant-based programming とは

不変式プログラミングは、実際のプログラム文の前に仕様と不変量が書かれたプログラミング方法論です。プログラミングプロセス中に不変量を書き留めることには、多くの利点があります。プログラマは、実際にプログラムを実装する前にプログラムの動作を明示する必要があり、実行中に不変量を動的に評価して一般的なプログラミングエラーを捕捉できます。さらに、十分に強力であれば、プログラム文の正式なセマンティクスに基づいてプログラムの正確性を証明するために不変量を使用することができます。強力で正式な証明システムに接続されたプログラミング言語と仕様言語の組み合わせは、一般的ではないプログラムの完全な検証には一般的に必要となります。この場合、プルーフの高度な自動化も可能です。
ほとんどの既存のプログラミング言語では、主な構成構造は、forループ、whileループ、if文などの制御フローブロックです。そのような言語は、不変量を書く前にプログラマが制御フローを決定することを強制するため、不変量 – 最初のプログラミングには理想的ではないかもしれない。さらに、多くのプログラミング言語は、数量演算子を持たず、一般に高次の特性を表現できないため、仕様や不変量を記述するのに適していません。
その証拠と一緒にプログラムを開発する考えは、E.W. Dijkstraに由来しています。実際にはプログラムステートメントの前にインバリアントを記述することは、M.H. van Emden、J.C. ReynoldsおよびR-J Back。