第４章 構造化プログラミング
証明
有害宣言
機能分割
正式に証明できない
救済のための科学
テスト
内容
構造化プログラミングとは、goto文を有害なものとしてなくし、その代わりに if/then/else や do/while/until などの「順次」「分岐」「反復」の制御を実現したプログラミングのこと。
構造化プログラミングは、Edger Wyde Dijikstra（読めない）が、数学の証明とプログラミングを結びつけることによってプログラムが正しいことを証明できるようにしようとして提唱したもの。
goto文をなくすことによって機能を正しく小さく分割できるようになった。
それによって問題が小さく分解され、正しいプログラムの証明ができるようになってきたかのように見えた。
しかし、結局は数学的証明はできなかった。
わかったことは、プログラミングは数学的な証明はできないこと。
プログラミングは正しいことを証明する数学ではなく、正しくないことを証明する科学（反証可能）であること。
科学は、どんなに実証しても常に「正しくないこと」の可能性が常に残っているが、それが目的のために十分正しいと判断されれば使われるもの。
これは、バグによって正しくないことの証明はできるが、それを修正したとしてもなんらかの「正しくないこと」の可能性が常に残っていることを意味する。
テストでは「正しくない」ことを「証明できなければ」、目的のために十分正しいとみなすという理屈で正しさを担保する。
アーキテクチャは正しく機能分割されていることがベストプラクティスと考えられている。
なので、構造化プログラミングの観点でアーキテクチャにとって重要なのは、反証可能な単位で正しく機能分割しプログラムを作成することである。
学びを活かすアイディア・行動
特になし
No responses yet