読者です 読者をやめる 読者になる 読者になる

$shibayu36->blog;

株式会社はてなでエンジニアをしています。プログラミングや読書のことなどについて書いています。

関数の仕様を正しく実装していることをどう保証するのか

 静的型チェックがあったらテストはあまり書かなくて良いのか - $shibayu36->blog; で静的型チェックがあったとしても、テストをあまり書かなくて良いわけではないという話を書いた。するとブコメでいろいろ意見をもらえた。これらの意見から、関数の仕様を正しく実装していることをどう保証するのかについてもう少し深く考えてみようと思い、その考えがまとまってきたので、ブログに書いておく。

 一応前提として、今回の話は自分の経験とこれまでの本を読んだ知識を元に自分で考えたものであり、何かの理論に則って話しているわけではない。この部分が違うなどあれば突っ込みを受けたい。

今回考える仕様

 このようなことを考える時、非常にシンプルに考えたほうが理解がしやすいので、以下の様な仕様を持つ関数addNaturalIntを考える。

関数addNaturalIntは正の整数を二つ受け取り、足しあわせて正の整数を返す

 さらにこの仕様をもう少し分解すると次のようになる。

  • 1. 引数として整数を二つ受け取り
  • 2. それらは正の整数であり
  • 3. 二つの引数を足しあわせた結果を返す
  • 4. 結果は整数であり
  • 5. かつ正の整数である

実装の正しさが保証されていない簡単な実装

 以上の仕様をJavaScriptっぽい記法で簡単に実装すると

function addNaturalInt(a, b) {
    return a + b;
}

となる。しかしこれは先程分解した仕様の1~5の全てを満たしていることを保証できていない。それぞれ以下のような間違いが起きうるようになっている。

  • 引数として小数を受け取ると1の仕様を満たさない
  • 引数として負の整数を受け取ると2の仕様を満たさない
  • 現在は正しい実装であるが、もしa + bのところを間違えてa + b + 1としていたら、3の仕様を満たさない
  • 引数が正しくない場合や内部実装が間違っていた場合、4の仕様を満たしていると限らない
  • 引数が正しくない場合や内部実装が間違っていた場合、5の仕様を満たしていると限らない

実装の正しさを保証する

 それではどのようにすると、実装がこれらの仕様を満たすことを保証できるだろうか。保証する方法として、例えば以下の方法が考えられる。

  • 型検査
  • 表明
  • テスト

 他の方法ももちろんあるだろうが、今回はこの3つで考えてみる。

型検査で1と4の仕様を満たすことを保証する

 型検査があれば、1と4の仕様を満たすことを保証できる。例えば先ほどの実装を型があるものに置き換えたものが以下である。

function addNaturalInt(a: Int, b: Int): Int {
    return a + b;
}

 これにより少なくとも引数が整数であり、返り値が整数であることは型システムによって保証できた。ただし、これだけだと正の整数であることまでは保証できてはいないことに注意。


 仕様を満たすことを保証するということだけであれば、型検査は静的型検査でも動的型検査でもどちらでも良い。静的型検査のほうがコンパイル時にチェックされるため、バグを早期に見つけられるという利点はある。動的型検査については、以前Web+DBに書かせてもらったので、こちらも参考にして欲しい。

blog.shibayu36.org

表明で2と5の仕様を満たすことを保証する

 型検査の段階で関数の入力が整数であり、出力が整数であることが保証された。しかし、入力が正の整数であり、出力が正の整数であること、つまり2と5の仕様は保証されていない。

 この時、例えばNaturalInt型のようなものを使うという手もあるが、表明という仕組みもある。表明とは、wikipediaから参照すると次のものである。

表明(ひょうめい、assertion)とは、プログラミング言語の構文の一種であり、そのプログラムの前提条件を示すのに使われる。アサーションとも呼ばれる。

https://ja.wikipedia.org/wiki/%E8%A1%A8%E6%98%8E

 また表明についてはオブジェクト指向入門という本にも紹介されていて、1章近く説明されているので、そちらも参照して欲しい。
「オブジェクト指向入門 第11章 契約による設計」を読んだ - $shibayu36->blog;という記事でも少し言及している。

 これを先ほどの関数に追加してみる。オブジェクト指向入門という本では事前条件にrequire、事後条件にensureというキーワードを利用しているので、このキーワードを利用して記述してみる。よくある表明の記法とは違っているけど、事前条件と事後条件をチェックするというのを分かりやすく書くためにこういう記法にしている。

function addNaturalInt(a: Int, b: Int): Int require(a > 0 && b > 0) {
    return a + b;
} ensure(return_value > 0);

 この書き方の意味は、渡ってきたaとbは両方とも0より大きい数字であり、また返り値は0より大きい数字であるというものである。このチェックは実行時に行われ、もしこれを満たさなかった場合例外が起こるようになる。


 これにより引数と結果は正であることが保証され、これと先ほどの型制約と合わせることによって、2と5の仕様である引数が正の整数で、結果が正の整数であることが保証された。


テストで3の仕様を満たすことを保証する

 あとは3番目の「二つの引数を足しあわせた結果を返す」について保証したい。これはテストを書くことである程度は保証できる。

 例えばこの関数とは別に、以下のテストを書いてみる。この時正の整数以外が入力に入ることは他の項目で保証されているので、気にしなくても良い。

assert.equal(addNaturalInt(2, 3), 5);
assert.equal(addNaturalInt(100, 205), 305);

 全ての正の整数を網羅するわけではないので完全に保証できるわけではないが、二つの数字を足し合わせていることがある程度ではあるが保証できる。少なくとも内部でa - bしているとか、a + b + 1していることはないということは保証できる。


 一旦テストケースの網羅性の話は今回はしない。この話は http://qualab.jp/materials/q_te.140528.color.pdf が良い資料だった。

 また関連して、テストが何を保証してくれて、さらにプログラムの証明という分野の話もしている プログラムに証明が付く日 | RANDMAX の資料も面白かった。プログラムの証明という話はCoq を始めよう も参考になりそう。

まとめ

 今回は関数の仕様を正しく実装できていることをどう保証するかというネタでブログを書いてみた。最初に書いたとおり、今回の話は自分の経験とこれまでの本を読んだ知識を元に自分で考えたものであるため、何か突っ込みがあれば教えて欲しい。

 あと表明の話とかはオブジェクト指向入門を読むと最高の気分になれるのでおすすめです。

オブジェクト指向入門 第2版 原則・コンセプト (IT Architect’Archive クラシックモダン・コンピューティング)

オブジェクト指向入門 第2版 原則・コンセプト (IT Architect’Archive クラシックモダン・コンピューティング)