Wiki Agenda Contact Version française

Inverting an Injection, in Why3

Inverting an injective array, in Why3


Authors: Jean-Christophe Filliâtre

Topics: Array Data Structure / Permutation

Tools: Why3

References: The 1st Verified Software Competition / The VerifyThis Benchmarks

see also the index (by topic, by tool, by reference, by year)


(*
   VSTTE'10 competition http://www.macs.hw.ac.uk/vstte10/Competition.html
   Problem 2: inverting an injection

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

module InvertingAnInjection

  use import int.Int
  use import array.Array
  use map.MapInjection as M

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

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

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

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

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

  let inverting2 (a: array int) (n: int)
    requires { n = length a /\ injective a n /\ range a n }
    ensures { length result = n /\ injective result n /\
      forall i: int. 0 <= i < n -> result[a[i]] = i }
  = let b = make n 0 in
    for i = 0 to n - 1 do
      invariant { forall j: int. 0 <= j < i -> b[a[j]] = j }
      b[a[i]] <- i
    done;
    b

end

module Test

  use import array.Array
  use import InvertingAnInjection

  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
    }

end

download ZIP archive

Why3 Proof Results for Project "vstte10_inverting"

Theory "vstte10_inverting.InvertingAnInjection": fully verified in 1.88 s

ObligationsAlt-Ergo (0.99.1)CVC3 (2.4.1)CVC4 (1.4)Coq (8.4pl6)Z3 (4.3.2)
VC for inverting---------------
split_goal_wp
  1. postcondition0.00------------
2. loop invariant init0.01------------
3. index in array bounds0.01------------
4. type invariant0.01------------
5. index in array bounds0.02------------
6. loop invariant preservation---0.00---------
7. type invariant0.01------------
8. postcondition---------0.84---
VC for inverting2---------------
split_goal_wp
  1. array creation size0.01------------
2. postcondition---------------
split_goal_wp
  1. VC for inverting20.010.010.01---0.00
2. VC for inverting2---------------
inline_goal
  1. VC for inverting20.01---0.01---0.01
3. VC for inverting20.00------------
3. loop invariant init0.01------------
4. index in array bounds0.02------------
5. type invariant0.01------------
6. index in array bounds0.00------------
7. loop invariant preservation0.01------------
8. type invariant0.00------------
9. postcondition---------------
split_goal_wp
  1. VC for inverting20.00------------
2. VC for inverting2---------0.85---
3. VC for inverting20.01------------

Theory "vstte10_inverting.Test": fully verified in 0.59 s

ObligationsAlt-Ergo (0.99.1)
VC for test---
split_goal_wp
  1. array creation size0.01
2. index in array bounds0.01
3. index in array bounds0.01
4. index in array bounds0.00
5. index in array bounds0.01
6. index in array bounds0.01
7. index in array bounds0.02
8. index in array bounds0.01
9. index in array bounds0.01
10. index in array bounds0.01
11. index in array bounds0.01
12. assertion0.08
13. precondition0.22
14. assertion0.18