【15】コードの論理的検証

　ソフトウェアに誤りがないことを論理的に検証するための「形式的証明（formal proof）」という手法があります。しかし形式的証明を手作業でやろうとすると、コードそのものを書くより手間がかかり、しかもその際にミスが起きる恐れもあります。自動ツールが使えればそのほうが望ましいのは確かですが、いつもそれが可能とは限りません。ここは間を取って、半形式的証明とでも呼べる方法をここでお話ししましょう。

　まずすべきことは、対象となるコードをすべて短いセクション——1 行、ファンクションコール 1 つだけのブロックから 10 行くらいのブロックまで——に分割することです。そうして短く切った上で、個々のセクションが正しいかどうかをチーム内で話し合うのです。その場合、どのセクションについても、メンバーの中で最も懐疑的な態度の人が正しいと納得すれば、一応「正しい」とみなしていいでしょう。

　コードをセクションに分ける際には、まずセクションの終端までの間で、プログラムのステート（プログラムカウンタや、すべての「生きた」オブジェクトの持つ値）が、簡単に説明できるようになっていることが重要です。また、セクションの中での機能（状態変化）は 1 つのタスク（仕事）に絞りこまれていて、これも簡単に説明できることが大切です。このガイドラインを守ると、検証が容易になり、関数の 事前条件 や 事後条件、ループやクラス（のインスタンス）の 不変条件（invariant）といった概念の意味を統一することにもつながります。個々のセクションをできるだけ他から独立させるように努力することも重要です。これも、もちろん検証を容易にすることに役立つわけですが、セクションに変更を加える際に、他への影響を考えずに済むという意味でも、絶対に必要なことと言えます。

　よく知られていて、一般的に良いとされている（しかし実際にはあまり実践されていない）コーディングプラクティスの多くは、コードの論理的検証を容易にする上でもやはり役立ちます。これは逆に言えば、論理的検証を楽にしようと努力するだけで、コードのスタイルや構造の改善につながるということです。実践すべきコーディングプラクティスの例を次にあげておきます。当然のことながら、こうしたプラクティスが守られているか否かは、多くの場合、静的コード解析によって自動的にチェックできます。

• goto 文の使用は避ける。使用すると、離れたところにあるセクションどうしに強い依存関係が生じてしまう。
• 変更可能なグローバル変数は作らない。変更可能なグローバル変数があると、それを使用するすべてのセクションが相互依存関係になってしまう。
• 変数のスコープは可能な限り小さくする。たとえば、ローカルオブジェクトは、最初に使用する部分の直前で宣言する。
• オブジェクトは可能な限り、不変（immutable）オブジェクト にする。
• 縦、横にうまくスペースを入れて、できるだけコードを読みやすくする。たとえば、関連し合う部分には同じようにインデントを入れる、セクションの分かれ目には空白行を入れるなど。
• オブジェクトや型、関数などには、その特性や機能がすぐにわかる（しかも比較的短い）名前をつける。それによりコードが自己ドキュメント化され、おおよその意味が、一見するだけでわかるようになる。
• セクションを入れ子にする必要が出た時は、それを関数にする。
• 関数はできる限り短くし、機能は 1 つに絞り込む。古くから言われる「24 行制限」は今も有効である。ディスプレイのサイズや解像度は変わっているが、人間の認知能力は 1960 年代からまったく変化していない。
• 関数のパラメータはできるだけ減らす（最高でも 4 つまでにする）。これは必ずしも、関数で扱うデータを減らすということを意味しない。関連するパラメータを 1 つのオブジェクトにまとめることで、オブジェクトの不変条件を 1 箇所に集中させることができる。それにより凝集性、整合性の検証が容易になる。
• ブロックからライブラリにいたるまで、コードのどの単位においても、インターフェースはできる限り狭くすべし。外部とのコミュニケーションが減れば、その分だけ検証すべき事柄も減ることになる。オブジェクト内部の状態を戻す「getter」があると、その分検証の負担が増える。処理対象となる情報を提供するようオブジェクトに要求する、というのは望ましいことではない。オブジェクトには、そのオブジェクトがすでに持っている情報の処理をさせるべきである。言い換えると、カプセル化とは結局のところ、インターフェースを狭くするということである。
• クラスの不変条件を保つという観点から、「setter」の使用は推奨できない。setter があると、オブジェクトの状態が変化することになり、不変条件が満たせなくなってしまう。

　コード正しさを論理的に検証すると同時に、コードの内容についても検証をし、チーム内で話し合うようにすれば、より理解を深めるのに役立ちます。自分が理解したことを互いに伝え合えば、全員にとって利益になるでしょう。