examples/optimal_replay.mlw

   1
   2 (*
   3    Author: Jean-Christophe Filliatre (CNRS)
   4    Tool:   Why3 (see http://why3.lri.fr/)
   5
   6    The following problem was suggested to me by Ernie Cohen (Microsoft Research)
   7
   8    We are given an integer N>0 and a function f such that 0 <= f(i) < i
   9    for all i in 1..N-1. We define a reachability as follows:
  10    each integer i in 1..N-1 can be reached from any integer in f(i)..i-1
  11    in one step.
  12
  13    The problem is then to compute the distance from 0 to N-1 in O(N).
  14    Even better, we want to compute this distance, say d, for all i
  15    in 0..N-1 and to build a predecessor function g such that
  16
  17       i <-- g(i) <-- g(g(i)) <-- ... <-- 0
  18
  19    is the path of length d[i] from 0 to i.
  20 *)
  21
  22 module OptimalReplay
  23
  24   use int.Int
  25   use ref.Refint
  26   use array.Array
  27
  28   val constant n: int
  29     ensures { 0 < result }
  30
  31   val function f (k:int): int
  32     requires { 0 < k < n }
  33     ensures { 0 <= result < k}
  34
  35   (* path from 0 to i of distance d *)
  36   inductive path int int =
  37   | path0: path 0 0
  38   | paths: forall i: int. 0 <= i < n ->
  39            forall d j: int. path d j -> f i <= j < i -> path (d+1) i
  40
  41   predicate distance (d i: int) =
  42     path d i /\ forall d': int. path d' i -> d <= d'
  43
  44   (* function [g] is built into local array [g]
  45      and ghost array [d] holds the distance *)
  46   let distance () =
  47     let g = make n 0 in
  48     g[0] <- -1; (* sentinel *)
  49     let ghost d = make n 0 in
  50     let ghost count = ref 0 in
  51     for i = 1 to n-1 do
  52       invariant { d[0] = 0 /\ g[0] = -1 /\ !count + d[i-1] <= i-1 }
  53       (* local optimality *)
  54       invariant {
  55         forall k: int. 0 < k < i ->
  56            g[g[k]] < f k <= g[k] < k /\
  57            0 < d[k] = d[g[k]] + 1 /\
  58            forall k': int. g[k] < k' < k -> d[g[k]] < d[k'] }
  59       (* could be deduced from above, but avoids induction *)
  60       invariant { forall k: int. 0 <= k < i -> distance d[k] k }
  61       let j = ref (i-1) in
  62       while g[!j] >= f i do
  63         invariant { f i <= !j < i /\ !count + d[!j] <= i-1 }
  64         invariant { forall k: int. !j < k < i -> d[!j] < d[k] }
  65         variant { !j }
  66         incr count;
  67         j := g[!j]
  68       done;
  69       d[i] <- 1 + d[!j];
  70       g[i] <- !j
  71     done;
  72     assert { !count < n }; (* O(n) is thus ensured *)
  73     assert { forall k: int. 0 <= k < n -> distance d[k] k } (* optimality *)
  74
  75 end