## Inverting an Injection, in Why3

Inverting an injective array, in Why3

Auteurs: Jean-Christophe Filliâtre

Catégories: Array Data Structure / Permutation

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