Merge branch '863-forward-propagation-strategy-accept-optionnal-arguments' into ...
[why3.git] / examples / pancake_sorting.mlw
blobdce637b95434db573a0482171f14846b1c07c38f
2 (** {1 Pancake sorting}
4    See {h <a href="https://en.wikipedia.org/wiki/Pancake_sorting">Pancake
5    sorting</a>}.
7    Author: Jean-Christophe FilliĆ¢tre (CNRS)
8 *)
10 use mach.int.Int
11 use ref.Ref
12 use array.Array
13 use array.ArraySwap
14 use array.ArrayPermut
16 (** We choose to have the bottom of the stack of pancakes at `a[0]`.
17     So it means we sort the array in reverse order. *)
19 predicate sorted (a: array int) (hi: int) =
20   forall j1 j2. 0 <= j1 <= j2 < hi -> a[j1] >= a[j2]
22 (** Insert the spatula at index `i` and flip the pancakes *)
23 let flip (a: array int) (i: int)
24   requires { 0 <= i < length a }
25   ensures  { forall j. 0 <= j < i        -> a[j] = (old a)[j] }
26   ensures  { forall j. i <= j < length a -> a[j] = (old a)[length a -1-(j-i)] }
27   ensures  { permut_all (old a) a }
28 = let n = length a in
29   for k = 0 to (n - i) / 2 - 1 do
30     invariant { forall j. 0   <= j < i   -> a[j] = (old a)[j]     }
31     invariant { forall j. i   <= j < i+k -> a[j] = (old a)[n-1-(j-i)] }
32     invariant { forall j. i+k <= j < n-k -> a[j] = (old a)[j]     }
33     invariant { forall j. n-k <= j < n   -> a[j] = (old a)[n-1-(j-i)] }
34     invariant { permut_all (old a) a }
35     swap a (i + k) (n - 1 - k)
36   done
38 let pancake_sort (a: array int)
39   ensures { sorted a (length a) }
40   ensures { permut_all (old a) a }
41 = for i = 0 to length a - 2 do
42     invariant { sorted a i }
43     invariant { forall j1 j2. 0 <= j1 < i <= j2 < length a -> a[j1] >= a[j2] }
44     invariant { permut_all (old a) a }
45     (* 1. look for the maximum of a[i..] *)
46     let m = ref i in
47     for k = i + 1 to length a - 1 do
48       invariant { i <= !m < length a }
49       invariant { forall j. i <= j < k -> a[j] <= a[!m] }
50       if a[k] > a[!m] then m := k
51     done;
52     (* 2. then flip the pancakes to put it at index i *)
53     if !m = i then continue;
54     if !m < length a - 1 then flip a !m;
55     flip a i
56   done