合同程式設計

你可以使用 requires 宣告引數具有特定值。

int fib (int i) requires (i > 0) {
    if (i == 1) {
        return i;
    } else {
        return fib (i - 1) + fib (i - 2);
    }
}

fib (-1);

編譯期間不會出現任何錯誤，但執行程式時會出錯，但函式不會執行。

你還可以斷言返回值與 ensures 匹配某個條件

int add (int a, int b) ensures (result >= a && result >= b) {
    return a + b;
}

你可以擁有儘可能多的 requires 和 ensures。