「構造化プログラミング」の版間の差分
削除された内容 追加された内容
I.hidekazu (会話 | 投稿記録) |
「プログラムの正しさの証明」についての解説を追加 |
||
38行目:
実際、ヤコピーニの論文はフローチャートやそれによって表現されるプログラム・関数・チューリングマシンなどの理論的側面に注目している。これは任意の論理回路が[[否定論理積|NAND]]素子の組み合わせによって表現できるとか、[[ラムダ計算|λ式]]がSおよびKという名の2つの[[SKIコンビネータ計算|コンビネータ]]によって表現できるとかいった研究に近い。回路設計者が直接NANDを組み合わせて電子回路を設計しないのと同じように、ヤコピーニの研究は良いプログラムの作成を(少なくとも直接的には)意図していない。
=== プログラムの正しさの証明 ===
1960年代後半、科学の領域にプログラミング方法論が現れると、初期の計算機でもてはやされたプログラムの効率を良くする技巧<ref name="bit1975_microcomputer">E.W.ダイクストラ, "マイクロコンピュータのインパクト", 川合慧 訳, ''bit'', Vol.7, Issue 6, 1975, pp.4-6, 共立出版. </ref>だけでなく、品質やプログラムの正しさという問題にも関心が集まった<ref name="from_craft_to_scientific_discipline"/>。
プログラムが正しいことをを確認するには、それを証明しなければならない<ref name="structured_programming"/>。テストはプログラムの正しさに対する疑いを全て取り除くには不十分であるとされた<ref name="systematic_programming">N.ヴィルト, "系統的プログラミング/入門", 野下浩平, 筧捷彦, 武市正人 訳, 近代科学社, 1978. </ref><ref name="how_to_sove_it_by_computer">R.Geoff Dromey, "How to Solve it by Computer", Prentice Hall, 1982. </ref>。これについてダイクストラは「テストはバグの存在を示すには有効だが、バグが存在しないことは証明できない」と表現を好んで用いた<ref name="structured_programming"/><ref name="the_humble_programmer">E.W.ダイクストラ, “謙虚なプログラマ”, ''ACMチューリング賞講演集'', 木村泉 訳, 共立出版, 1989, pp.23-43. </ref><ref name="ewd273">[http://www.cs.utexas.edu/users/EWD/transcriptions/EWD02xx/EWD273.html E.W.Dijkstra, "The Programming Task Considered as an Intellectual Challenge", 1969. ]</ref><ref name="ewd288">[http://www.cs.utexas.edu/users/EWD/transcriptions/EWD02xx/EWD288.html E.W.Dijkstra, "Concern for Correctness as a Guiding Principle for Program Composition", 1970. ]</ref><ref name="ewd361">[http://www.cs.utexas.edu/users/EWD/transcriptions/EWD03xx/EWD361.html E.W.Dijkstra, "Programming as a discipline of mathematical nature", 1973. ]</ref>。構造化プログラミングの支持者らは，プログラムの正しさの重要性と証明の方法や表明の使い方について説いた<ref name="the_science_of_programming"/><ref name="systematic_programming"/><ref name="the_craft_of_programming">[http://www.cs.cmu.edu/~jcr/craftprog.html John C. Reynolds, "The Craft of Programming", Prentice-Hall, 1981. ]</ref><ref name="how_to_solve_it_by_computer">R.G.Dromey, "How to Solve it by Computer", Prentice Hall, 1982. </ref>。理想的にはテストだけに依存せず、プログラムの正しさの証明も与えるべきである<ref name="proving_programs_correct">ロバート B.アンダーソン, "演習プログラムの証明", 有沢誠 訳, 近代科学社, 1980. </ref><ref name="basic_theorem_of_programs">小野寛晰, "プログラムの基礎理論", サイエンス社, 1975. </ref>。ダイクストラは，プログラミングと同時にプログラムの証明を進めることを推奨している<ref name="a_discipline_of_programming"/>{{#tag:ref|ダイクストラはプログラミングと証明を並行するのに適した、最弱事前条件をによる検証方法を考案した。ホーア論理は作り終わったものは証明できるが、これから作るプログラムについては指標を与えてくれない<ref name="software_cleanroom">二木厚吉 監修, "ソフトウェアクリーンルーム手法", 日科技連, 1997. </ref>。|group="注釈"}}。
プログラムの構造化の指標は、goto文の有無だけではなく証明のしやすさにも現れる<ref name="new_generation_programming">淵一博, "新世代プログラミング", 共立出版, 1986. </ref>。すなわちプログラムの構造化だけでなく、人間の思考も構造化しなければならない<ref name="new_generation_programming"/><ref name="structured_and_how_to">[http://ci.nii.ac.jp/naid/110002720195 和田英一, "「構造的...」と「いかにして...」", ''情報処理'', Vol.16, No.3, 1975, pp.169, 情報処理学会. ]</ref>。そのためプログラミングには、ある程度の数学的な教育が必要とされる<ref name="from_craft_to_scientific_discipline"/>。しかし形式的な証明は、時として非人間的な長さの記述になることもダイクストラは認めている<ref name="a_discipline_of_programming"/><ref name="from_craft_to_scientific_discipline"/>。同氏は、プログラムの証明が厳密であることにはこだわらないという意見を明らかにした<ref name="a_discipline_of_programming"/>{{#tag:ref|形式化にとらわれない点では（当時のダイクストラの）構造化プログラミングは[[形式手法]]と趣きが異なる。なおプログラムの正当性の証明とはウォークスルーやインスペクションによるレビューではなく、帰納法や最弱事前条件による検証を指す。
形式的でない証明の方法については、ロバートの「プログラムの証明」が入門書の一つである。|group="注釈"}}。
また、プログラムの証明に対する反論も存在する。マイケル・ジャクソンは、個々のプログラムに証明を付けることは現実的に難しいだろうと述べている<ref name="bit1979_software_design">, "ソフトウェア設計哲学", ''bit'', Vol.11, Issue 2, 1979, pp.4-12, 共立出版.</ref>{{#tag:ref|ジャクソンは構造化プログラミング手法の一つであるジャクソン法で有名なコンピュータ・コンサルタント。|group="注釈"}}。
== goto論争 ==
| |||