## Inverting an Injection, in Why3

Inverting an injective array, in Why3

Authors: Jean-Christophe Filliâtre

Topics: Array Data Structure / Permutation

Tools: Why3

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
```

# Why3 Proof Results for Project "vstte10_inverting"

## Theory "vstte10_inverting.InvertingAnInjection": fully verified

 Obligations Alt-Ergo 2.0.0 CVC3 2.4.1 CVC4 1.5 Coq 8.11.2 Z3 4.6.0 VC for inverting --- --- --- --- --- split_goal_right loop invariant init 0.01 --- --- --- --- index in array bounds 0.01 --- --- --- --- index in array bounds 0.02 --- --- --- --- loop invariant preservation --- 0.00 --- --- --- postcondition --- --- --- 0.31 --- postcondition 0.00 --- --- --- --- VC for inverting2 --- --- --- --- --- split_goal_right array creation size 0.01 --- --- --- --- loop invariant init 0.01 --- --- --- --- index in array bounds 0.02 --- --- --- --- index in array bounds 0.00 --- --- --- --- loop invariant preservation 0.01 --- --- --- --- postcondition --- --- --- --- --- split_goal_right VC for inverting2 0.00 --- --- --- --- VC for inverting2 --- --- --- 0.34 --- VC for inverting2 0.01 0.01 0.01 --- 0.00 out of loop bounds 0.00 --- --- --- ---

## Theory "vstte10_inverting.Test": fully verified

 Obligations Alt-Ergo 2.0.0 VC for test --- split_goal_right array creation size 0.01 index in array bounds 0.01 index in array bounds 0.01 index in array bounds 0.00 index in array bounds 0.01 index in array bounds 0.01 index in array bounds 0.02 index in array bounds 0.01 index in array bounds 0.01 index in array bounds 0.01 index in array bounds 0.01 assertion 0.04 precondition 0.13 assertion 0.39