構造化プログラミング
こちらの本を読んでいます。
「構造化プログラミング」の章を読んで色々調べて自分なりの解釈をギリギリ持てたので、記録します
構造化プログラミングという概念が登場するまでの経緯と、目的、
現代の研究の進捗までをざっくりと説明してみます。
ハードウェアの進歩の歴史
1940年代から1950年代: 真空管時代
コンピュータシステムは真空管を主要な電子部品として使用していた。
真空管は大きく、エネルギーを多く消費し、発熱も大きかった。
1950年代から1960年代: トランジスタ時代
トランジスタの発明により、真空管から小型・低消費電力な電子部品への移行が始まった。
トランジスタは信号増幅や制御に使用され、コンピュータの性能と信頼性を向上させた。
1960年代から1970年代: 集積回路（IC）時代
集積回路は、複数のトランジスタや他の電子部品を半導体上に統合したもの。
ICの導入により、コンピュータの小型化、信頼性の向上、電力効率の改善が実現した。
1970年代から1980年代: マイクロプロセッサ時代
マイクロプロセッサの登場により、CPU（中央演算処理装置）が一つのチップ上に統合されるようになった。
マイクロプロセッサの普及により、パーソナルコンピュータが一般化し始めた。
ソフトウェア危機
高性能化するハードウェアのコストは低下する一方、複雑化するソフトウェア開発のコストは上昇する傾向が続くことにより、将来的にソフトウェアの供給が需要を満たせなくなるという考え方
(出典：https://ja.wikipedia.org/wiki/ソフトウェア危機)
真空管コンピュータ時代のプログラム
構造化プログラミングの概念が登場する以前、ソフトウェアが動作するハードウェアはこんな感じのものだった
UNIVAC120 (出典: http://museum.ipsj.or.jp/heritage/handai-shinkukan.html)
真空管コンピュータは、メモリ容量が限られており、したがって、載せられるプログラムのサイズに限りがあった。
つまり小規模プログラムの実行しか行えなかった。
- 基本的な算術演算
- データのソート、検索、統計処理
- 機械制御やシステムの制御(リアルタイム性はなし)
- 数値シミュレーション
このような小規模プログラムは、当時「手続き型」と呼ばれる方法で作られていた。
やりたい処理（手順）を順番に記述していく。
プログラムが小規模なため、直線的なプログラムはむしろ記述も理解も容易だった。
この時代、プログラムの正しさをどのように保障していたのかというと、
プログラマのスキルと経験、手作業による慎重なコーディングやデバッグによるものだったらしい。
トランジスタ時代のプログラム
トランジスタの発明、集積回路の開発が進むと、コンピュータのメモリ容量も増え、動作可能なプログラムのサイズが大きくなっていく。
すると、ソフトウェアに対して、さらなる需要が生まれてきた。
- グラフィックス処理
- データベース処理を用いたアプリケーション
- 大規模なデータ解析
このような中規模以上のプログラムを作るようになると、手続き型のメリットはそのままデメリットに変わった。
つまり、ロジックを直線的に記述する形では、ロジックを追うのが大変。
よって、プログラマの経験と勘でプログラムの正しさを保障する従来のやり方では、プログラムのサイズに対して開発のコストが爆発的に大きくなり、将来的にソフトウェアの供給が需要を満たせなくなるのではないかという危機感が生じた。（ソフトウェア危機）
プログラムの正しさを、論理的に（現実的な時間内で）証明する術があれば、問題は解決する。
プログラムの正しさの証明の試み
「証明」といえば数学。
数学では、公理・定義・定理・系・補助定理といった構造が採用されていて、その構造に論理を段階的に適用することで証明を行っている。
これと同じことが、（原理的には）プログラムにおいても可能であることは分かっている。(らしい。)
現実的にもそれが可能であることを示したい！
ダイクストラの研究
参考: https://eel3.hatenablog.com/entry/20150221/1424445453
プログラムには「静的構造」と「動的構造」というものがある。
この両方に対して証明を行わなければ、そのプログラムが正しいとは言えない。
GOTOを含む制御構文の話は、ここから先になる。GOTOの乱用が戒められた理由は、プログラムの静的構造>（ソースコード）と動的構造（実行時のフロー）の乖離が大きくなるからであった。
プログラムの静的構造と動的構造が一致しているならば、ソースコードという静的構造からプログラムの正しさが証明されている時、実行時のフローという動的構造の正しさも証明されている、と考えても問題ないだろう。しかし静的構造と動的構造が一致していないならば、静的構造の正しさが証明されても、それは動的構造の正しさが証明されたことを意味しない。
そこでまず、これらが一致するような形で、
かつ、「静的構造」が、正しさを証明することが現実的に可能な構造となるようにプログラムを構築する。
そして「静的構造」に対して証明を与えることで、動的構造の正しさをも保障し、プログラムの正しさを証明しようと試みた。
証明のための条件
- 静的構造と動的構造の一致
- 正しさを証明することが現実的に可能な構造
という二つの条件が必要だ。
しかし従来の（当時の）手続き型プログラミングは、go to文というものが不適切に多用されていることが原因で前者の条件を満たしていないことをダイクストラは突き止めた。
逆に言うと、適切にgo to文を使用すれば問題ない。
具体的には、「順次」「選択」「反復」の構造を作るという目的のみでgo to文を使用し、またそれらの構造のみで構築されたプログラムであれば、前者の条件を満たすことができる。
※goto文の例。これが多用されると、複雑怪奇なスパゲッティコードが出来上がる。
int x = 0;
int y = 0;
start:
x = x + 1;
y = y + 2;
if (x < 5) {
goto start;
}
※「順次」「選択」「反復」のみで任意のプログラムが構築できることの証明は、ベームとヤコピーニが証明した。（構造化定理）
証明の限界と、反証可能性
しかしながら、後者の条件は、達成されなかった。
静的構造と動的構造が一致するプログラムを構築していざ証明しようと思うと、莫大なコストがかかってしまう。
「正しさを証明することが現実的に可能な構造」がどういうものであるかは、いまだ未解決問題として残されている。
しかし、収穫はあった。
プログラムの全体の正しさを証明することが現実的にできなくても、
部分的にであれば正しいことを現実的に証明できるようになった。
許される時間内で、できるだけ多くの部分について、正しさを証明することにしよう。
以下は自分の解釈。
「部分」が正しいことを独立して証明するには、他の部分から影響を受けないことが重要である。
そのような構造は、「順次」「選択」「反復」以外の要素があるプログラムではありえない。
部分的に正しくないことが示されれば、そのプログラムは（全体としても）正しくないと確実に言える。
つまり、プログラムの「反証」である。
プログラムは（現実的に）証明可能ではないが、（現実的に）反証可能であることが分かった。
数学的アプローチとは異なり、科学的なアプローチと言える。
プログラムが「正しくない」ことの証明
いわゆる「テスト」である。
そして、反証（すなわちテスト）が（より）容易になるような制限を、
さらに上位のレベルでかけることになる。
（テストが「容易になる」とはどういうことか？逆にいうと、テストが困難とはどういうことなのか？）
Comming Soon …
まとめ
現在の言語では、go to文の無制限使用は許されていない。
よって、現代のプログラマは、構造化プログラミングを無意識のうちに行なっている。
それにより、プログラムは反証可能な状態で記述されている。
そして、その反証可能性に従って、時間の許す限りテストを書いてプログラムの信頼性をできる限り上げるということをしている。
一方で、中規模以上のプログラムにおいても、正しさを現実的に数学的に証明する方法の研究は続いている。
Discussion