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 int.Int
  use 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) : unit
    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. 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) : array int
    requires { n = length a /\ injective a n /\ range a n }
    ensures  { length result = n /\ injective result n /\
               forall i. 0 <= i < n -> result[a[i]] = i }
  = let b = make n 0 in
    for i = 0 to n - 1 do
      invariant { forall j. 0 <= j < i -> b[a[j]] = j }
      b[a[i]] <- i
    done;
    b

end

module Test

  use array.Array
  use 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

ObligationsAlt-Ergo 2.0.0CVC3 2.4.1CVC4 1.5Coq 8.11.2Z3 4.6.0
VC for inverting---------------
split_goal_right
loop invariant init0.01------------
index in array bounds0.02------------
index in array bounds0.01------------
loop invariant preservation---0.00---------
postcondition---------0.31---
postcondition0.00------------
VC for inverting2---------------
split_goal_right
array creation size0.01------------
loop invariant init0.01------------
index in array bounds0.00------------
index in array bounds0.02------------
loop invariant preservation0.01------------
postcondition---------------
split_goal_right
VC for inverting20.00------------
VC for inverting2---------0.34---
VC for inverting20.010.010.01---0.00
out of loop bounds0.00------------

Theory "vstte10_inverting.Test": fully verified

ObligationsAlt-Ergo 2.0.0
VC for test---
split_goal_right
array creation size0.01
index in array bounds0.01
index in array bounds0.01
index in array bounds0.00
index in array bounds0.01
index in array bounds0.01
index in array bounds0.02
index in array bounds0.01
index in array bounds0.01
index in array bounds0.01
index in array bounds0.01
assertion0.04
precondition0.13
assertion0.39