## 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 <- 9;
a <- 3;
a <- 8;
a <- 2;
a <- 7;
a <- 4;
a <- 0;
a <- 1;
a <- 5;
a <- 6;
assert {
a = 9 &&
a = 3 &&
a = 8 &&
a = 2 &&
a = 7 &&
a = 4 &&
a = 0 &&
a = 1 &&
a = 5 &&
a = 6
};
let b = inverting2 a 10 in
assert {
b = 6 &&
b = 7 &&
b = 3 &&
b = 1 &&
b = 5 &&
b = 8 &&
b = 9 &&
b = 4 &&
b = 2 &&
b = 0
}

end
```