Refinement calculus とは

リファインメント計算は、プログラム構築のための段階的リファインメントへの形式化されたアプローチである。最終的な実行可能プログラムの必要な振る舞いは、抽象的かつおそらく実行不可能な「プログラム」として指定され、一連の正当性保持の変換によって効率的に実行可能なプログラムに洗練される。
提案者には、1978年の「プログラム開発の精緻化ステップの正確性に関する論文」とキャロル・モルガンの「プログラミングからのプログラミング」(Prentice Hall、1994年第2版、ISBN 0-13)のアプローチを起したRalph-Johan Back -123274-6)。後者の場合、動機づけは、Abjellの仕様表記Zを、動作を維持するプログラム洗練の厳密な関係を介して、Dijkstraの保護されたコマンドの言語に基づく実行可能なプログラミング記法にリンクすることであった。この場合の行動保存とは、プログラムによって満足されるすべてのHoareトリプルが、その洗練されたものによって満たされなければならないことを意味する。この概念は、前提条件と事後条件として、それらの間に置かれる。