E0038

Warning name: missing_invariant

错误案例

循环缺少 proof_invariant 子句。

///|
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_invariant: a <= b,
  }
}