詳細化
「操作の詳細化」は、システムの操作の仕様を実装可能なプログラム(例えば、プロシージャ)に変換することである。この過程で事前条件は弱められ、事後条件は強められる。これにより仕様に内在する非決定性を削減し、完全に決定的な実装へと変換する。