プログラム中で特定の条件が満たされていることに言及するために、Scalaでは標準ライブラリでいくつかの関数が提供されています。assert, assume, require, ensuring です。それぞれどう使い分けたら良いのか、知らなかったので調べました。
Predef.scala のコメント には次のように書かれています。
* === Assertions ===
* A set of `assert` functions are provided for use as a way to document
* and dynamically check invariants in code. Invocations of `assert` can be elided
* at compile time by providing the command line option `-Xdisable-assertions`,
* which raises `-Xelide-below` above `elidable.ASSERTION`, to the `scalac` command.
*
* Variants of `assert` intended for use with static analysis tools are also
* provided: `assume`, `require` and `ensuring`. `require` and `ensuring` are
* intended for use as a means of design-by-contract style specification
* of pre- and post-conditions on functions, with the intention that these
* specifications could be consumed by a static analysis tool. For instance,
*
* {{{
* def addNaturals(nats: List[Int]): Int = {
* require(nats forall (_ >= 0), "List contains negative numbers")
* nats.foldLeft(0)(_ + _)
* } ensuring(_ >= 0)
* }}}
*
* The declaration of `addNaturals` states that the list of integers passed should
* only contain natural numbers (i.e. non-negative), and that the result returned
* will also be natural. `require` is distinct from `assert` in that if the
* condition fails, then the caller of the function is to blame rather than a
* logical error having been made within `addNaturals` itself. `ensuring` is a
* form of `assert` that declares the guarantee the function is providing with
* regards to its return value.
assert が基本で、assume, require, ensuring はそのバリエーションという位置づけです。
require と ensuring は契約による設計（design-by-contract, DbC)スタイルの事前条件、事後条件を表現するのに使います。
コードを呼ぶ側が事前条件と不変条件を満たす義務を負うことで、呼ばれたコードはその条件が恒真であるとの前提を利益として得る。引き換えに、呼ばれたコードは事後条件と不変条件を義務として負い、呼ぶ側の利益としてこれを保証する。
契約プログラミング (Wikipedia)
コメント中の addNaturals() 定義の例で示されているように、メソッドの引数が満たすべき性質（事前条件）の言及に requre を使い、メソッドの戻り値が満たすべき性質の言及に ensuring を使います。契約による設計では、事前条件(require)が満たされないのは呼び出し元の責任、事後条件(ensuring)が満たされないのは呼び出された側の責任です。
コンストラクタ引数に対しても呼び出し元に要求する制約は require で書くのが自然だと思います。
投げる例外
条件が満たされたなかった時にそれぞれ例外を投げます。assert, assume, ensuring は java.lang.AssertionError を投げます。require は java.lang.IllegalArgumentException を投げます。
ここからも require はメソッド引数が満たすべき条件をチェックすることに使うべきであると読み取れます。
コンパイル時に消せるか？
事後条件はメソッド実装の誤りを検知するためなので、メソッド実装がテストされた後では不要です（実際には網羅的なテストができないことのほうが多いですが）。性能の観点からは無い方が良いと言えます。
@elidable はコンパイル時に条件的に取り除くコードを示す annotation です。 assert, assume には @elidable(ASSERTION) が付いています。コンパイル時オプションに -Xdisable-assertions あるいは ASSERTION は 2000 と定義されているのでそれより大きい数を -Xelide-below 2001 などと指定することで assert, assume の呼び出しが消えてなくなります。
一方で require には @elidable が付いていません。require は呼び出し元の過ちを検知するためのものであり、呼び出し元と呼び出される側でコンパイル単位が別れる可能性を考慮すると、コンパイル時に確認することができないからでしょう。
ensuring にも @elidable は付いていません。 ensuring は def f(...) = { ... }.ensuring(cond) という使い方をすることを想定しているため、 もしコンパイル時に消すとメソッドの実装が消えてしまうことになるからでしょう。
ensuring は内部で assert を呼び出しています。ensuring のコンパイルは、Predef object を含む scala-library-x.y.z.jar を作成する際に終わっています。ユーザコードをコンパイルする際に -Xdisable-assertionsを付けても ensuring 内から呼び出している assert は消えません。 Predef.scala をコンパイルするときに -Xdisable-assertionsを付けると、チェックはせず単に渡された値を返す関数になりますが、通常は Predef.scala を自分でコンパイルすることはないでしょう。
assume って?
ここまでで require, ensuring についてはだいぶわかりました。 assume って何なんでしょう？
This method differs from assert only in the intent expressed: assert contains a predicate which needs to be proven, while assume contains an axiom for a static checker.
Predef.scala:223
静的コード解析ツールに対して、満たされているとみなして良い性質を与えるためのもののようです。assume で与えられた性質を仮定して、assert が満たされるかを静的コード解析ツールがチェックする、と。確認したい assert があって、その大前提として成り立っているべき条件があるときに assume を使うのでしょうか。
簡単に探したところ assume を解釈する静的コード解析ツールは今のところ無さそうです。あったら教えてください。
使い分け
使い分けるならこんな感じでしょうか。
- メソッドやコンストラクタの引数チェック → require
- メソッドの戻り値チェック → ensuring
- 別の assert の前提となる性質に言及する → assume
- その他 → assert