examples/vstte10_inverting.mlw

   1 (*
   2    VSTTE'10 competition http://www.macs.hw.ac.uk/vstte10/Competition.html
   3    Problem 2: inverting an injection
   4
   5    Author: Jean-Christophe Filliatre (CNRS)
   6    Tool:   Why3 (see http://why3.lri.fr/)
   7 *)
   8
   9 module InvertingAnInjection
  10
  11   use int.Int
  12   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     ensures  { length result = n /\ injective result n /\
  34                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       b[a[i]] <- i
  39     done;
  40     b
  41
  42 end
  43
  44 module Test
  45
  46   use array.Array
  47   use InvertingAnInjection
  48
  49   let test () =
  50     let a = make 10 0 in
  51     a[0] <- 9;
  52     a[1] <- 3;
  53     a[2] <- 8;
  54     a[3] <- 2;
  55     a[4] <- 7;
  56     a[5] <- 4;
  57     a[6] <- 0;
  58     a[7] <- 1;
  59     a[8] <- 5;
  60     a[9] <- 6;
  61     assert {
  62       a[0] = 9 &&
  63       a[1] = 3 &&
  64       a[2] = 8 &&
  65       a[3] = 2 &&
  66       a[4] = 7 &&
  67       a[5] = 4 &&
  68       a[6] = 0 &&
  69       a[7] = 1 &&
  70       a[8] = 5 &&
  71       a[9] = 6
  72     };
  73     let b = inverting2 a 10 in
  74     assert {
  75       b[0] = 6 &&
  76       b[1] = 7 &&
  77       b[2] = 3 &&
  78       b[3] = 1 &&
  79       b[4] = 5 &&
  80       b[5] = 8 &&
  81       b[6] = 9 &&
  82       b[7] = 4 &&
  83       b[8] = 2 &&
  84       b[9] = 0
  85     }
  86
  87 end