構造化定理

Structured_program_theorem
構造化プログラムの定理とも呼ばれる、ベームJacopini定理、 における結果である言語理論をプログラム。制御フローグラフのクラス（このコンテキストでは歴史的にフローチャートと呼ばれていました）は、3つの特定の方法（制御構造）でのみサブプログラムを組み合わせた場合、計算可能な関数を計算できると述べています。これらは
1つのサブプログラムを実行し、次に別のサブプログラムを実行する（シーケンス）
ブール式の値に従って2つのサブプログラムの1つを実行する（選択）
ブール式が真である限り、サブプログラムを繰り返し実行します（反復）
NS図（青）とフローチャート（緑）を使用した、構造化プログラム定理の3つの基本パターン（シーケンス、選択、繰り返し）の
グラフィック表現 ただし、これらの制約の対象となる構造化チャートでは、元のプログラムがプログラムの場所によって表す情報を追跡するために、ビット形式の追加の変数（元のプルーフの追加の整数変数に格納されている）を使用できます。構築はベームのプログラミング言語P ”に基づいていました。
この定理は、構造化プログラミングの基礎を形成します。これは、gotoコマンドを避け、サブルーチン、シーケンス、選択、および反復を排他的に使用するプログラミングパラダイムです。

コンテンツ
1 起源と変種
1.1 ループ中のシングル、フォークバージョンの定理 1.2 ベームとジャコピーニの証明
2 含意と改良
3 COBOLへの適用
4 も参照してください
5 参考文献
6 参考文献

起源と変種
この定理は通常、コラド・ベームとジュゼッペ・ジャコピーニによる1966年の論文に381 とクレジットされています。デビッド・ハレルは1980年に、ベーム・ジャコピーニの論文が「普遍的な人気」を享受したと書いています ：381 特に構造化プログラミングの支持者。ハレルはまた、「そのかなり技術的なスタイルのために[1966年のベーム-ジャコピーニの論文]は、詳細に読むよりも明らかに引用されることが多い」と述べた ：381 、そして1980年までに出版された多数の論文を検討した後、ハレルは主張したベーム・ジャコピーニの証明の内容は、通常、より単純な結果を本質的に含むフォーク定理として誤って伝えられていました。その結果自体は、フォンノイマンとクリーンの論文における現代の計算理論の始まりにまでさかのぼることができます。 ：383 
ハレルはまた、より一般的な名前が1970年代初頭に「構造定理」としてHDミルズによって提案されたと書いています。 ：381 

ループ中のシングル、フォークバージョンの定理
このバージョンの定理は、元のプログラムのすべての制御フローを、元の非構造化プログラムで可能なすべてのラベル（フローチャートボックス）を通過whileするプログラムカウンターをシミュレートする単一のグローバルループに置き換えます。ハレルは、このフォーク定理の起源を、コンピューティングの始まりを示す2つの論文にまでさかのぼりました。1つは、1946年のフォンノイマンアーキテクチャの説明です。これは、プログラムカウンターがwhileループの観点からどのように動作するかを説明しています。Harelは、構造化プログラミング定理のフォークバージョンで使用される単一ループは、基本的に、フォンノイマンコンピューターでフローチャートを実行するための操作的意味論を提供するだけであると述べています。 ：383 ハレルがフォークバージョンの定理をたどったもう1つのさらに古い情報源は、1936年のスティーブンコールンの通常の形式の定理です。 ：383 
ドナルド・クヌースは、元のプログラムの構造がこの変換で完全に失われることを指摘することにより、この形式の証明を批判しました。これにより、以下のような擬似コードが生成されます。 ：274 同様に、ブルース・イアン・ミルズはこのアプローチについて次のように書いています。「ブロック構造の精神は言語ではなくスタイルです。フォンノイマン型マシンをシミュレートすることで、スパゲッティコードの動作をブロック構造化言語。これは、スパゲッティになることを妨げるものではありません。」
P ：= 1ながら P > 0で 行う 場合は 、pは = 1が 次に
実行 ステップ 1 からの フローチャートP ：=得られた後続のステップ数のステップ1からのフローチャート（0ならない後継）エンド場合場合、pは= 2が次に実行ステップ2からフローチャートP ：=得られた後続のステップ番号のステップ2からのフローチャート（0あればなし後継）エンド場合…もしP = N 、次に行うステップをn個のフローチャートP ：=得られた後続のステップ数のステップNからフローチャート（後継者がいない場合は0 ）end if end while

ベームとジャコピーニの証明
あなたはそれに追加することによって助けることができます
BöhmとJacopiniの論文の証明は、フローチャートの構造に関する帰納法によって進められています。 ：381 グラフでパターンマッチングを採用しているため、ベームとジャコピーニの証明はプログラム変換アルゴリズムとして実際には実用的ではなく、この方向での追加研究への扉を開きました。

含意と改良
Böhm–Jacopiniの証明は、ソフトウェア開発に構造化プログラミングを採用するかどうかの問題を解決しませんでした。これは、構造がプログラムを改善するよりも不明瞭にする可能性が高いためです。それどころか、それは議論の始まりを示していた。エドガー・ダイクストラの有名な手紙「有害であると考えられる声明に行く」は、1968年に続いた。
一部の学者は、ベーム-ジャコピニの結果に純粋なアプローチを取り、ループのような命令breakやreturnループの途中からの命令でさえ、ベーム-ジャコピニの証明では必要ないため、悪い習慣であると主張しました。したがって、すべてのループに単一のループが必要であると主張しました。出口点。この純粋主義的なアプローチは、Pascalプログラミング言語（1968年から1969年に設計された）で具体化されています。これは、1990年代半ばまで、学界でプログラミングの入門クラスを教えるための好ましいツールでした。
エドワード・ヨードンは、1970年代には、最初から構造化プログラミングの方法で考える必要があるという議論に基づいて、自動化された手段によって非構造化プログラムを構造化プログラムに変換することに哲学的な反対さえあったと述べています。実用的な対位法は、そのような変換が既存のプログラムの大部分に利益をもたらしたということでした。自動変換の最初の提案の中には、EdwardAshcroftとZoharMannaによる1971年の論文がありました。
Böhm–Jacopiniの定理を直接適用すると、構造化チャートに追加のローカル変数が導入される可能性があり、コードの重複が発生する可能性も後者の問題は、この文脈ではループと半分の問題と呼ばれます。 Pascalはこれらの問題の両方の影響を受け、Eric S. Robertsが引用した経験的研究によると、学生プログラマーは、配列内の要素を検索する関数を作成するなど、いくつかの単純な問題についてPascalで正しい解を作成するのに苦労しました。Robertsが引用したHenryShapiroによる1980年の研究では、Pascalが提供する制御構造のみを使用すると、被験者の20％のみが正しい解を与えたが、ループの真ん中。
1973年、S。RaoKosarajuは、ループからの任意の深さのマルチレベルブレークが許可されている限り、構造化プログラミングに変数を追加することを回避できることを証明しました。 さらに、コサラジュは、プログラムの厳密な階層が存在することを証明しました。現在、コサラジュ階層と呼ばれ、整数nごとに、プログラムとして書き換えることができない深さnのマルチレベルブレークを含むプログラムが存在します。n未満の深さのマルチレベルブレークを使用（追加の変数を導入せずに）。 Kosarajuは、BLISSプログラミング言語のマルチレベルブレーク構造を引用しています。キーワードの形式でのマルチレベルの区切りは、実際にはその言語のBLISS-11バージョンで導入されました。オリジナルのBLISSにはシングルレベルのブレークしかありませんでした。BLISSファミリーの言語は、無制限のgotoを提供しませんでした。Javaプログラミング言語は、後にもこのアプローチに従うでしょう。 ：960–965 leave label
Kosarajuの論文からのより単純な結果は、プログラムが2つの異なる出口を持つループを含まない場合にのみ、（変数を追加せずに）構造化プログラムに還元できるということです。還元性は、大まかに言えば、元のプログラムと同じ関数を計算し、同じ「プリミティブアクション」と述語を使用するが、異なる制御フロー構造を使用することとして、Kosarajuによって定義されました。（これは、Böhm–Jacopiniが使用したものよりも還元性の狭い概念です。）この結果に触発されて、循環的複雑度の概念を紹介した彼の非常に引用された論文のセクションVIで、Thomas J.McCabeはクラトフスキの定理の類似物を説明しました。非構造化プログラムの制御フローグラフ（CFG）、つまり、プログラムのCFGを非構造化にする最小のサブグラフ。これらのサブグラフは、自然言語で非常によく説明されています。彼らです：
ループからの分岐（ループサイクルテスト以外）
ループに分岐
決定への分岐（つまり、if「分岐」への分岐）
決定からの分岐
McCabeは、サブグラフとして表示されるときにこれら4つのグラフが独立していないことを実際に発見しました。つまり、プログラムが非構造化されるための必要十分条件は、CFGがこれら4つのグラフのうち3つのサブセットのいずれかをサブグラフとして持つことです。彼はまた、非構造化プログラムにこれら4つのサブグラフのいずれかが含まれている場合、4つのセットとは別のサブグラフが含まれている必要があることも発見しました。この後者の結果は、非構造化プログラムの制御フローが一般に「スパゲッティコード」と呼ばれるものにどのように絡み合うかを説明するのに役立ちます。McCabeはまた、任意のプログラムが与えられた場合に、構造化プログラムであるという理想からどれだけ離れているかを定量化する数値測定を考案しました。マッケイブは彼の測定を本質的な複雑さと呼んだ。
少なくともダイクストラのD構造が構成要素と見なされる場合、構造化プログラミングの禁止グラフのMcCabeによる特性評価は不完全であると見なすことができます。 ：274–275 
1990年まで、既存のプログラムからgotoを排除し、その構造のほとんどを維持するための方法が提案されていました。この問題へのさまざまなアプローチは、上記のフォーク定理のような出力を回避するために、単にチューリングの等価性よりも厳密な等価性のいくつかの概念も提案しました。選択された同等性の概念の厳密さにより、必要な制御フロー構造の最小セットが決まります。Lyle Ramshawによる1988年のJACM論文は、それまでの分野を調査し、独自の方法を提案しています。 Java仮想マシンコードにはオフセットとして表現されたターゲットを持つ分岐命令があるため、Ramshawのアルゴリズムは、たとえば一部のJavaデコンパイラで使用されましたが、高レベルのJava言語にはマルチレベルとステートメントしかありません。 Ammarguellat（1992）は、単一出口の強制に戻る変換方法を提案しました。breakcontinue

COBOLへの適用
1980年代、IBMの研究者であるHarlan Millsは、COBOLコードに構造化アルゴリズムを適用したCOBOL構造化機能の開発を監督しました。Millsの変革には、手順ごとに次の手順が含まれていました。
手順の基本ブロックを特定します。
各ブロックの入口パスに一意のラベルを割り当て、各ブロックの出口パスに、それらが接続する入口パスのラベルを付けます。プロシージャからの戻りには0を使用し、プロシージャのエントリパスには1を使用します。
手順を基本ブロックに分割します。
1つの出口パスのみの宛先であるブロックごとに、そのブロックをその出口パスに再接続します。
プロシージャで新しい変数を宣言します（参照用にLと呼ばれます）。
残りの接続されていない出口パスごとに、そのパスのラベル値にLを設定するステートメントを追加します。
結果のプログラムを、Lで示されたエントリパスラベルでプログラムを実行する選択ステートメントに結合します。
Lが0でない限り、この選択ステートメントを実行するループを構築します。
Lを1に初期化し、ループを実行するシーケンスを作成します。
この構造は、選択ステートメントの一部のケースをサブプロシージャに変換することで改善できることに注意して

も参照してください
構造化プログラミング
チューリング完全性

参考文献
^ xter Kozen and Wei-Lung Dustin Tseng（2008）。Böhm–Jacopiniの定理は誤りであり、提案的です （PDF）。Mpc2008。コンピュータサイエンスの講義ノート。5133。177〜192ページ。CiteSeerX  10.1.1.218.9241。土井：10.1007 / 978-3-540-70594-9_11。ISBN 978-3-540-70593-2。
^ 「CSE111、2004年秋、BOEHM-JACOPINITHEOREM」。Cse.buffalo.edu。2004-11-22 。
^ Harel、David（1980）。「フォーク定理について」（PDF）。ACMの通信。23（7）：379–389。土井：10.1145 /358886.358892。
^ ボーム、コラド; ジュゼッペ・ジャコピーニ（1966年5月）。「フロー図、チューリングマシン、および2つのフォーメーションルールのみの言語」。ACMの通信。9（5）：366–371。CiteSeerX 10.1.1.119.9119。土井：10.1145 /355592.365646。   ^ ドナルドクヌース（1974）。「gotoStatementsを使用した構造化プログラミング」。コンピューティング調査。6（4）：261–301。CiteSeerX 10.1.1.103.6084。土井：10.1145 /356635.356640。   ^ ブルースイアンミルズ（2005）。プログラミングの理論的紹介。スプリンガー。NS。279. ISBN  978-1-84628-263-8。
^ Ammarguellat、Z。（1992）。「制御フローの正規化アルゴリズムとその複雑さ」。ソフトウェアエンジニアリングに関するIEEEトランザクション。18（3）：237–251。土井：10.1109 /32.126773。
^ Dijkstra、Edsger（1968）。「有害と考えられるステートメントに移動」。ACMの通信。11（3）：147–148。土井：10.1145 /362929.362947。2007年7月3日にオリジナルからアーカイブされました。
^ Roberts、E。「ループ出口と構造化プログラミング：討論の再開」、ACM SIGCSE Bulletin、（27）1：268–272。
^ EN Yourdon（1979）。ソフトウェア工学の古典。ユアドンプレス。PP。  49-50。ISBN  978-0-917072-14-7。
^ アシュクロフト、エドワード; ゾハル・マンナ（1971）「gotoprogramsから ‘while’programsへの翻訳」。IFIP会議の議事録。
配布が限られているために元の会議議事録では入手が困難であったこの論文は、Yourdonの1979年の本の51〜65ページに再発行されました。
^ デビッド・アンソニー・ワット; ウィリアムフィンドレイ（2004）。プログラミング言語の設計概念。ジョン・ワイリー＆サンズ。NS。 228。ISBN  978-0-470-85320-7。
^ ケネスC.ラウデン; ケネスA.ランバート（2011）。プログラミング言語：原則と実践（3版）。センゲージラーニング。頁 422 -423。ISBN  978-1-111-52941-3。
^ コサラジュ、S。ラオ。「構造化プログラムの分析」、Proc。第5回ACMシロップ。計算理論、（1973年5月）、240-252; また
Kosaraju、S.ラオ（1974）。「構造化プログラムの分析」。コンピュータとシステム科学のジャーナル。9：232–255。土井：10.1016 / S0022-0000（74）80043-7。ドナルド・クヌース（1974）によって引用されました
。「gotoStatementsを使用した構造化プログラミング」。コンピューティング調査。6（4）：261–301。CiteSeerX 10.1.1.103.6084。土井：10.1145 /356635.356640。  ^ ブレンダー、ロナルドF.（2002）。「BLISSプログラミング言語：歴史」（PDF）。ソフトウェア：実践と経験。32（10）：955–981。土井：10.1002 /spe.470。
^ 元の論文は
ThomasJ。McCabe（1976年12月）です。「複雑さの測定」。ソフトウェアエンジニアリングに関するIEEEトランザクション。SE-2（4）：315–318。土井：10.1109 /tse.1976.233837。二次解説については、Paul C. Jorgensen（2002）を参照してください
。ソフトウェアテスト：職人のアプローチ、第2版（第2版）。CRCプレス。pp。150–153。ISBN 978-0-8493-0809-3。
^ ウィリアムズ、MH（1983）。「フローチャートスキーマと命名法の問題」。コンピュータジャーナル。26（3）：270–276。土井：10.1093 / comjnl /26.3.270。
^ Ramshaw、L。（1988）。「プログラム構造を維持しながらgotoを排除する」。ACMのジャーナル。35（4）：893–920。土井：10.1145 /48014.48021。
^ ゴッドフリーノーラン（2004）。Javaの逆コンパイル。押してNS。142. ISBN  978-1-4302-0739-9。
^ https://www.usenix.org/legacy/publications/library/proceedings/coots97/full_papers/proebsting2/proebsting2.pdf ^ http://www.openjit.org/publications/pro1999-06/decompiler-pro-199906.pdf

参考文献
上記でまだカバーされていない資料：
デミロ、リチャードA.（1980）。「構造化プログラミングにおける時空のトレードオフ：改良された組み合わせ埋め込み定理」。ACMのジャーナル。27（1）：123–127。土井：10.1145 /322169.322180。
デビエンヌ、フィリップ（1994）。1つのバイナリホーン節で十分です。コンピュータサイエンスの講義ノート。775。pp。19–32。CiteSeerX  10.1.1.14.537。土井：10.1007 / 3-540-57785-8_128。ISBN 978-3-540-57785-0。