ヤルキデナイズド

Unclassified Articles on Software and IT

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);
}