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.7.1Z3 4.6.0
VC inverting---------------
split_goal_right
VC inverting.00.01------------
VC inverting.10.02------------
VC inverting.20.01------------
VC inverting.3---0.00---------
VC inverting.4---------0.34---
VC inverting.50.00------------
VC inverting2---------------
split_goal_right
VC inverting2.00.01------------
VC inverting2.10.01------------
VC inverting2.20.00------------
VC inverting2.30.02------------
VC inverting2.40.01------------
VC inverting2.5---------------
split_goal_right
VC inverting2.5.00.00------------
VC inverting2.5.1---------0.24---
VC inverting2.5.20.010.010.01---0.00
VC inverting2.60.00------------

Theory "vstte10_inverting.Test": fully verified

ObligationsAlt-Ergo 2.0.0
VC test---
split_goal_right
VC test.00.01
VC test.10.01
VC test.20.01
VC test.30.00
VC test.40.01
VC test.50.01
VC test.60.02
VC test.70.01
VC test.80.01
VC test.90.01
VC test.100.01
VC test.110.04
VC test.120.13
VC test.130.39