「構造化プログラミング」の版間の差分

削除された内容 追加された内容
m 節構造の変更
検証手法についてとりあえず記載した。
2行目:
'''構造化プログラミング'''(こうぞうかプログラミング、{{lang-en-short|structured programming}})とは、1960年代後半に[[エドガー・ダイクストラ]]らによって提唱された仮想機械モデルに基づく段階的詳細化法を用いたプログラミングのことを言う。
 
歴史的経緯から、構造化プログラミングはIBMの{{仮リンク|[[ハーラン・ミルズ|en|Harlan Mills|de|Harlan]](Harlan Mills|label=Mills}}Mills)の提案に由来するgoto-lessプログラミングとして一部分を切り取られた形で広く知られている<ref name="goto_nested_loop">{{cite journal|和書|naid=110002712129 |last=金藤|first=栄孝 |last2=二木|first2=厚吉 |title=多重ループからの脱出でのgoto文の是非:Hoare理論の観点から |journal=情報処理学会論文誌 |volume45 |issue= 3 |year=2004 |page=770-784 }}</ref><ref name="goto_finite_state_machines">{{cite journal|和書|naid=110002712260 |last=金藤|first=栄孝 |last2=二木|first2=厚吉 |title=有限状態機械に基づくプログラミングでのgoto文使用の是非 : Hoare論理の観点から |journal=情報処理学会論文誌 |volume= 45 |issue= 9, 2004 |pages=2124-2137}}</ref><ref name="box_structured">H.D.Mills, R.C.Linger, a.R.Hevner, “ボックス構造化情報システム”, ''ソフトウェアエンジニアリング論文集80's'', Tom DeMarco, Timothy Lister編著, 児玉公信 監訳, 翔泳社, 2006, pp.187-219. </ref>。
 
== 概要 ==
構造化プログラミングではプログラミング言語が持つ[[ステートメント]]を直接使ってプログラムを記述するのではなく、機能を抽象化した仮想機械を想定し、その仮想機械が提供する命令群でプログラムを記述する。普通、抽象化は1段階ではなく階層的である。各階層での実装の詳細は他の階層と隔離されており、実装の変更の影響はその階層内のみに留まる(<ref name="structured_programming"/> Abstract data structures)。各階層はアプリケーションに近い抽象的な方から土台に向かって順序付けられている。この順序は各階層を設計した時間的な順番とは必ずしも一致しない(<ref name="structured_programming"/> Concluding remarks)。
 
== ダイクストラによるプログラムの正当性しさの検証手法 ==
計算機(computer)は与えたプログラムに応じてそれを計算し結果を出力するという装置であるが、プログラムに誤りがあると、当初の意図した命題(仕様)を肯定しないものとなる<ref>たとえば、一律に個々の構成要素が正しい確率を p とすると、N 個の構成要素からなるプログラム全体が正しい確率 P は、安直に計算すれば、
1960年代後半、科学の領域にプログラミング方法論が現れると、初期の計算機でもてはやされたプログラムの効率を良くする技巧<ref name="bit1975_microcomputer">E.W.ダイクストラ, "マイクロコンピュータのインパクト", 川合慧 訳, ''bit'', Vol.7, Issue 6, 1975, pp.4-6, 共立出版. </ref>だけでなく、品質やプログラムの正しさという問題にも関心が集まった<ref name="from_craft_to_scientific_discipline"/>。
: P = p<sup>N</sup>
となり、 N が大きいプログラム(大規模なソフトウェア)においては、誤りの混入により命題(仕様)を肯定しない可能性は飛躍的に高まることがわかる。</ref>。
 
プログラマは、正しいプログラムを作り出すばかりでなく、納得のいくやり方で正しさを証明することも仕事の一つであるという立場を取っていた<ref>[[#構造化プログラミング(1975) |構造化プログラミング(1975)]] p.6</ref>[[ダイクストラ]]は、プログラムの正しさの納得のいく証明を遂行するための手法を導入した<ref>これは計算機や大規模プログラムを一種のブラックボックス化された機械装置とみなしてテストによって正しさを確認する手法ではない。ダイクストラは、テストはプログラムに対する疑いを全て取り除くには不十分であることを主張していた。[[#構造化プログラミング(1975)|構造化プログラミング(1975)]] p.5 <br />
プログラムが正しいことを確認するには、それを証明しなければならない<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>。所与のプログラムの正しさを後付けで証明することは、はじめから証明を意識して作られたプログラムの場合より難しいことが経験的に知られている
これについてダイクストラは「テストはバグの存在を示すには有効だが、バグが存在しないことは証明できない」という表現を好んで用いた、といわれる。
* E.W.ダイクストラ, “謙虚なプログラマ”, ''ACMチューリング賞講演集'', 木村泉 訳, 共立出版, 1989, pp.23-43.
* [http://www.cs.utexas.edu/users/EWD/transcriptions/EWD02xx/EWD273.html E.W.Dijkstra, "The Programming Task Considered as an Intellectual Challenge", 1969. ]
* [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. ]
* [http://www.cs.utexas.edu/users/EWD/transcriptions/EWD03xx/EWD361.html E.W.Dijkstra, "Programming as a discipline of mathematical nature", 1973. ]
</ref>。ただし、その検証<ref>D.グリースはプログラムの正しさの証明を、抽象的なレベルでは正当性証明、具体的なレベルではプログラムの検証と言葉を使い分けているが、ここでは厳密な区別はしない。
* 金山裕 編, "構造的プログラミング −批判と支持−", ''bit'', Vol.7, Issue 7, 1975, pp.6-13, 共立出版.</ref>を実行するためには対象となるプログラムは「うまく構造化」されていなくてはならず、その「うまく構造化」されたプログラムを開発する手法が'''構造化プログラミング'''である<ref>すなわち、プログラム検証と構造化プログラミングとは不可分の関係にある。</ref>。
 
その手法とは、文の解釈過程そのものであり<ref>ダイクストラ自身は「数学の証明」になぞらえたが、これは技巧的な点が強調される傾向が強くなるため適切ではない。</ref>、文(プログラム)を文節分けし、文法の妥当性、個々の単語(名詞、動詞)の妥当性確認を再帰的に繰り返していくというものである<ref>自然言語の文の場合、労力の観点から厳密に用語の正統性を確認することはまれであるが、プログラムの場合、一回一回全部原始的な概念にまで立ち戻るという行為を行うというところが大きな違いである。</ref>。
 
=== プログラムの正しさに関する様々な意見 ===
構造化プログラミングの支持者らは、プログラムの正しさの重要性と証明の方法や表明(assertion)の使い方について熱心に説いた<ref name="the_science_of_programming"/><ref name="structured_programming_72"/><ref name="how_to_solve_it_by_computer">R.Geoff Dromey, ''How to Solve it by Computer'', Prentice Hall, 1982. </ref><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="注釈"}}。
24 ⟶ 38行目:
=== 三つの構造化文 ===
 
ダイクストラは“Go To Statement Considered Harmful”<ref name="go_to_statement_considered_harmful"/>および“Structured Programming”<ref name="structured_programming"/>において、好ましい構造として手続き呼び出しの他に、順次・反復・分岐の3つを挙げた。ヴィルトはこれらを構造化文(structured statement)と呼んだ <ref name="systematic_programming">N.ヴィルト, ''系統的プログラミング/入門'', 野下浩平, 筧捷彦, 武市正人 訳, 近代科学社, 1978. </ref>。goto文を避けて構造化文を用いるようプログラマーに教えることが、構造化プログラミングの伝統的な知恵である<ref name="sp_in_introductory_programming_courses">C.A.R.Hoare, "Structured programming in introductory programming courses", ''Structured Programming'', Infotech state of the art report, 1976, pp.257-263, Infotech International. </ref>。
 
;順次
64 ⟶ 78行目:
 
== 参考文献 ==
* {{Citation |和書| title=構造化プログラミング | author=E.W.ダイクストラ | author2=C.A.R.ホーア | author3=O.-J.ダール | translator=野下浩平 | year=1975 | publisher=サイエンス社 | ref=構造化プログラミング(1975) }}
{{refbegin|2}}
* {{Cite book |和書| title=ソフトウェア工学実践の基礎 -分析・設計・プログラミング | author=落水 浩一郎}}
* {{Cite book |和書| title=ずっと受けたかったソフトウェア設計の授業 | author=飯泉 純子, 大槻 繁}}
* {{citation | author=D.L.Parnas | year=1975 | title=Use of the concept of transparency in the design of hierarchically structured systems | url=http://ivizlab.sfu.ca/arya/Papers/SW/TranspDesignHierSys.pdf }}
* {{citation | author=D.L.Parnas | year=1971 | title=Information Distribution Aspects of Design Methodology | url=http://cseweb.ucsd.edu/~wgg/CSE218/Parnas-IFIP71-information-distribution.PDF }}
77 ⟶ 90行目:
* {{Citation |和書| title=プログラミング原論 ― いかにしてプログラムをつくるか | author=E.W.ダイクストラ | translator=浦昭治 | year=1983 | publisher=サイエンス社}}
* {{Citation |和書| title=プログラミングの方法 | author=E.W.ダイクストラ | author2=W.H.J.フェイエン | translator=玉井浩 | year=1991 | publisher=サイエンス社}}
* {{Citation |和書| title=構造化プログラミング | author=E.W.ダイクストラ | author2=C.A.R.ホーア | author3=O.-J.ダール | translator=野下浩平 | year=1975 | publisher=サイエンス社}}
{{refend}}
== 関連項目 ==
* [[Simula]]
* [[抽象データ型]]
* 抽象化 (計算機科学)
* [[ジャクソン流構造化プログラミング]]
* プログラム検証