「構造化プログラミング」の版間の差分
削除された内容 追加された内容
編集の要約なし |
編集の要約なし |
||
14行目:
#'''選択'''（''selection''） 条件式が導出した状態に従い、次に実行する部分プログラムを選択して分岐する。
#'''反復'''（''repetition''）条件式が導出した特定の状態の間、部分プログラムを繰り返し実行する。
[[ファイル:Structured_program_patterns.png|中央|サムネイル|700x700ピクセル|順次、選択、反復の描写図（青はNSダイアグラム、緑はフローチャート）]]
== 構造化設計 ==
79 ⟶ 77行目:
なお、ベームとヤコピーニの証明は、フローチャートやそれによって表現されるプログラム・関数・チューリングマシンなどの理論的側面に注目している。これは任意の論理回路が[[否定論理積|NAND]]素子の組み合わせによって表現できるとか、[[ラムダ計算|λ式]]がSおよびKという名の2つの[[SKIコンビネータ計算|コンビネータ]]によって表現できるとかいった研究に近い。回路設計者が直接NANDを組み合わせて電子回路を設計しないのと同じように、構造化定理は良いプログラムの作成を（少なくとも直接的には）意図していない。ハレルも構造化定理は実際の内容以上に引用されて民間伝承定理（''folk theorem''）化していると指摘していた<ref name=":0" />。
=== プログラム正当性検証のための構造化 ===
ダイクストラは、プログラマは正しいプログラムを作り出すばかりでなく納得のいくやり方で正しさを証明（検証）することも仕事の一つであるという立場を取っていた<ref>[[構造化プログラミング#構造化プログラミング(1975)|構造化プログラミング(1975)]] p.6</ref>。ただしその検証<ref>D.グリースはプログラムの正しさの証明を、抽象的なレベルでは正当性証明、具体的なレベルではプログラムの検証と言葉を使い分けているが、ここでは厳密な区別はしない。
* 金山裕 編, "構造的プログラミング −批判と支持−", ''bit'', Vol.7, Issue 7, 1975, pp.6-13, 共立出版.</ref>をするためのプログラムはよく構造化（''well-structured''）されていなくてはならず、そのために提唱された技法が構造化プログラミングであった{{#tag:ref|すなわち、プログラム検証と構造化プログラミングとは不可分の関係にある。|group="注釈"}}<ref>所与のプログラムの正しさを後付けで証明することは、はじめから証明を意識して作られたプログラムの場合より難しいことが経験的に知られている、と言われる。
* E.W.Dijkstra, "Programming methodologies, their objectives and their nature", ''Structured Programming'', Infotech state of the art report, 1976, pp.205-212, Infotech International.</ref>。1967年のノート「Towards Correct Programs」でダイクストラはよく構造化するための三つのメンタルツール（''mental tool''）をこのように提示している。
# 列挙（enumeration）： 一人の人間の能力でできる範囲でプログラムの命令の妥当性を一つ一つ確認していく作業
# 数学的帰納（mathematical induction）： while文など計算機特有の多数の繰り返し文についてのみ数学的帰納法を用いて確認する作業
# 抽象（abstraction）： プログラムのブロックなどに名前をつけ、さらに中身を見ないで正しいと仮定することで検証作業を後回しにする操作
プログラムが正しいことを確認するには、それを証明しなければならない<ref name="structured_programming" />{{#tag:ref|D.グリースはプログラムの正しさの証明を、抽象的なレベルでは正当性証明、具体的なレベルではプログラムの検証と言葉を使い分けているが<ref name="bit1975_structured_programming">金山裕 編, "構造的プログラミング −批判と支持−", ''bit'', Vol.7, Issue 7, 1975, pp.6-13, 共立出版.</ref>、ここでは厳密な区別はしない。|group="注釈"}}。テストはプログラムに対する疑いを全て取り除くには不十分であるという意見が上がった<ref name="systematic_programming">N.ヴィルト, ''系統的プログラミング/入門'', 野下浩平, 筧捷彦, 武市正人 訳, 近代科学社, 1978. </ref><ref name="how_to_solve_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>。構造化プログラミングの支持者らは、プログラムの正しさの重要性と証明の方法や表明(assertion)の使い方について熱心に説いた<ref name="the_science_of_programming" /><ref name="structured_programming_72" /><ref name="systematic_programming" /><ref name="how_to_solve_it_by_computer" /><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="proving_programs_correct">ロバート B.アンダーソン, ''演習プログラムの証明'', 有沢誠 訳, 近代科学社, 1980. </ref><ref name="basic_theorem_of_programs">小野寛晰, ''プログラムの基礎理論'', サイエンス社, 1975. </ref>。所与のプログラムの正しさを後付けで証明することは、はじめから証明を意識して作られたプログラムの場合より難しいことが経験的に知られている<ref name="programming_methodologies">E.W.Dijkstra, "Programming methodologies, their objectives and their nature", ''Structured Programming'', Infotech state of the art report, 1976, pp.205-212, Infotech International.</ref>。ダイクストラは、プログラミングと同時にプログラムの証明を（わずかに証明を先行して）進めることを推奨している<ref name="a_discipline_of_programming">E.W.ダイクストラ, ''プログラミング原論 ― いかにしてプログラムをつくるか'', 浦昭治訳, サイエンス社, 1983. </ref>。そのようなアプローチでプログラムの正当性の問題にあたれば、複雑な問題であっても知的管理が可能であると述べた{{#tag:ref|ダイクストラはプログラミングと証明を並行するのに適した、最弱事前条件をによる検証方法を考案した。ホーア論理は作り終わったものは証明できるが、これから作るプログラムについては指標を与えてくれない<ref name="software_cleanroom">二木厚吉 監修, ''ソフトウェアクリーンルーム手法'', 日科技連, 1997. </ref>。|group="注釈"}}。しかし形式的な証明は、時として非人間的な長さの記述になることもダイクストラは認めている<ref name="a_discipline_of_programming" /><ref name="from_craft_to_scientific_discipline" />。同氏は、プログラムの証明が形式的であることにはこだわらないという意見を明らかにした<ref name="a_discipline_of_programming" /><ref name="structured_programming_with_go_to_statements" />{{#tag:ref|形式化にとらわれない点では（当時のダイクストラの）構造化プログラミングは[[形式手法]]と趣きが異なる。なおプログラムの正しさの証明とはウォークスルーやインスペクションによるレビューではなく、帰納法や最弱事前条件による検証を指す。
形式的でない証明の方法については、ロバートの「プログラムの証明」<ref name="proving_programs_correct"/>が良い入門書の一つである。|group="注釈"}}。
=== ダイクストラの後述 ===
| |||