Rust 言語の事前条件制約
追記:以下の記述は古くなっている。事前条件制約はすでに言語から取り除かれた。
Rust 言語では関数に事前条件を指定することができる。
use std; // predicate pure fn is_even(x: int) -> bool { ret x % 2 == 0; } fn print_even_number(x: int) : is_even(x) { std::io::println(#fmt("%d", x)); } fn main(args: [str]) { let x = 42; check is_even(x); print_even_number(x); }
bool を返す pure 関数は predicate と呼ばれる。いかなる関数にも事前条件として predicate を指定することができる。事前条件 pred_fn(x)
を持つ関数を呼ぶときは、事前に check pred_fn(x);
を実行しなければならない。 check 式は predicate が真を返せば処理を続行し、偽を返せばその場で fail する。
check 式の強制は静的に解決される。 check pred_fn(x);
を通過した後、事前条件 pred_fn(x)
を持つ関数が呼ばれるまでに変数 x
が破壊的に変更されうる場合、コンパイルは失敗する。
Rust では、変数の破壊的変更可能性の有無は静的に判別できる。 Rust の軽量スレッド機構はスレッド間の変数共有を許可しないため、別スレッドにより変数が動的に書き換えられてしまうことはない。
ある関数が check 式をパスした値を返すとき、その値は呼び出し側では check 式をパスしたものとみなされないので注意が必要である。例:
fn get_even_number() -> int { let x = 42; check is_even(x); ret x; } fn main(args: [str]) { let x = get_even_number(); check is_even(x); // 必要 print_even_number(x); }