error contract

Некорректный requires, ensures или invariant.

What it means#

Contract clauses are boolean expressions (§6.7, §4.2). requires may use the parameters, ensures may additionally use result and old(e), and invariant ranges over the fields. A clause of a non-boolean type, or one that uses a name that is not available in that position, is rejected.

Example#

fn withdraw(n: i32, amt: i32) -> i32 pure
  requires old(n) > 0      // <- contract (`old` is defined for ensures only)
  => n - amt

contract

How to fix#

fn withdraw(n: i32, amt: i32) -> i32 pure
  requires n > 0
  ensures result == old(n) - amt
  => n - amt

Make the clause a boolean expression over names visible there. Contract checks are on in the dev and test profiles and a violation panics.

See also#

• type-mismatch
• effects