改良（コンピューティング）

改良とは、正しいコンピュータ プログラムを作成し、既存のプログラムを簡素化して形式検証を可能にするため のさまざまなアプローチを網羅するコンピュータ サイエンスの一般的な用語です。

形式手法では、プログラムの改良とは、抽象的な（高レベルの）形式仕様を具体的な（低レベルの）実行可能プログラムに検証可能に変換することです。^[要出典]段階的な改良により、このプロセスを段階的に実行できます。論理的には、改良には通常、含意が含まれますが、追加の複雑さが生じる可能性があります。

スクラムなどのアジャイルソフトウェア開発アプローチにおける製品バックログ（要件リスト）の段階的なジャストインタイムの準備は、一般的にリファインメントとも呼ばれます。^[1]

データの洗練は、抽象データ モデル (セットなど) を実装可能なデータ構造(配列など) に変換するために使用されます。^[要出典]操作の洗練は、システム上の操作の仕様を実装可能なプログラム(手順など)に変換します。このプロセスでは、事後条件を強化したり、前提条件を弱めたりすることができます。これにより、仕様の非決定性は低減され、通常は完全に決定論的な実装になります。

たとえば、x ∈ {1,2,3} ( x は演算後の変数 xの値) は、 x ∈ {1,2} に精製され、次にx ∈ {1} となり、x := 1 として実装されます。 この場合、精製に別のルートを使用すれば、 x  := 2 とx := 3 の実装も 同様に受け入れられます。 ただし、x ∈ {} ( falseに相当) に精製しないように注意する必要があります。 これは実装不可能であり、空集合からメンバーを選択することは不可能です。

具体化という用語も時々使用されます (クリフ・ジョーンズによる造語)。削減は、形式的な洗練が不可能な場合に代替となる手法です。 洗練の反対は抽象化です。

改良計算は、プログラムの改良を促進する形式システム( Hoare 論理からヒントを得たもの)です。FermaT 変換システムは、改良の産業用実装です。B メソッドも、改良計算をコンポーネント言語で拡張した形式手法であり、産業開発で使用されています。

型理論において、洗練型^{[2] [3] [4]}は、洗練型の任意の要素に対して成立すると想定される述語を備えた型である。洗練型は、関数の引数として使用される場合の前提条件、または戻り値の型として使用される場合の事後条件を表現できる。たとえば、自然数を受け入れ、5より大きい自然数を返す関数の型は、 と記述される。したがって、洗練型は動作サブタイピングに関連している。 ${\displaystyle f:\mathbb {N} \rightarrow \{n:\mathbb {N} \,|\,n>5\}}$

• 具象化（コンピュータサイエンス）