プログラム導出
プログラム導出とは、計算機科学において数学的手段を用いて仕様からプログラムを導き出すことである。
プログラムを「導出」するとは、通常そのままでは実行不可能な形式的仕様を記述し、数学的に正しい規則を適用して実行可能なプログラムに変換することを意味する。このような手法で得られたプログラムは（最初の仕様にバグがない限り）構造的に正しいことが証明されている。
形式的検証の場合、最初にプログラムを書き、それが与えられた仕様に照らして正しいことの証明を与える。この際の問題は以下の通りである。
- 結果として出てくる証明は長くて複雑になる。
- そのプログラムがどのように開発されたかを示せない。まるで「帽子から出てきたうさぎ」のように見える。
プログラム導出はそのような欠点を次のようにして改善する。
- 適切な数学的記法を新たに開発して証明を短くする。
- 仕様を操作することでプログラムを発見する。
プログラム導出とほぼ同義の用語として、transformational programming、algorithmics、deductive programming などがある。
関連項目
[編集]参考文献
[編集] |
- Edsger Dijkstra, Wim H. J. Feijen, A Method of Programming, Addison-Wesley, 1988年, 188ページ
- Edward Cohen, Programming in the 1990's, Springer-Verlag, 1990年
- Anne Kaldewaij, Programming: The Derivation of Algorithms, Prentice-Hall, 1990年, 216ページ
- David Gries, The Science of Programming, Springer-Verlag, 1981年, 350ページ
- A.J.M. van Gasteren. On the Shape of Mathematical Arguments. Lecture Notes in Computer Science #445, Springer-Verlag, 1990年. 明確で正確な証明の書き方