詳細化

出典: フリー百科事典『ウィキペディア（Wikipedia）』

詳細化（しょうさいか、Refinement）とは、形式手法において、抽象的な形式仕様記述から具体的な実行プログラムへと検証可能な変換を行うことである。

[編集] 概要

段階的な詳細化として段階を踏んで詳細化を行うこともできる。論理的には、詳細化は含意による変換であるが、追加的な複雑化を生じる要因もある。「データの詳細化」は、抽象的データモデル（例えば集合）を実装可能なデータ構造（例えば配列）に変換することである。「操作の詳細化」は、システムの操作の仕様を実装可能なプログラム（例えば、プロシージャ）に変換することである。この過程で事前条件は弱められ、事後条件は強められる。これにより仕様に内在する非決定性を削減し、完全に決定的な実装へと変換する。

例えば、変数 x にある操作を行った後の値が x' ∈ {1,2,3} であるとする。この操作を x' ∈ {1,2} となる操作に詳細化し、さらに x' ∈ {1} となる操作に詳細化する。そして、x := 1 として実装する。同様に別の経路の詳細化によって x := 2 や x := 3 が得られる。ただし、x' ∈ {} となる操作（偽と等価）は実装不可能なので詳細化されない。空集合から要素を取り出すことはできないのである。

類似の用語として Reification（具象化）がある（Cliff Jones が使用した用語で、オブジェクト指向設計におけるデータモデルの詳細化を指す）。形式的な詳細化が不可能な場合の代替技法を Retrenchment（削減）と呼ぶ。詳細化の反対語は抽象化である。