vstte10_inverting.mlw 1.85 KB
Newer Older
1 2 3 4
(*
   VSTTE'10 competition http://www.macs.hw.ac.uk/vstte10/Competition.html
   Problem 2: inverting an injection

5 6
   Author: Jean-Christophe Filliatre (CNRS)
   Tool:   Why3 (see http://why3.lri.fr/)
7
*)
8

9
module InvertingAnInjection
10

11 12
  use int.Int
  use array.Array
13
  use map.MapInjection as M
14

15
  predicate injective (a: array int) (n: int) = M.injective a.elts n
16

17
  predicate surjective (a: array int) (n: int) = M.surjective a.elts n
18

19
  predicate range (a: array int) (n: int) = M.range a.elts n
20

21
  let inverting (a: array int) (b: array int) (n: int) : unit
22
    requires { n = length a = length b /\ injective a n /\ range a n }
23
    ensures  { injective b n }
24
  = for i = 0 to n - 1 do
25
      invariant { forall j. 0 <= j < i -> b[a[j]] = j }
26
      b[a[i]] <- i
27
    done
28

29
  (* variant where array b is returned /\ with additional post *)
30

31
  let inverting2 (a: array int) (n: int) : array int
32
    requires { n = length a /\ injective a n /\ range a n }
33 34
    ensures  { length result = n /\ injective result n /\
               forall i. 0 <= i < n -> result[a[i]] = i }
35
  = let b = make n 0 in
36
    for i = 0 to n - 1 do
37
      invariant { forall j. 0 <= j < i -> b[a[j]] = j }
38 39 40 41 42 43 44 45
      b[a[i]] <- i
    done;
    b

end

module Test

46 47
  use array.Array
  use InvertingAnInjection
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 77 78 79 80 81 82 83 84 85 86

  let test () =
    let a = make 10 0 in
    a[0] <- 9;
    a[1] <- 3;
    a[2] <- 8;
    a[3] <- 2;
    a[4] <- 7;
    a[5] <- 4;
    a[6] <- 0;
    a[7] <- 1;
    a[8] <- 5;
    a[9] <- 6;
    assert {
      a[0] = 9 &&
      a[1] = 3 &&
      a[2] = 8 &&
      a[3] = 2 &&
      a[4] = 7 &&
      a[5] = 4 &&
      a[6] = 0 &&
      a[7] = 1 &&
      a[8] = 5 &&
      a[9] = 6
    };
    let b = inverting2 a 10 in
    assert {
      b[0] = 6 &&
      b[1] = 7 &&
      b[2] = 3 &&
      b[3] = 1 &&
      b[4] = 5 &&
      b[5] = 8 &&
      b[6] = 9 &&
      b[7] = 4 &&
      b[8] = 2 &&
      b[9] = 0
    }

87
end