構造化プログラム定理は、ベーム・ヤコピニ定理とも呼ばれ、[1] [2]プログラミング言語理論の結果である。これは、制御フローグラフ(この文脈では歴史的にフローチャートと呼ばれていた)のクラスは、サブプログラムを3つの特定の方法(制御構造)でのみ組み合わせる場合、任意の計算可能な関数を計算できるというものである。
- 1つのサブプログラムを実行し、次に別のサブプログラムを実行する(シーケンス)
- ブール式の値に応じて 2 つのサブプログラムのうち 1 つを実行する(選択)
- ブール式が真である限りサブプログラムを繰り返し実行する(反復)
ただし、これらの制約、特に単一の終了を意味するループ制約 (この記事の後半で説明) に従う構造化チャートは、元のプログラムがプログラムの場所によって表す情報を追跡するために、ビット形式の追加の変数(元の証明では追加の整数変数に格納) を使用する場合があります。構築は、Böhm のプログラミング言語P′′に基づいています。
この定理は、 goto コマンドを避け、サブルーチン、シーケンス、選択、反復のみを使用するプログラミング パラダイムである構造化プログラミング の基礎を形成します。

起源と変種
この定理は、一般的にはコラード・ベームとジュゼッペ・ヤコピニによる1966年の論文[ 3] : 381 によるものとされている。 [4] デイヴィッド・ハレルは1980年に、ベーム-ヤコピニの論文は「普遍的な人気」を誇っており、 [3] : 381 特に 構造化プログラミングの支持者の間で人気があったと書いている。ハレルはまた、「そのかなり技術的なスタイルのために [1966年のベーム-ヤコピニの論文] は詳細に読まれるよりも引用されることが多いようだ」[3] : 381 とも指摘し、1980年までに発表された多数の論文を検討した後、ハレルは、ベーム-ヤコピニの証明の内容は、本質的にはより単純な結果を含む俗説として誤って伝えられることが多いと主張した。その結果自体は、フォン・ノイマン[5]とクリーネの論文における現代コンピューティング理論の始まりにまで遡ることができる。[3] : 383
ハレルはまた、より一般的な名前が1970年代初頭にHDミルズによって「構造定理」として提案されたと書いている。[3] : 381
単一whileループ、定理のフォークバージョン
このバージョンの定理は、元のプログラムの制御フローのすべてを、元の非構造化プログラム内のすべての可能なラベル (フローチャート ボックス) をプログラム カウンターwhileがシミュレートする単一のグローバル ループに置き換えます。Harel は、このフォーク定理の起源を、コンピューティングの始まりを示す 2 つの論文にまでさかのぼりました。1 つは、1946 年のフォン ノイマン アーキテクチャの説明で、プログラム カウンターがwhile ループの観点からどのように動作するかを説明しています。Harel は、構造化プログラミング定理のフォーク バージョンで使用される単一のループは、基本的にフォン ノイマン コンピューターでのフローチャートの実行に対する操作的意味論を提供しているだけだと指摘しています。 [3] : 383 Harel がフォーク バージョンの定理をたどったもう 1 つの、さらに古いソースは、1936 年のStephen Kleeneの正規形定理です。 [3] : 383
ドナルド・クヌースは、この証明形式は以下のような疑似コードになり、この変換では元のプログラムの構造が完全に失われると指摘して批判した。 [6] : 274 同様に、ブルース・イアン・ミルズはこのアプローチについて「ブロック構造の精神はスタイルであり、言語ではない。フォン・ノイマン・マシンをシミュレートすることで、ブロック構造言語の範囲内であらゆるスパゲッティ・コードの動作を生み出すことができる。これによってスパゲッティであることを妨げるものではない」と書いている。[7]
p := 1 while p > 0 do if p = 1の場合、フローチャートのステップ1を実行します。 p :=結果として得られる後続ステップフローチャートのステップ1の番号(後続ステップがない場合は0 ) end if if p = 2の場合、フローチャートのステップ2を実行します。p : =結果として得られる後続ステップフローチャートのステップ2の番号(後続ステップがない場合は0 ) end if ... if p = nの場合、フローチャートのステップnを実行します。p :=結果として得られる後続ステップフローチャートのステップnの番号(後続ステップがない場合は0 ) end if end while
ベームとヤコピニの証明
ボームとヤコピニの論文の証明は、フローチャートの構造に基づく帰納法によって進められている。 [3] : 381 グラフのパターンマッチングを採用していたため、ボームとヤコピニの証明はプログラム変換アルゴリズムとしては実用的ではなく、この方向へのさらなる研究への扉が開かれた。[8]
リバーシブルバージョン
可逆構造化プログラム定理[9] は、可逆コンピューティングの分野における重要な概念です。可逆プログラムで実行可能な計算はすべて、シーケンス、選択、反復などの制御フロー構造の構造化された組み合わせのみを使用した可逆プログラムでも実行できると仮定しています。従来の不可逆プログラムで実行可能な計算はすべて可逆プログラムでも実行できますが、各ステップが可逆で、何らかの追加出力が必要であるという制約が追加されます。[10] さらに、可逆な非構造化プログラムは、追加出力なしで 1 回の反復のみで構造化された可逆プログラムでも実行できます。この定理は、構造化プログラミングフレームワーク内で可逆アルゴリズムを構築するための基本原理を示しています。
構造化プログラム定理については、ローカル[11]とグローバル[12]の両方の証明方法が知られています。しかし、その可逆バージョンについては、グローバルな証明方法は認識されているものの、Böhm と Jacopini [11]が行ったようなローカルなアプローチはまだ知られていません。この違いは、従来のコンピューティングパラダイムと比較して、可逆コンピューティングの基礎を確立する際の課題と微妙な違いを強調する例です。
意味と改良点
ベーム・ヤコピニの証明は、ソフトウェア開発に構造化プログラミングを採用するかどうかという問題を解決しなかった。その理由の1つは、構造化プログラミングはプログラムを改善するよりも、むしろプログラムをわかりにくくする可能性が高いからである。それどころか、それは議論の始まりを告げた。エドガー・ダイクストラの有名な手紙「Go To 文は有害であると考えられる」は1968年に続いた。[13]
一部の学者は、ボーム=ヤコピニの結果に対して純粋主義的なアプローチを取り、ループの途中からbreakのやreturnのような命令でさえボーム=ヤコピニの証明には必要ないので悪い習慣であると主張し、すべてのループには単一の終了点があるべきだと主張した。この純粋主義的なアプローチは、 1968年から1969年に設計されたPascalプログラミング言語に具体化されており、1990年代半ばまで、学術界の入門プログラミングクラスで好んで使用されていた。[14]
エドワード・ユアドンは、1970年代には、最初から構造化プログラミングのやり方で考える必要があるという議論に基づいて、非構造化プログラムを自動化された手段で構造化プログラムに変換することに対して哲学的な反対意見さえあったと指摘している。実用的な反論は、そのような変換は既存のプログラムの多くに利益をもたらすというものだった。[15]自動化された変換の最初の提案の1つは、1971年のエドワード・アシュクロフトとゾハル・マンナによる論文であった。[16]
ベーム・ヤコピニの定理を直接適用すると、構造化チャートに追加のローカル変数が導入される可能性があり、コードの重複も発生する可能性があります。[17]後者の問題は、この文脈ではループ半問題と呼ばれています。[18] Pascal はこれらの問題の両方の影響を受けており、Eric S. Robertsが引用した実証研究によると、学生プログラマーは、配列内の要素を検索する関数の作成など、いくつかの簡単な問題に対して Pascal で正しい解答を定式化するのに苦労していました。Roberts が引用した Henry Shapiro による 1980 年の研究では、Pascal が提供する制御構造のみを使用した場合、正しい解答を与えたのは被験者の 20% のみでしたが、ループの途中から return を記述できる場合は、この問題に対して間違ったコードを記述した被験者はいませんでした。[14]
1973 年、S. ラオ コサラジュは、任意の深さのループからのマルチレベルブレークが許される限り、構造化プログラミングで追加の変数を追加せずに済むことを証明しました。[1] [19]さらに、コサラジュは、今日ではコサラジュ階層と呼ばれる厳密なプログラムの階層が存在することを証明しました。これは、すべての整数nに対して、深さnのマルチレベルブレークを含むプログラムが存在し、それを (追加の変数を導入せずに) n未満の深さのマルチレベルブレークを含むプログラムとして書き直すことができないというものです。[1]コサラジュは、マルチレベルブレーク構造をBLISSプログラミング言語に引用しています。キーワード形式のマルチレベルブレークは、実際にはその言語の BLISS-11 バージョンで導入されました。元の BLISS にはシングルレベルブレークしかありませんでした。BLISS ファミリーの言語は、無制限の goto を提供しませんでした。Javaプログラミング言語も後にこのアプローチを採用しました。[20] : 960–965 leave label
Kosaraju の論文から得られるより単純な結果は、プログラムが (変数を追加せずに) 構造化プログラムに還元可能であるのは、2 つの異なる出口を持つループを含まない場合のみであるということです。還元可能性は、Kosaraju によって、大まかに言えば、元のプログラムと同じ関数を計算し、同じ「基本アクション」と述語を使用するが、異なる制御フロー構造を使用する可能性があると定義されました。(これは、Böhm-Jacopini が使用した還元可能性よりも狭い概念です。) この結果に触発されて、Thomas J. McCabe は、サイクロマティック複雑度の概念を導入した引用数の多い論文のセクション VI で、非構造化プログラムの制御フロー グラフ(CFG)に対するKuratowski の定理の類似物、つまり、プログラムの CFG を非構造化にする最小のサブグラフについて説明しました。これらのサブグラフは、自然言語で非常によく説明できます。次のとおりです。
- ループからの分岐(ループサイクルテスト以外)
- ループに分岐する
- 決定への分岐(つまり、if「分岐」)
- 決定から分岐する
マッケイブは、実際にこれら 4 つのグラフがサブグラフとして現れるときには独立していないことを発見しました。つまり、プログラムが非構造化であるための必要十分条件は、その CFG がサブグラフとしてこれら 4 つのグラフのうち 3 つのサブセットのいずれか 1 つを持つことであるということです。また、非構造化プログラムがこれら 4 つのサブグラフのいずれかを含む場合、4 つのセットから別のサブグラフを必ず含まなければならないことも発見しました。この後者の結果は、非構造化プログラムの制御フローが一般に「スパゲッティ コード」と呼ばれるものに絡み合う仕組みを説明するのに役立ちます。マッケイブはまた、任意のプログラムが与えられたときに、それが構造化プログラムの理想からどれだけ離れているかを定量化する数値尺度を考案しました。マッケイブは、この尺度を「本質的複雑性」と呼びました。[21]
構造化プログラミングにおける禁制グラフのマッケイブによる特徴づけは、少なくともダイクストラのD構造を構成要素とみなす場合には不完全であると考えられる。[22] : 274–275 [明確化が必要]
1990 年までに、既存のプログラムから goto を排除し、その構造の大部分を維持する方法が数多く提案されました。この問題に対するさまざまなアプローチでは、上記のフォーク定理のような出力を回避するために、単純なチューリング同値よりも厳密な同値の概念もいくつか提案されました。選択された同値の概念の厳密さによって、必要な制御フロー構造の最小セットが決まります。1988 年のJACM論文では、Lyle Ramshaw がそれまでの分野を調査し、独自の方法を提案しています。[23] Ramshaw のアルゴリズムは、たとえば一部の Javaデコンパイラで使用されました。これは、 Java 仮想マシンコードには、ターゲットがオフセットとして表現される分岐命令があるのに対し、高水準 Java 言語には多段階のbreakandcontinue文しかないためです。[24] [25] [26] Ammarguellat (1992) は、シングル エグジットの強制に立ち返る変換方法を提案しました。[8]
Cobolへの応用
1980 年代、IBM の研究者であるHarlan Mills 氏は、 COBOLコードに構造化アルゴリズムを適用する COBOL Structuring Facility の開発を監督しました。Mills 氏の変換には、各手順で次の手順が含まれていました。
- 手順内の基本的なブロックを識別します。
- 各ブロックのエントリ パスに一意のラベルを割り当て、各ブロックの終了パスに、それらが接続するエントリ パスのラベルを付けます。プロシージャからの戻りには 0 を使用し、プロシージャのエントリ パスには 1 を使用します。
- 手順を基本ブロックに分割します。
- 1 つの出口パスのみの宛先である各ブロックについては、そのブロックをその出口パスに再接続します。
- プロシージャ内で新しい変数を宣言します (参照用に L と呼びます)。
- 残りの接続されていない各出口パスに、そのパスのラベル値を L に設定するステートメントを追加します。
- 結果のプログラムを、Lで示されるエントリパスラベルを持つプログラムを実行する選択ステートメントに結合します。
- L が 0 でない限り、この選択ステートメントを実行するループを構築します。
- L を 1 に初期化し、ループを実行するシーケンスを構築します。
この構造は、選択ステートメントのいくつかのケースをサブプロシージャに変換することによって改善できます。
参照
参考文献
- ^ abc Dexter Kozenおよび Wei-Lung Dustin Tseng (2008)。「プログラム構築の数学 - ボーム-ヤコピニの定理は命題的に偽である」( PDF) 。MPC 2008。コンピュータサイエンスの講義ノート。5133 : 177–192。CiteSeerX 10.1.1.218.9241。doi : 10.1007 / 978-3-540-70594-9_11。ISBN 978-3-540-70593-2。
- ^ 「CSE 111、2004年秋、BOEHM-JACOPINI THEOREM」。Cse.buffalo.edu。2004年11月22日。 2013年8月24日閲覧。
- ^ abcdefgh Harel, David (1980). 「フォーク定理について」(PDF) . Communications of the ACM . 23 (7): 379–389. doi :10.1145/358886.358892. S2CID 16300625.
- ^ Bohm, Corrado; Giuseppe Jacopini (1966 年 5 月). 「フロー図、チューリングマシン、および 2 つの形成規則のみを持つ言語」. Communications of the ACM . 9 (5): 366–371. CiteSeerX 10.1.1.119.9119 . doi :10.1145/355592.365646. S2CID 10236439.
- ^ Burks, Arthur W. ; Goldstine, Herman ; von Neumann, John (1947)、「電子計算機の論理設計に関する予備的考察」、プリンストン、ニュージャージー州:高等研究所
- ^ Donald Knuth (1974). 「go to ステートメントによる構造化プログラミング」. Computing Surveys . 6 (4): 261–301. CiteSeerX 10.1.1.103.6084 . doi :10.1145/356635.356640. S2CID 207630080.
- ^ ブルース・イアン・ミルズ (2005).プログラミング理論入門. シュプリンガー. p. 279. ISBN 978-1-84628-263-8。
- ^ ab Ammarguellat, Z. (1992). 「制御フロー正規化アルゴリズムとその複雑さ」. IEEE Transactions on Software Engineering . 18 (3): 237–251. doi :10.1109/32.126773.
- ^横山哲夫、ホルガー・ボック・アクセルセン、ロバート・グリュック(2016 年1月)。「可逆フローチャート言語の基礎」理論計算機科学。611 :87–115。doi :10.1016/ j.tcs.2015.07.046。
- ^ Bennett, CH (1973 年 11 月). 「計算の論理的可逆性」. IBM Journal of Research and Development . 17 (6): 525–532. doi :10.1147/rd.176.0525.
- ^ ab Böhm, Corrado; Jacopini, Giuseppe (1966 年 5 月). 「フロー図、チューリングマシン、および 2 つの形成規則のみを持つ言語」. Communications of the ACM . 9 (5): 366–371. doi :10.1145/355592.365646.
- ^ Cooper, David C. (1967 年 8 月). 「Böhm と Jacopini のフローチャートの簡約」. Communications of the ACM . 10 (8): 463. doi :10.1145/363534.363539.
- ^ Dijkstra, Edsger (1968). 「Go To ステートメントは有害であると考えられる」Communications of the ACM . 11 (3): 147–148. doi : 10.1145/362929.362947 . S2CID 17469809.
- ^ ab Roberts, E. [1995]「ループ終了と構造化プログラミング:議論の再開」、ACM SIGCSE 速報、(27)1: 268–272。
- ^ EN Yourdon (1979). Classics in Software Engineering . Yourdon Press. pp. 49–50. ISBN 978-0-917072-14-7。
- ^ Ashcroft, Edward; Zohar Manna (1971)。「go to プログラムから 'while' プログラムへの変換」。IFIP会議の議事録。この論文は、配布が限られているため、オリジナルの会議議事録で入手することは困難ですが、ユアドンの1979年の本の51-65ページに再掲載されました。
- ^ David Anthony Watt、William Findlay (2004)。プログラミング言語設計コンセプト。John Wiley & Sons。p. 228。ISBN 978-0-470-85320-7。
- ^ Kenneth C. Louden、Kenneth A. Lambert (2011)。プログラミング言語:原則と実践(第3版)。Cengage Learning。pp. 422–423。ISBN 978-1-111-52941-3。
- ^ KOSARAJU, S. RAO. 「構造化プログラムの分析」、Proc. Fifth Annual ACM Syrup. Theory of Computing、(1973 年 5 月)、240-252。また、Kosaraju , S. Rao (1974) 「構造化プログラムの分析」。Journal of Computer and System Sciences。9 ( 3): 232–255。doi :10.1016/S0022-0000(74)80043-7。Donald Knuth (1974)による引用。「go to文による構造化プログラミング」。コンピューティング調査。6 (4): 261–301。CiteSeerX 10.1.1.103.6084。doi : 10.1145 /356635.356640。S2CID 207630080 。
- ^ Brender, Ronald F. (2002). 「BLISSプログラミング言語:歴史」(PDF) .ソフトウェア:実践と経験. 32(10):955–981. doi:10.1002/spe.470. S2CID 45466625.
- ^ オリジナルの論文はThomas J. McCabe (1976 年 12 月) です。「複雑性の尺度」IEEE Transactions on Software Engineering SE -2 (4): 315–318. doi :10.1109/tse.1976.233837. S2CID 9116234.二次的な解説については、Paul C. Jorgensen (2002) の「ソフトウェアテスト: 職人のアプローチ、第 2 版 (第 2 版)」を参照してください。CRC Press。pp. 150–153。ISBN 978-0-8493-0809-3。
- ^ Williams, MH (1983). 「フローチャートスキーマと命名法の問題」.コンピュータジャーナル. 26 (3): 270–276. doi : 10.1093/comjnl/26.3.270 .
- ^ Ramshaw, L. (1988). 「プログラム構造を維持しながら go to をなくす」Journal of the ACM . 35 (4): 893–920. doi : 10.1145/48014.48021 . S2CID 31001665.
- ^ Godfrey Nolan (2004). Decompiling Java . Apress. p. 142. ISBN 978-1-4302-0739-9。
- ^ 「Krakatoa: Java での逆コンパイル」(PDF) . www.usenix.org .
- ^ 「Java バイトコード用の効果的な逆コンパイル アルゴリズム」(PDF) . www.openjit.org .
さらに読む
上記でまだ取り上げられていない資料:
- DeMillo, Richard A. (1980). 「構造化プログラミングにおける空間と時間のトレードオフ: 改良された組み合わせ埋め込み定理」. Journal of the ACM . 27 (1): 123–127. doi : 10.1145/322169.322180 . S2CID 15669719.
- Devienne, Philippe ( 1994)。「バイナリホーン節は 1 つで十分」。Stacs 94 。コンピュータサイエンスの講義ノート。第 775 巻。pp. 19–32。CiteSeerX 10.1.1.14.537。doi : 10.1007 / 3-540-57785-8_128。ISBN 978-3-540-57785-0。
