## FoVeOOS'11 Competition: challenge 3 in Why3

Auteurs: Jean-Christophe Filliâtre

Catégories: Array Data Structure

Outils: Why3

Références: The COST FoVeOOS'11 Competition

see also the index (by topic, by tool, by reference, by year)

```(* FoVeOOS 2011 verification competition
http://foveoos2011.cost-ic0701.org/verification-competition

Challenge 3
*)

module TwoEqualElements

use int.Int
use ref.Refint
use array.Array

predicate appear_twice (a: array int) (v: int) (u: int) =
exists i: int. 0 <= i < u /\ a[i] = v /\
exists j: int. 0 <= j < u /\ j <> i /\ a[j] = v

let two_equal_elements (a: array int) (n: int) : (v1:int, v2:int)
requires { length a = n+2 /\ n >= 2 }
requires { forall i: int. 0 <= i < length a -> 0 <= a[i] < n }
requires {
exists v1: int. appear_twice a v1 (n+2) /\
exists v2: int. appear_twice a v2 (n+2) /\ v2 <> v1 }
ensures  {
appear_twice a v1 (n+2) /\ appear_twice a v2 (n+2) /\ v1 <> v2 }
= let deja_vu = make n False in
let v1 = ref (-1) in
let v2 = ref (-1) in
for i = 0 to n+1 do
invariant { !v1 = -1 -> !v2 = -1 }
invariant { !v1 <> -1 -> appear_twice a !v1 i }
invariant { !v2 <> -1 -> appear_twice a !v2 i /\ !v2 <> !v1 }
invariant { forall v: int. 0 <= v < n ->
if deja_vu[v]=True then exists j: int. 0 <= j < i /\ a[j] = v
else forall j: int. 0 <= j < i -> a[j] <> v }
invariant { !v1 = -1 ->
forall v: int. 0 <= v < n -> not (appear_twice a v i) }
invariant { !v2 = -1 -> forall v: int. 0 <= v < n -> v <> !v1 ->
not (appear_twice a v i) }
let v = a[i] in
if deja_vu[v] then begin
if !v1 = -1 then v1 := v
else if !v2 = -1 && v <> !v1 then v2 := v
end else
deja_vu[v] <- True
done;
(!v1, !v2)

end
```