(*
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 0..N-1. We define a reachability as follows:
each integer i in 0..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 Distance
use import int.Int
use import module ref.Refint
use import module 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 in an array and then returned *)
let distance () =
{ }
let g = make n 0 in
g[0] <- -1; (* sentinel *)
let d = make n 0 in
d[0] <- 0; (* redundant *)
let count = ref 0 in (* ghost *)
for i = 1 to n-1 do
invariant { g[0] = -1 /\
(forall k: int. 0 < k < i -> f k <= g[k] < k) /\
(forall k: int. 0 < k < i -> d[k] = d[g[k]] + 1) (* /\
(forall k: int. 0 <= k < i -> path d[k] k) *) }
let j = ref (i-1) in
while g[!j] >= f i do
invariant { f i <= !j < i }
variant { !j }
j := g[!j];
incr count
done;
d[i] <- 1 + d[!j];
g[i] <- !j
done;
g
{ forall k: int. 0 < k < n -> f k <= result[k] < k }
end
(*
Local Variables:
compile-command: "why3ide distance.mlw"
End:
*)