optimal_replay.mlw 2.3 KB
 Jean-Christophe committed Jul 18, 2012 1 2 3 4 5 6 7 8 `````` (* 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 `````` Jean-Christophe committed Jul 20, 2012 9 10 `````` 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 `````` Jean-Christophe committed Jul 18, 2012 11 12 13 14 15 16 17 18 19 20 21 `````` 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. *) `````` Jean-Christophe Filliatre committed Oct 31, 2012 22 ``````module OptimalReplay `````` Jean-Christophe committed Jul 18, 2012 23 24 `````` use import int.Int `````` Andrei Paskevich committed Oct 13, 2012 25 26 `````` use import ref.Refint use import array.Array `````` Jean-Christophe committed Jul 18, 2012 27 28 29 30 31 32 `````` (* parameters [N] and [f] are introduced as logic symbols *) constant n: int axiom n_nonneg: 0 < n function f int: int `````` Jean-Christophe committed Jul 20, 2012 33 `````` axiom f_prop: forall k: int. 0 < k < n -> 0 <= f k < k `````` Jean-Christophe committed Jul 18, 2012 34 35 36 37 38 39 40 41 42 43 `````` (* 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' `````` Jean-Christophe committed Jul 20, 2012 44 `````` (* function [g] is built into local array [g] `````` Jean-Christophe committed Jul 21, 2012 45 `````` and ghost array [d] holds the distance *) `````` Jean-Christophe committed Jul 18, 2012 46 47 48 `````` let distance () = let g = make n 0 in g[0] <- -1; (* sentinel *) `````` Jean-Christophe committed Jul 21, 2012 49 50 `````` let ghost d = make n 0 in let ghost count = ref 0 in `````` Jean-Christophe committed Jul 18, 2012 51 `````` for i = 1 to n-1 do `````` Andrei Paskevich committed Oct 13, 2012 52 53 `````` invariant { d[0] = 0 /\ g[0] = -1 /\ !count + d[i-1] <= i-1 } (* local optimality *) `````` Jean-Christophe committed Jul 20, 2012 54 `````` invariant { `````` Andrei Paskevich committed Oct 13, 2012 55 `````` forall k: int. 0 < k < i -> `````` Jean-Christophe committed Jul 20, 2012 56 `````` g[g[k]] < f k <= g[k] < k /\ `````` Jean-Christophe Filliatre committed Sep 07, 2012 57 `````` 0 < d[k] = d[g[k]] + 1 /\ `````` Andrei Paskevich committed Oct 13, 2012 58 59 60 `````` 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 -> path d[k] k } `````` Jean-Christophe committed Jul 18, 2012 61 62 `````` let j = ref (i-1) in while g[!j] >= f i do `````` Andrei Paskevich committed Oct 13, 2012 63 64 `````` invariant { f i <= !j < i /\ !count + d[!j] <= i-1 } invariant { forall k: int. !j < k < i -> d[!j] < d[k] } `````` Jean-Christophe committed Jul 18, 2012 65 `````` variant { !j } `````` Jean-Christophe committed Jul 21, 2012 66 `````` incr count; `````` Jean-Christophe committed Jul 21, 2012 67 `````` j := g[!j] `````` Jean-Christophe committed Jul 18, 2012 68 `````` done; `````` Jean-Christophe committed Jul 21, 2012 69 `````` d[i] <- 1 + d[!j]; `````` Jean-Christophe committed Jul 18, 2012 70 71 `````` g[i] <- !j done; `````` Jean-Christophe committed Jul 20, 2012 72 73 `````` assert { !count < n }; (* O(n) is thus ensured *) assert { forall k: int. 0 <= k < n -> distance d[k] k } (* optimality *) `````` Jean-Christophe committed Jul 18, 2012 74 75 `````` end``````