## VerifyThis 2017: Pair Insertion Sort

solution to VerifyThis 2017 challenge 1

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

**Topics:** Array Data Structure / Sorting Algorithms

**Tools:** Why3

**References:** VerifyThis @ ETAPS 2017

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

# VerifyThis @ ETAPS 2017 competition Challenge 1: Pair Insertion Sort

See https://formal.iti.kit.edu/ulbrich/verifythis2017/

Author: Jean-Christophe FilliĆ¢tre (CNRS)

module Challenge1 use int.Int use ref.Refint use array.Array use array.ArrayPermut let pair_insertion_sort (a: array int) ensures { forall k l. 0 <= k <= l < length a -> a[k] <= a[l] } ensures { permut_all (old a) a } = let i = ref 0 in (* i is running index (inc by 2 every iteration)*) while !i < length a - 1 do invariant { 0 <= !i <= length a } invariant { forall k l. 0 <= k <= l < !i -> a[k] <= a[l] } invariant { permut_all (old a) a } variant { length a - !i } let x = ref a[!i] in (* let x and y hold the next to elements in A *) let y = ref a[!i + 1] in if !x < !y then (* ensure that x is not smaller than y *) begin let tmp = !x in x := !y; y := tmp end (* swap x and y *) else begin label L in assert { exchange (a at L) a[(!i-1)+1 <- !y][(!i-1)+2 <- !x] ((!i-1)+1) ((!i-1)+2) } end; let j = ref (!i - 1) in (* j is the index used to find the insertion point *) while !j >= 0 && a[!j] > !x do (* find the insertion point for x *) invariant { -1 <= !j < !i } invariant { forall k l. 0 <= k <= l <= !j -> a[k] <= a[l] } invariant { forall k l. 0 <= k <= !j -> !j+2 < l < !i+2 -> a[k] <= a[l] } invariant { forall k l. !j+2 < k <= l < !i+2 -> a[k] <= a[l] } invariant { forall l. !j+2 < l < !i+2 -> !x < a[l] } invariant { permut_all (old a) a[!j+1 <- !y][!j+2 <- !x] } variant { !j } label L in a[!j + 2] <- a[!j]; (* shift existing content by 2 *) assert { exchange (a at L)[!j+2 <- !x] a[!j <- !x] !j (!j + 2) }; assert { exchange (a at L)[!j+1 <- !y][!j+2 <- !x] a[!j+1 <- !y][!j <- !x] !j (!j + 2) }; assert { exchange (a at L)[!j+1 <- !y][!j+2 <- a[!j]][!j <- !x] a[!j <- !y][!j+1 <- !x][!j+2 <- a[!j]] !j (!j + 1) }; j := !j - 1 done; a[!j + 2] <- !x; (* store x at its insertion place *) (* A[j+1] is an available space now *) while !j >= 0 && a[!j] > !y do (* #ind the insertion point for y *) invariant { -1 <= !j < !i } invariant { forall k l. 0 <= k <= l <= !j -> a[k] <= a[l] } invariant { forall k l. 0 <= k <= !j -> !j+1 < l < !i+2 -> a[k] <= a[l] } invariant { forall k l. !j+1 < k <= l < !i+2 -> a[k] <= a[l] } invariant { forall l. !j+1 < l < !i+2 -> !y <= a[l] } invariant { permut_all (old a) a[!j+1 <- !y] } variant { !j } label L in a[!j + 1] <- a[!j]; (* shift existing content by 1 *) assert { exchange (a at L)[!j+1 <- !y] a[!j <- !y] !j (!j + 1) }; j := !j - 1 done; a[!j + 1] <- !y; (* store y at its insertion place *) i := !i + 2 done; if !i = length a - 1 then begin (* if length(A) is odd, an extra *) let y = a[!i] in (* single insertion is needed for *) let j = ref (!i - 1) in (* the last element *) while !j >= 0 && a[!j] > y do invariant { -1 <= !j < !i } invariant { forall k l. 0 <= k <= l <= !j -> a[k] <= a[l] } invariant { forall k l. 0 <= k <= !j -> !j+1 < l < length a -> a[k] <= a[l] } invariant { forall k l. !j+1 < k <= l < length a -> a[k] <= a[l] } invariant { forall l. !j+1 < l < length a -> y < a[l] } invariant { permut_all (old a) a[!j+1 <- y] } variant { !j } label L in a[!j+1] <- a[!j]; assert { exchange (a at L)[!j+1 <- y] a[!j <- y] !j (!j + 1) }; j := !j - 1 done; a[!j + 1] <- y end end

download ZIP archive

# Why3 Proof Results for Project "verifythis_2017_pair_insertion_sort"

## Theory "verifythis_2017_pair_insertion_sort.Challenge1": fully verified

Obligations | Alt-Ergo 2.0.0 | CVC3 2.4.1 | CVC4 1.5 | Z3 4.5.0 | |

VC pair_insertion_sort | --- | --- | --- | --- | |

split_goal_right | |||||

VC pair_insertion_sort.0 | 0.00 | --- | --- | --- | |

VC pair_insertion_sort.1 | 0.00 | --- | --- | --- | |

VC pair_insertion_sort.2 | 0.01 | --- | --- | --- | |

VC pair_insertion_sort.3 | 0.00 | --- | --- | --- | |

VC pair_insertion_sort.4 | 0.00 | --- | --- | --- | |

VC pair_insertion_sort.5 | 0.00 | --- | --- | --- | |

VC pair_insertion_sort.6 | 0.00 | --- | --- | --- | |

VC pair_insertion_sort.7 | 0.01 | --- | --- | --- | |

VC pair_insertion_sort.8 | 0.00 | --- | --- | --- | |

VC pair_insertion_sort.9 | 0.00 | --- | --- | --- | |

VC pair_insertion_sort.10 | 0.30 | --- | --- | --- | |

VC pair_insertion_sort.11 | 0.00 | --- | --- | --- | |

VC pair_insertion_sort.12 | 0.00 | --- | --- | --- | |

VC pair_insertion_sort.13 | 0.00 | --- | --- | --- | |

VC pair_insertion_sort.14 | 0.01 | --- | --- | --- | |

VC pair_insertion_sort.15 | 0.05 | --- | --- | --- | |

VC pair_insertion_sort.16 | 0.36 | --- | --- | --- | |

VC pair_insertion_sort.17 | 0.00 | --- | --- | --- | |

VC pair_insertion_sort.18 | 0.00 | --- | --- | --- | |

VC pair_insertion_sort.19 | 0.22 | --- | --- | --- | |

VC pair_insertion_sort.20 | 0.16 | --- | --- | --- | |

VC pair_insertion_sort.21 | 0.24 | --- | --- | --- | |

VC pair_insertion_sort.22 | 0.14 | --- | --- | --- | |

VC pair_insertion_sort.23 | --- | 0.10 | --- | --- | |

VC pair_insertion_sort.24 | 0.01 | --- | --- | --- | |

VC pair_insertion_sort.25 | 0.01 | --- | --- | --- | |

VC pair_insertion_sort.26 | 0.03 | --- | --- | --- | |

VC pair_insertion_sort.27 | 0.04 | --- | --- | --- | |

VC pair_insertion_sort.28 | 0.08 | --- | --- | --- | |

VC pair_insertion_sort.29 | 0.01 | --- | --- | --- | |

VC pair_insertion_sort.30 | 0.38 | --- | --- | --- | |

VC pair_insertion_sort.31 | 0.01 | --- | --- | --- | |

VC pair_insertion_sort.32 | 0.01 | --- | --- | --- | |

VC pair_insertion_sort.33 | 0.01 | --- | --- | --- | |

VC pair_insertion_sort.34 | 0.02 | --- | --- | --- | |

VC pair_insertion_sort.35 | 0.01 | --- | --- | --- | |

VC pair_insertion_sort.36 | 0.01 | --- | --- | --- | |

VC pair_insertion_sort.37 | 0.18 | --- | --- | --- | |

VC pair_insertion_sort.38 | 0.08 | --- | --- | --- | |

VC pair_insertion_sort.39 | 0.14 | --- | --- | --- | |

VC pair_insertion_sort.40 | 0.02 | --- | --- | --- | |

VC pair_insertion_sort.41 | --- | --- | 0.09 | 0.03 | |

VC pair_insertion_sort.42 | 0.01 | --- | --- | --- | |

VC pair_insertion_sort.43 | 0.01 | --- | --- | --- | |

VC pair_insertion_sort.44 | 0.01 | --- | --- | --- | |

VC pair_insertion_sort.45 | 0.14 | --- | --- | --- | |

VC pair_insertion_sort.46 | 0.02 | --- | --- | --- | |

VC pair_insertion_sort.47 | 0.02 | --- | --- | --- | |

VC pair_insertion_sort.48 | 0.00 | --- | --- | --- | |

VC pair_insertion_sort.49 | 0.00 | --- | --- | --- | |

VC pair_insertion_sort.50 | 0.01 | --- | --- | --- | |

VC pair_insertion_sort.51 | 0.00 | --- | --- | --- | |

VC pair_insertion_sort.52 | 0.00 | --- | --- | --- | |

VC pair_insertion_sort.53 | 0.42 | --- | --- | --- | |

VC pair_insertion_sort.54 | 0.00 | --- | --- | --- | |

VC pair_insertion_sort.55 | 0.00 | --- | --- | --- | |

VC pair_insertion_sort.56 | 0.00 | --- | --- | --- | |

VC pair_insertion_sort.57 | 0.01 | --- | --- | --- | |

VC pair_insertion_sort.58 | 0.04 | --- | --- | --- | |

VC pair_insertion_sort.59 | 0.47 | --- | --- | --- | |

VC pair_insertion_sort.60 | 0.00 | --- | --- | --- | |

VC pair_insertion_sort.61 | 0.01 | --- | --- | --- | |

VC pair_insertion_sort.62 | 0.27 | --- | --- | --- | |

VC pair_insertion_sort.63 | 0.28 | --- | --- | --- | |

VC pair_insertion_sort.64 | 0.32 | --- | --- | --- | |

VC pair_insertion_sort.65 | 0.12 | --- | --- | --- | |

VC pair_insertion_sort.66 | --- | 0.11 | --- | --- | |

VC pair_insertion_sort.67 | 0.01 | --- | --- | --- | |

VC pair_insertion_sort.68 | 0.00 | --- | --- | --- | |

VC pair_insertion_sort.69 | 0.04 | --- | --- | --- | |

VC pair_insertion_sort.70 | 0.02 | --- | --- | --- | |

VC pair_insertion_sort.71 | 0.20 | --- | --- | --- | |

VC pair_insertion_sort.72 | 0.02 | --- | --- | --- | |

VC pair_insertion_sort.73 | 0.44 | --- | --- | --- | |

VC pair_insertion_sort.74 | 0.01 | --- | --- | --- | |

VC pair_insertion_sort.75 | 0.00 | --- | --- | --- | |

VC pair_insertion_sort.76 | 0.01 | --- | --- | --- | |

VC pair_insertion_sort.77 | 0.02 | --- | --- | --- | |

VC pair_insertion_sort.78 | 0.01 | --- | --- | --- | |

VC pair_insertion_sort.79 | 0.01 | --- | --- | --- | |

VC pair_insertion_sort.80 | 0.16 | --- | --- | --- | |

VC pair_insertion_sort.81 | 0.10 | --- | --- | --- | |

VC pair_insertion_sort.82 | 0.16 | --- | --- | --- | |

VC pair_insertion_sort.83 | 0.04 | --- | --- | --- | |

VC pair_insertion_sort.84 | 2.13 | --- | --- | --- | |

VC pair_insertion_sort.85 | 0.01 | --- | --- | --- | |

VC pair_insertion_sort.86 | 0.00 | --- | --- | --- | |

VC pair_insertion_sort.87 | 0.01 | --- | --- | --- | |

VC pair_insertion_sort.88 | 0.25 | --- | --- | --- | |

VC pair_insertion_sort.89 | 0.02 | --- | --- | --- | |

VC pair_insertion_sort.90 | 0.00 | --- | --- | --- | |

VC pair_insertion_sort.91 | 0.00 | --- | --- | --- | |

VC pair_insertion_sort.92 | 0.00 | --- | --- | --- | |

VC pair_insertion_sort.93 | 0.00 | --- | --- | --- | |

VC pair_insertion_sort.94 | 0.00 | --- | --- | --- | |

VC pair_insertion_sort.95 | 0.00 | --- | --- | --- | |

VC pair_insertion_sort.96 | 0.17 | --- | --- | --- | |

VC pair_insertion_sort.97 | 0.00 | --- | --- | --- | |

VC pair_insertion_sort.98 | 0.00 | --- | --- | --- | |

VC pair_insertion_sort.99 | 0.00 | --- | --- | --- | |

VC pair_insertion_sort.100 | 0.01 | --- | --- | --- | |

VC pair_insertion_sort.101 | 0.01 | --- | --- | --- | |

VC pair_insertion_sort.102 | 0.00 | --- | --- | --- | |

VC pair_insertion_sort.103 | 0.05 | --- | --- | --- | |

VC pair_insertion_sort.104 | 0.06 | --- | --- | --- | |

VC pair_insertion_sort.105 | 0.10 | --- | --- | --- | |

VC pair_insertion_sort.106 | 0.01 | --- | --- | --- | |

VC pair_insertion_sort.107 | 0.84 | --- | --- | --- | |

VC pair_insertion_sort.108 | 0.00 | --- | --- | --- | |

VC pair_insertion_sort.109 | 0.07 | --- | --- | --- | |

VC pair_insertion_sort.110 | 0.01 | --- | --- | --- | |

VC pair_insertion_sort.111 | 0.00 | --- | --- | --- | |

VC pair_insertion_sort.112 | 0.01 | --- | --- | --- |