Wiki Agenda Contact Version française

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

ObligationsAlt-Ergo (0.99.1)CVC3 (2.4.1)
VC for two_way_sort------
split_goal_wp
  1. loop invariant init0.02---
2. loop invariant init0.02---
3. loop invariant init0.01---
4. loop invariant init0.02---
5. type invariant0.01---
6. index in array bounds0.02---
7. loop invariant preservation0.03---
8. loop invariant preservation0.02---
9. loop invariant preservation0.02---
10. loop invariant preservation0.02---
11. loop variant decrease0.02---
12. index in array bounds0.01---
13. loop invariant preservation0.02---
14. loop invariant preservation0.02---
15. loop invariant preservation0.02---
16. loop invariant preservation0.02---
17. loop variant decrease0.01---
18. precondition0.02---
19. loop invariant preservation0.04---
20. loop invariant preservation0.04---
21. loop invariant preservation------
split_goal_wp
  1. loop invariant preservation---0.94
22. loop invariant preservation0.10---
23. loop variant decrease0.02---
24. type invariant0.01---
25. postcondition0.02---
26. postcondition0.02---