15-コードの論理的検証

「プログラマが知るべき97のこと」の15個目のエピソードは、コードの正さを証明する方法の話です。コードの論理的な検証の方法として「形式的証明（formal proof）」と呼ばれる方法があります。詳細までは知りませんが、数学的なアプローチでプログラムを検証する方法だそうです。これに対し、JUnitなどで単体テストを行うような場合は、いわゆるサンプリングによる検証です。サンプリングによる検証も有効ですが、サンプリングである以上網羅的で完璧な証明は出来ません。形式的証明、つまり入力値が数学的なモデルに落とし込み帰納法などの手法を組み合わせるなどの方法をとることで、より完全に近づいた検証が可能になるります。しかし、形式的証明ができれば完璧かというとそうではありません。検証自体に誤りが混在する可能性はゼロにできませんし、コストも高く、難易度も高いのです。また、形式的証明を使ったとしてもソフトウェアにバグが無いことは証明できません*1。
このエピソードでは半形式的証明という方法を紹介しています。半形式的証明と言っても特別な事は何もありません。コードが正しい事を検証しやすい形でコードを記述し、レビューによってコードの検証を行うということです。

論理的検証を楽にしようと努力するだけで、コードのスタイルや構造の改善につながるということです。

検証しやすい形にするため、メソッドの粒度を適切に細かくし、各メソッドの責務を最小限に、解りやすくします。これは一般的に「良いコード」を書くためのプラクティスですが、「良いコード」は同時に検証を行いやすいという事です。一目で何をしたいを雄弁に語るコードであれば、論理的に間違っている可能性は低くなります。可読性が高ければレビュー時に検証を行うコストも下がり、間違いに気付きやすいでしょう。コードを美しく保つこと、それがコードの正さを検証する為に最も効果があるのです。
その為に必要なプラクティスとして次のような項目があげられています。

• goto禁止
• グローバル変数を避ける
• 変数のスコープは短く
• 不変オブジェクトを好む
• コードレイアウトを工夫する
• 名前重要
• 関数に分割する
• 関数のパラメータは４つまで
• インターフェイスを狭くする
• setterを避ける

どの項目も、いわゆるコーディング標準等で規定されている内容です。コーディング規約を学び守ることは自然に美しく検証しやすいコードを書く訓練です。自由に書く事を美徳とするのも良いですが、一般的な型を知りそこから自分流を作らなければ、ただの読みにくい勝手コードでしかありません。
読みやすく美しいコードを書くことはコードの品質を高める事に繋がります。

プログラマが知るべき97のこと

*1:皮肉なことに、バグがないことを証明できないことは簡単に証明できる