## 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.

**Authors:** Jean-Christophe Filliâtre

**Topics:** Array Data Structure

**Tools:** Why3

**References:** The 2nd Verified Software Competition

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

download ZIP archive

(* The 2nd Verified Software Competition (VSTTE 2012) https://sites.google.com/site/vstte2012/compet Problem 1: Sorting an array of Boolean values, using swaps only *) module TwoWaySort use import int.Int use import bool.Bool use import ref.Refint use import array.Array use import array.ArraySwap use import 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 } = 'Init: 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 (at a 'Init) 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 in 1.52 s

Obligations | Alt-Ergo (0.99.1) | CVC3 (2.4.1) | ||

VC for two_way_sort | --- | --- | ||

split_goal_wp | ||||

1. loop invariant init | 0.02 | --- | ||

2. loop invariant init | 0.02 | --- | ||

3. loop invariant init | 0.01 | --- | ||

4. loop invariant init | 0.02 | --- | ||

5. type invariant | 0.01 | --- | ||

6. index in array bounds | 0.02 | --- | ||

7. loop invariant preservation | 0.03 | --- | ||

8. loop invariant preservation | 0.02 | --- | ||

9. loop invariant preservation | 0.02 | --- | ||

10. loop invariant preservation | 0.02 | --- | ||

11. loop variant decrease | 0.02 | --- | ||

12. index in array bounds | 0.01 | --- | ||

13. loop invariant preservation | 0.02 | --- | ||

14. loop invariant preservation | 0.02 | --- | ||

15. loop invariant preservation | 0.02 | --- | ||

16. loop invariant preservation | 0.02 | --- | ||

17. loop variant decrease | 0.01 | --- | ||

18. precondition | 0.02 | --- | ||

19. loop invariant preservation | 0.04 | --- | ||

20. loop invariant preservation | 0.04 | --- | ||

21. loop invariant preservation | --- | --- | ||

split_goal_wp | ||||

1. loop invariant preservation | --- | 0.94 | ||

22. loop invariant preservation | 0.10 | --- | ||

23. loop variant decrease | 0.02 | --- | ||

24. type invariant | 0.01 | --- | ||

25. postcondition | 0.02 | --- | ||

26. postcondition | 0.02 | --- |