コンピュータ科学において、プログラム導出とは、数学的な手法を用いて、プログラムの仕様からプログラムを導出することである。
プログラムを導出するとは、通常は実行不可能な形式仕様を記述し、その仕様を満たす実行可能なプログラムを得るために数学的に正しい規則を適用することである。このようにして得られたプログラムは、構成上正しい。プログラムと正当性の証明は同時に構築される。
形式検証で一般的に採用されるアプローチは、まずプログラムを作成し、次にそれが与えられた仕様に準拠していることを証明することです。このアプローチの主な問題点は次のとおりです。
- その結果得られる証明は、しばしば長くて煩雑なものとなる。
- プログラムがどのように開発されたかについての説明は一切なく、まるで「帽子からウサギが出てくる」ような印象を受ける。
- もしプログラムに何らかの微妙な誤りがあった場合、それを検証しようとする試みは時間がかかり、おそらく無駄に終わるだろう。
プログラム派生は、以下の方法でこれらの欠点を克服しようと試みます。
- 適切な数学的記号を開発することにより、証明を簡潔にする。
- 仕様を形式的に操作することによって設計上の決定を行う。
プログラム導出とほぼ同義の用語としては、変換プログラミング、アルゴリズム、演繹プログラミングなどが挙げられる。
バード＝メーテンス形式は、プログラム導出のための手法である。
分散コンピューティングにおける正確性を実現するためのアプローチには、Pプログラミング言語などの研究用言語が含まれる。
参考文献
- Edsger W. Dijkstra、Wim HJ Feijen、「プログラミングの方法」、Addison-Wesley、1988 年、188 ページ
- エドワード・コーエン著『1990年代のプログラミング』、シュプリンガー・フェルラーク、1990年
- アン・カルデワイ著『プログラミング：アルゴリズムの導出』プレンティス・ホール、1990年、216ページ
- デイヴィッド・グリース著『プログラミングの科学』、シュプリンガー・フェルラーク、1981年、350ページ
- キャロル・モーガン（コンピュータ科学者）、『仕様からのプログラミング』、国際コンピュータ科学シリーズ（第2版）、プレンティス・ホール、1998年。
- エリック・C・R・ヘーナー著『プログラミングの実践理論』、2008年、235ページ
- AJM van Gasteren著。『数学的議論の形式について』。コンピュータサイエンス講義ノート第445巻、Springer-Verlag、1990年。明瞭かつ正確な証明の書き方を解説。
- Martin Rem著「小規模プログラミング演習」は、『Science of Computer Programming』第3巻（1983年）から第14巻（1990年）に掲載された。
- ローランド・バックハウス著『プログラム構築：仕様からの実装の計算』、ワイリー、2003年 。ISBN 978-0-470-84882-1。
- デリック・G・クーリー、ブルース・W・ワトソン。『プログラミングにおける構成による正しさのアプローチ』。シュプリンガー・フェルラーク、2012年。ISBN 978-3-642-27919-5小さく扱いやすい改良を用いて、数学的に正しいアルゴリズムを導出する方法を段階的に説明します。
