method Max(a: int, b: int)
    returns (m: int)
  ensures m >= a && m >= b
  ensures m == a || m == b
{
  if a >= b { m := a; }
  else { m := b; }
}

predicate Sorted(s: seq<int>)
{
  forall i, j ::
    0 <= i < j < |s| ==>
      s[i] <= s[j]
}

method BinarySearch(a: array<int>,
    key: int)
    returns (index: int)
  requires Sorted(a[..])
  ensures 0 <= index ==>
    a[index] == key
  ensures index < 0 ==>
    forall k ::
      0 <= k < a.Length ==>
        a[k] != key
{
  var lo, hi := 0, a.Length;
  while lo < hi
    invariant 0 <= lo <= hi
  {
    var mid := (lo + hi) / 2;
    if a[mid] < key {
      lo := mid + 1;
    } else if key < a[mid] {
      hi := mid;
    } else {
      return mid;
    }
  }
  return -1;
}

lemma MaxCommutative(a: int, b: int)
  ensures Max(a, b) == Max(b, a)
{
}

fn verify(x: &State) -> bool {
    x.balance >= 0
        && x.locked <= x.balance
}

#[requires(n > 0)]
#[ensures(ret >= n)]
fn next_pow2(n: u64) -> u64 {
    let mut p = 1;
    while p < n {
        p <<= 1;
    }
    p
}

(declare-const x Int)
(declare-const y Int)
(assert (> x 0))
(assert (= (+ x y) 10))
(check-sat)
; sat
(get-model)
; (define-fun x () Int 3)
; (define-fun y () Int 7)

(assert (forall ((a Int) (b Int))
  (=> (and (> a 0) (> b 0))
      (> (+ a b) 0))))
(check-sat)
; unsat

impl Repair for Patch {
    fn verify(&self) -> Outcome {
        if self.tests_pass()
            && self.no_regression() {
            Outcome::Plausible
        } else {
            Outcome::Rejected
        }
    }
}

Martin Mirchev

Blog posts