Loading article…
改良とは、コンピュータ科学における一般的な用語であり、正しいコンピュータプログラムを作成したり、既存のプログラムを簡略化して形式検証を可能にするための様々な手法を包括する。
形式手法において、プログラムの洗練とは、抽象的な（高レベルの）形式仕様を具体的な（低レベルの）実行可能なプログラムへと検証可能な形で変換することである。段階的な洗練によって、このプロセスを段階的に行うことができる。論理的には、洗練には通常、含意が伴うが、さらに複雑な問題が生じる場合もある。
スクラムなどのアジャイルソフトウェア開発手法における、製品バックログ（要件リスト）の段階的なジャストインタイム準備は、一般的にリファインメントとも呼ばれます。[ 1 ]
データリファインメントは、抽象的なデータモデル（例えば集合）を実装可能なデータ構造（配列など）に変換するために使用されます。操作リファインメントは、システム上の操作の仕様を実装可能なプログラム（例えばプロシージャ）に変換します。このプロセスでは、事後条件を強化したり、事前条件を弱めたりすることができます。これにより、仕様における非決定性が低減され、通常は完全に決定論的な実装になります。
例えば、x ∈ {1,2,3} (ここでxは演算後の変数xの値) は、 x ∈ {1,2}、次にx ∈ {1} に絞り込み、x := 1として実装できます。この場合、 x := 2 とx := 3 の実装も同様に許容されますが、絞り込みの方法は異なります。ただし、 x ∈ {} ( false と同等)に絞り込むことは実装不可能なので注意が必要です。空集合から要素を選択することは不可能です。
具体化という用語も時折用いられる（クリフ・ジョーンズが造語）。形式的な洗練が不可能な場合、縮小は代替的な手法となる。洗練の反対は抽象化である。
洗練計算は、プログラムの洗練を促進する形式体系（ホーア論理に着想を得たもの）です。FermaT変換システムは、産業レベルで利用可能な洗練の実装例です。Bメソッドもまた、コンポーネント言語を用いて洗練計算を拡張した形式手法であり、産業開発において活用されています。
型理論において、リファインメント型[ 2 ] [ 3 ] [ 4 ]とは、リファインメント型の任意の要素に対して成り立つと仮定される述語を備えた型のことである。リファインメント型は、関数の引数として使用される場合には事前条件を、戻り値の型として使用される場合には事後条件を表現できる。例えば、自然数を受け取り、5より大きい自然数を返す関数の型は、次のように記述できる。洗練タイプは、行動のサブタイプ化と関連している。
