distance.mlw 2.03 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
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:
*)