不変式とは？

不変式（Invariant）とは、プログラムの特定の地点や範囲において、実行の前後や途中を問わず常に真であることが保証される論理的な条件・性質のことです。プログラムの正しさ（correctness）を形式的に議論するための核心概念です。

不変式はその適用範囲によっていくつかの種類に分かれます。

• ループ不変式：ループの各イテレーション開始時に常に成り立つ条件。ループの正しさを証明するために使われる（例：「iが0以上かつn以下である」）
• クラス不変式：オブジェクト指向プログラミングにおいて、オブジェクトが有効な状態にあるときに常に成り立つ条件（例：「スタックのサイズは0以上かつ最大容量以下」）
• 型不変式：型システムが保証する性質（例：「null安全な型には必ず値が存在する」）

不変式は契約プログラミング（Design by Contract）の重要な要素の一つであり、事前条件・事後条件とともにコードの仕様を明確化します。EiffelやAdaなどの言語は不変式を言語機能として組み込んでおり、JavaのassertやC++のassert、Rustの型システムなどでも類似の役割を果たします。

不変式を明示することで、バグの早期発見・リファクタリングの安全性向上・コードのドキュメント化という三つの効果が得られます。テスト駆動開発や形式手法と組み合わせることで、より信頼性の高いソフトウェアの開発につながります。