プログラムの正しさってなんじゃ

こんばんわ、すげーことについて書かせていただく雄一です。 今回もCとか関係ないんですが、まぁいいよね。
ぶっちゃけCのことなんか知りたくないよね

やっぱり、ただ動けばいいというものではない

まぁ世の中いろんな電子機器があって、そのなかにはわれらの誇るプログラムで動いてるものばかりなのですが・・・
医療関係とか、航空関係とか、ちょっとミスあると大変なことになるようなものもプログラムで動いています。
で、そんなプログラムにはバグは大変まずいわけで、それはもう入念にチェックして使用しているハズです。
飛行機墜落しちゃったけど、管制塔システムのバグなんでしょうがないです。とかやばいですよね。

で、買い手は思うわけです。
作ってもらったプログラムが出来上がったけど、受け入れて問題ないのかなぁ?
当然ですよね、一般ソフトでなければ、そりゃもう多額ですから。
で、買い手は、ぱっと見思ったとおり動いているけど、このソフトが信用できる証拠をつけてくれ、その分の金も払うし、証拠がなきゃ買わないよん。
と、おっしゃいます。

で、現実どうやってんの?

さて、ソフト開発側としては困ったことになったぞーと思うわけです。
証拠って・・・何すりゃいいのさ?
現在のスタイルでは、テスト仕様書とテスト結果報告書を証拠とするのが一般的だと思います。
もう、見るもおぞましいほどの量を作成しなければなりません。
たいていの場合は、プログラムのステップ数(大雑把に行数)いくつにつき、いくつってカンジでテスト数の目安を決定し、テスト項目を作り、テストをこなすって流れ。
このステップ数にたいしてのテスト項目数の割合が信頼性の度合い・・・だそうで。
で、実際の作業でバグが出たら、報告書にバグ有、修正済ってことを書く。
ステップ数ふえればバグ増えるんで、ステップ数に対しての目標バグ検出数もきまってたり。
・・・はて?すでにおかしいとおもいませぬか?
たとえば入力がcharだけの関数をテストするなら、256通りのテストをするだけですよね?
何で行数だけでテスト数決めちゃってるの? どんなに長いプログラムでも、短いプログラムでも、テスト数は入力パターンに依存するんじゃないの? まぁcharだけの関数であまり長い関数ってのもないんで、現実テスト項目数10個とか。
え?後の246通りは放置プレイですか?
で、その10個ってどうやって決めたんですか?
「ん、マイナス値とかゼロとか、問題ありそうなところ」
え?問題あるプログラムを作っちゃったんですか?マゾ過ぎます!

じゃどうするの?

まぁプログラムの正当性を数学的に証明すればよいのです。
たとえばループ部分は帰納法を使って、「1の時に正しい解が出る。nの時正しい解が出る。n+1で正しい解が出る」ことを証明すればすべての値で正しい解が出る事を証明できたアレを使って〜みたいな。
まぁ難しいんで、ここでは解説しません。

プログラムが正しいってどういうこと?
そもそもどういうことなんでしょ。
学問的には条件二つ。
「事前条件が成り立つ時に、実行後に、事後条件が成立してること」
「プログラムが必ず停止すること」
つまり、無限ループしてても片方成り立つわけですな!間違った答えを出すならいっそとまらなければいいのに・・・

まとめ

まぁ理想論ばかり語っててもしょうがないのです。
だから現在はテストをすることでごまかしているのです。
というか、こんなにテストしたので勘弁してくださいとお願いしているわけです。
最後は泣きで済ませる業界なのです。
まだまだ進歩してない世界ってことですね。

テストは、「間違いの存在を示すには有効であるが、間違いが存在しないことを示すには絶望的に無力である」という本質的な限界を知るべき。