E0039

Warning name: missing_reasoning

当需要进行证明检查的 for 循环没有 proof_reasoning 子句时，会发出此警告。证明推理记录了说明循环不变量为何得以保持、以及循环结果为何满足外围契约的论证。

错误案例

循环缺少 proof_reasoning 子句。

///|
fn fib(n : Int) -> UInt64 {
  for i = 0, a = 0UL, b = 1UL; i < n; i = i + 1, a = b, b = a + b {

  } else {
    b
  }
}

建议

添加一些证明推理。

///|
fn fib(n : Int) -> UInt64 {
  for i = 0, a = 0UL, b = 1UL; i < n; i = i + 1, a = b, b = a + b {

  } nobreak {
    b
  } where {
    proof_reasoning: (
      #|The variables `a` and `b` represent consecutive Fibonacci numbers, 
      #|so `a` is always less than or equal to `b`.
      #|
    ),
  }
}