プログラム導出

プログラム導出とは、計算機科学において数学的手段を用いて仕様からプログラムを導き出すことである。

プログラムを「導出」するとは、通常そのままでは実行不可能な形式的仕様を記述し、数学的に正しい規則を適用して実行可能なプログラムに変換することを意味する。このような手法で得られたプログラムは（最初の仕様にバグがない限り）構造的に正しいことが証明されている。

形式的検証の場合、最初にプログラムを書き、それが与えられた仕様に照らして正しいことの証明を与える。この際の問題は以下の通りである。

• 結果として出てくる証明は長くて複雑になる。
• そのプログラムがどのように開発されたかを示せない。まるで「帽子から出てきたうさぎ」のように見える。

プログラム導出はそのような欠点を次のようにして改善する。

• 適切な数学的記法を新たに開発して証明を短くする。
• 仕様を操作することでプログラムを発見する。

プログラム導出とほぼ同義の用語として、transformational programming、algorithmics、deductive programming などがある。