diff --git a/examples/programs/distance.mlw b/examples/programs/distance.mlw
new file mode 100644
index 0000000000000000000000000000000000000000..64f9f8ea2b5a88a7556dd7ccf487612404698d5b
--- /dev/null
+++ b/examples/programs/distance.mlw
@@ -0,0 +1,76 @@
+
+(*
+ 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:
+*)
diff --git a/examples/programs/distance/why3session.xml b/examples/programs/distance/why3session.xml
new file mode 100644
index 0000000000000000000000000000000000000000..7fd363ef8b3e02cab36a03f6e169e599fa424932
--- /dev/null
+++ b/examples/programs/distance/why3session.xml
@@ -0,0 +1,493 @@
+
+
+
+
+
+
+
+
+
+
+
+