## Sort an array of Boolean values

Problem 1 of the second verified software competition.

The ZIP file below contains both the source code, the Why3 proof session file and the Coq script of the proof made in Coq. The Why3 source code is then displayed, followed by a summary of the proofs.

Auteurs: Jean-Christophe Filliâtre

Catégories: Array Data Structure

Outils: Why3

Références: The 2nd Verified Software Competition

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

```(* The 2nd Verified Software Competition (VSTTE 2012)

Problem 1:
Sorting an array of Boolean values, using swaps only *)

module TwoWaySort

use int.Int
use bool.Bool
use ref.Refint
use array.Array
use array.ArraySwap
use array.ArrayPermut

predicate le (x y: bool) = x = False \/ y = True

predicate sorted (a: array bool) =
forall i1 i2: int. 0 <= i1 <= i2 < a.length -> le a[i1] a[i2]

let two_way_sort (a: array bool)
ensures { sorted a }
ensures { permut_all (old a) a }
= let i = ref 0 in
let j = ref (length a - 1) in
while !i < !j do
invariant { 0 <= !i /\ !j < length a }
invariant { forall k: int. 0 <= k < !i -> a[k] = False }
invariant { forall k: int. !j < k < length a -> a[k] = True }
invariant { permut_all (old a) a }
variant   { !j - !i }
if not a[!i] then incr i
else if a[!j] then decr j
else begin swap a !i !j; incr i; decr j end
done

end
```

# Why3 Proof Results for Project "vstte12_two_way_sort"

## Theory "vstte12_two_way_sort.TwoWaySort": fully verified

 Obligations Alt-Ergo 2.1.0 VC for two_way_sort 0.09