跳转至

对范围进行限定

假设某个条件成立:assume

对于可能抛出异常的操作都在编译时进行检查,如果能证明不会抛出异常则不会生成运行时检查代码,但如果用户进行了错误的假设则可能导致大范围的未定义行为。

val a = 输入值;
assume a != 0;            // 用户假设 a 不为零
val b = 100.0 / a as f32; // 如果用户假设错误则这里会导致未定义行为
// 这之后我们会认为 b 是一个合法的浮点数
// 这也会自动移除所有对 b 是否为 NaN 或无穷大的检查
// 因为用户已经假设了 a 是不为零的整数

不管怎样,为一个量随意提供假设是很不安全的行为。一定要在能够保证假设正确的情况下使用 assume。在 Debug 模式下,assume 应当被视为 assert 进行校验。

如果出现任何在 assume 下不可达的代码路径,编译器应当产生编译错误。

通过 assume 推断参数范围

假设有如下代码:

fn reciprocal(int a) -> f32 {
    assume a != 0;
    return 1.0 / a as f32;
}

此时参数 a 会被标记为非零整数,因此在调用 reciprocal 时传入编译期常量 0 会导致编译错误:

val x = reciprocal(0); // 编译错误:参数 a 可能为零

当然一般情况 assume 是用来对 ffi 进行假设的。

对参数范围进行限定

我们用 where 关键字对泛型参数进行范围限定:

fn sqrt(f32 x where x >= 0.0) -> f32 {
    假设我们实现了
}

注意 where 后接一个布尔表达式,该表达式会在调用时进行检查,如果不满足则抛出异常。同时作为优化手段也会在编译期进行检查,如果能证明调用时该表达式总为真则不会生成运行时检查代码。

where 后的表达式必须为纯表达式,且只能使用参数变量和常量。