1969年の論文「構造化プログラミング」
出典: フリー百科事典『ウィキペディア(Wikipedia)』 (2022/04/25 06:17 UTC 版)
「構造化プログラミング」の記事における「1969年の論文「構造化プログラミング」」の解説
1969年度NATOソフトウェア工学会議に寄稿されたこの「Structured Programming」は、プログラム正当性の効率的な検証技術に重点を置き、当時問題視されていたコードサイズの際限なき肥大化によるソフトウェア危機の解決策として従来のボトムアップ設計からトップダウン設計への移行を推奨していた。 論文の前半では、プログラムサイズの肥大化に伴い、各プログラム部品およびそれらを組み合わせた際のプログラムの正当性(program correctness)の立証(demonstration)に必要な労力が指数的に増加して完遂が不可能になるというソフトウェア危機の問題について述べている。ダイクストラはプログラムの正しさに対して証明を与える従来の研究を分析して、証明の手続きを考えずに書かれたプログラムは証明に必要な労力がプログラムのサイズに対して爆発するとし、「与えられたプログラムに対してどうやって証明をするか」ではなく「証明がしやすいプログラムの構造とは何か」についてフォーカスするとした。 後半ではそのための方法について説明している。まず推論しやすい構造として、ステートメントが順に並んだだけのものを挙げている。また、if文1つだけも推論しやすいとしている。しかし、if文がN個並んだ場合、そのままでは2のN乗ステップの推論が必要であるとしている。そこでif文を抽象ステートメントで1つずつ置き換える段階的抽象化(step-wise abstraction)により、Nに比例する推論で正しさを示せるとした。また、そのためには制御のジャンプを制限し、制御構造は順次の他に、選択、反復、および手続き呼び出しに限るべきとしている(なお、順次、選択、反復のいわゆる制御構造(control structures)に触れているのはこの文節だけである)。この例のように詳細なプログラムを抽象化(abstraction)していくのではなく、逆に抽象的なプログラムから始めて詳細化(refinement)していくというやり方を示している。 詳細化の際には共同詳細化(joint-refinement)という考え方が示されている。これは抽象データ構造の詳細化と共にそれを扱う抽象ステートメントを同時に詳細化し、それを1つのプログラムテキストのユニットに分離するというものである。このユニットをダイクストラは真珠(pearl)と呼んだ。また、抽象的な真珠が1段階具体的な真珠に依存し、その真珠がさらに具体的な真珠に依存していったものをネックレスに例えた。そしてネックレスの上部は下部に関わらず正しさを証明することができ、また下部を取り替えることでプログラムのバリエーションを労力をかけずに作れるとした。
※この「1969年の論文「構造化プログラミング」」の解説は、「構造化プログラミング」の解説の一部です。
「1969年の論文「構造化プログラミング」」を含む「構造化プログラミング」の記事については、「構造化プログラミング」の概要を参照ください。
- 1969年の論文「構造化プログラミング」のページへのリンク