Wiki Agenda Contact Version française

Optimal replay

Challenge proposed by Ernie Cohen


Authors: Jean-Christophe Filliâtre

Topics: Array Data Structure / Ghost code

Tools: Why3

see also the index (by topic, by tool, by reference, by year)


(*
   Author: Jean-Christophe Filliatre (CNRS)
   Tool:   Why3 (see http://why3.lri.fr/)

   The following problem was suggested to me by Ernie Cohen (Microsoft Research)

   We are given an integer N>0 and a function f such that 0 <= f(i) < i
   for all i in 1..N-1. We define a reachability as follows:
   each integer i in 1..N-1 can be reached from any integer in f(i)..i-1
   in one step.

   The problem is then to compute the distance from 0 to N-1 in O(N).
   Even better, we want to compute this distance, say d, for all i
   in 0..N-1 and to build a predecessor function g such that

      i <-- g(i) <-- g(g(i)) <-- ... <-- 0

   is the path of length d[i] from 0 to i.
*)

module OptimalReplay

  use import int.Int
  use import ref.Refint
  use import array.Array

  (* parameters [N] and [f] are introduced as logic symbols *)
  constant n: int
  axiom n_nonneg: 0 < n

  function f int: int
  axiom f_prop: forall k: int. 0 < k < n -> 0 <= f k < k

  (* path from 0 to i of distance d *)
  inductive path int int =
  | path0: path 0 0
  | paths: forall i: int. 0 <= i < n ->
           forall d j: int. path d j -> f i <= j < i -> path (d+1) i

  predicate distance (d i: int) =
    path d i /\ forall d': int. path d' i -> d <= d'

  (* function [g] is built into local array [g]
     and ghost array [d] holds the distance *)
  let distance () =
    let g = make n 0 in
    g[0] <- -1; (* sentinel *)
    let ghost d = make n 0 in
    let ghost count = ref 0 in
    for i = 1 to n-1 do
      invariant { d[0] = 0 /\ g[0] = -1 /\ !count + d[i-1] <= i-1 }
      (* local optimality *)
      invariant {
        forall k: int. 0 < k < i ->
           g[g[k]] < f k <= g[k] < k /\
           0 < d[k] = d[g[k]] + 1 /\
           forall k': int. g[k] < k' < k -> d[g[k]] < d[k'] }
      (* could be deduced from above, but avoids induction *)
      invariant { forall k: int. 0 <= k < i -> distance d[k] k }
      let j = ref (i-1) in
      while g[!j] >= f i do
        invariant { f i <= !j < i /\ !count + d[!j] <= i-1 }
        invariant { forall k: int. !j < k < i -> d[!j] < d[k] }
        variant { !j }
        incr count;
        j := g[!j]
      done;
      d[i] <- 1 + d[!j];
      g[i] <- !j
    done;
    assert { !count < n }; (* O(n) is thus ensured *)
    assert { forall k: int. 0 <= k < n -> distance d[k] k } (* optimality *)

end

download ZIP archive

Why3 Proof Results for Project "optimal_replay"

Theory "optimal_replay.OptimalReplay": fully verified in 1.58 s

ObligationsAlt-Ergo (0.99.1)CVC3 (2.4.1)CVC4 (1.4)Z3 (3.2)Z3 (4.3.2)
VC for distance---------------
split_goal_wp
  1. array creation size0.01------------
2. index in array bounds0.02------------
3. array creation size0.01------------
4. assertion0.01------------
5. assertion0.02------------
6. loop invariant init0.01------------
7. loop invariant init0.02------------
8. loop invariant init0.02------------
9. loop invariant init0.02------------
10. loop invariant init0.02------------
11. type invariant0.01------------
12. index in array bounds0.02------------
13. index in array bounds0.01------------
14. loop invariant preservation---0.040.020.020.03
15. loop invariant preservation---0.04---0.39---
16. loop variant decrease0.11------------
17. type invariant0.02------------
18. index in array bounds0.02------------
19. index in array bounds0.02------------
20. index in array bounds0.01------------
21. loop invariant preservation0.02------------
22. loop invariant preservation---0.280.05------
23. loop invariant preservation---------------
inline_goal
  1. loop invariant preservation---------------
split_goal_wp
  1. loop invariant preservation0.12------------
2. loop invariant preservation------0.17------
24. assertion0.02------------
25. assertion0.00------------