Contact Version française

The ProVal team was stopped at the end of August 2012, and reborn into a new team Toccata
These pages do not evolve anymore, please follow the link above for up-to-date informations about our team.

Hoare's Proof of a Program: FIND


Authors: Jean-Christophe Filliâtre

Topics: Historical examples / Array Data Structure

Tools: Why3

index



(*
 C. A. R. Hoare.
 Proof of a program: Find.
 Commun. ACM, 14:39--45, January 1971.
*)

module FIND

  use import int.Int
  use import ref.Ref
  use import array.Array
  use import array.ArrayPermut

  constant _N: int (* actually N in Hoare's notation *)
  constant f: int

  axiom f_N_range: 1 <= f <= _N

  predicate found (a: array int) =
    forall p q:int. 1 <= p <= f <= q <= _N -> a[p] <= a[f] <= a[q]

  predicate m_invariant (m: int) (a: array int) =
    m <= f /\ forall p q:int. 1 <= p < m <= q <= _N -> a[p] <= a[q]

  predicate n_invariant (n: int) (a: array int) =
    f <= n /\ forall p q:int. 1 <= p <= n < q <= _N -> a[p] <= a[q]

  predicate i_invariant (m: int) (n: int) (i: int) (r: int) (a: array int) =
    m <= i /\ (forall p:int. 1 <= p < i -> a[p] <= r) /\
    (i <= n -> exists p:int. i <= p <= n /\ r <= a[p])

  predicate j_invariant (m: int) (n: int) (j: int) (r: int) (a: array int) =
    j <= n /\ (forall q:int. j < q <= _N -> r <= a[q]) /\
    (m <= j -> exists q:int. m <= q <= j /\ a[q] <= r)

  predicate termination (i:int) (j:int) (i0:int) (j0:int) (r:int) (a:array int) =
    (i > i0 /\ j < j0) \/ (i <= f <= j /\ a[f] = r)

  let find (a: array int) =
    requires { length a = _N+1 }
    ensures  { found a /\ permut a (old a) }
'Init:
  let m = ref 1 in let n = ref _N in
  while !m < !n do
    invariant { m_invariant !m a /\ n_invariant !n a /\
      permut a (at a 'Init) /\ 1 <= !m /\ !n <= _N }
    variant { !n - !m }
    let r = a[f] in let i = ref !m in let j = ref !n in
    while !i <= !j do
      invariant { i_invariant !m !n !i r a /\ j_invariant !m !n !j r a /\
        m_invariant !m a /\ n_invariant !n a /\ 0 <= !j /\ !i <= _N + 1 /\
        termination !i !j !m !n r a /\ permut a (at a 'Init) }
      variant { _N + 2 + !j - !i }
  'L: while a[!i] < r do
        invariant { i_invariant !m !n !i r a /\
          at !i 'L <= !i <= !n /\ termination !i !j !m !n r a }
        variant { _N + 1 - !i }
        i := !i + 1
      done;

      while r < a[!j] do
        invariant { j_invariant !m !n !j r a /\
          !j <= at !j 'L /\ !m <= !j /\ termination !i !j !m !n r a }
        variant { !j }
        j := !j - 1
      done;

      assert { a[!j] <= r <= a[!i] };

      if !i <= !j then begin
        let w = a[!i] in begin a[!i] <- a[!j]; a[!j] <- w end;
        assert { exchange a (at a 'L) !i !j };
        assert { a[!i] <= r }; assert { r <= a[!j] };
        i := !i + 1;
        j := !j - 1
      end
    done;

    assert { !m < !i /\ !j < !n };

    if f <= !j then
      n := !j
    else if !i <= f then
      m := !i
    else
      begin n := f; m := f end
  done

end

download ZIP archive