改良計算

改良計算は、プログラム構築のための段階的な改良に対する形式化されたアプローチです。最終的な実行可能プログラムの必要な動作は、抽象的で実行不可能な「プログラム」として指定され、その後、一連の正確性を維持する変換によって効率的に実行可能なプログラムに改良されます。^[1]

支持者には、1978 年の博士論文「プログラム開発における改良手順の正確性について」でこの手法を考案したRalph-Johan Backや、特に著書「仕様からのプログラミング」 (Prentice Hall、第 2 版、1994 年、ISBN 0-13-123274-6 ) でこの手法を提唱したCarroll Morgan などがいます。後者の場合、動機は、動作保存プログラム改良の厳密な関係を介して、 Abrialの仕様表記Z を、 Dijkstraの保護されたコマンドの言語に基づく実行可能なプログラミング表記にリンクすることでした。この場合の動作保存とは、プログラムによって満たされるHoare トリプルは、そのプログラムのすべての改良によっても満たされる必要があることを意味します。この概念は、事前条件と事後条件としての仕様ステートメントを直接的に導き、その間に適切に配置できるすべてのプログラムに対して、それらのステートメントが単独で成り立つようにします。