Wiki Agenda Contact Version française

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

ObligationsAlt-Ergo 2.0.0CVC3 2.4.1CVC4 1.5Z3 4.5.0
VC pair_insertion_sort------------
split_goal_right
VC pair_insertion_sort.00.00---------
VC pair_insertion_sort.10.00---------
VC pair_insertion_sort.20.01---------
VC pair_insertion_sort.30.00---------
VC pair_insertion_sort.40.00---------
VC pair_insertion_sort.50.00---------
VC pair_insertion_sort.60.00---------
VC pair_insertion_sort.70.01---------
VC pair_insertion_sort.80.00---------
VC pair_insertion_sort.90.00---------
VC pair_insertion_sort.100.30---------
VC pair_insertion_sort.110.00---------
VC pair_insertion_sort.120.00---------
VC pair_insertion_sort.130.00---------
VC pair_insertion_sort.140.01---------
VC pair_insertion_sort.150.05---------
VC pair_insertion_sort.160.36---------
VC pair_insertion_sort.170.00---------
VC pair_insertion_sort.180.00---------
VC pair_insertion_sort.190.22---------
VC pair_insertion_sort.200.16---------
VC pair_insertion_sort.210.24---------
VC pair_insertion_sort.220.14---------
VC pair_insertion_sort.23---0.10------
VC pair_insertion_sort.240.01---------
VC pair_insertion_sort.250.01---------
VC pair_insertion_sort.260.03---------
VC pair_insertion_sort.270.04---------
VC pair_insertion_sort.280.08---------
VC pair_insertion_sort.290.01---------
VC pair_insertion_sort.300.38---------
VC pair_insertion_sort.310.01---------
VC pair_insertion_sort.320.01---------
VC pair_insertion_sort.330.01---------
VC pair_insertion_sort.340.02---------
VC pair_insertion_sort.350.01---------
VC pair_insertion_sort.360.01---------
VC pair_insertion_sort.370.18---------
VC pair_insertion_sort.380.08---------
VC pair_insertion_sort.390.14---------
VC pair_insertion_sort.400.02---------
VC pair_insertion_sort.41------0.090.03
VC pair_insertion_sort.420.01---------
VC pair_insertion_sort.430.01---------
VC pair_insertion_sort.440.01---------
VC pair_insertion_sort.450.14---------
VC pair_insertion_sort.460.02---------
VC pair_insertion_sort.470.02---------
VC pair_insertion_sort.480.00---------
VC pair_insertion_sort.490.00---------
VC pair_insertion_sort.500.01---------
VC pair_insertion_sort.510.00---------
VC pair_insertion_sort.520.00---------
VC pair_insertion_sort.530.42---------
VC pair_insertion_sort.540.00---------
VC pair_insertion_sort.550.00---------
VC pair_insertion_sort.560.00---------
VC pair_insertion_sort.570.01---------
VC pair_insertion_sort.580.04---------
VC pair_insertion_sort.590.47---------
VC pair_insertion_sort.600.00---------
VC pair_insertion_sort.610.01---------
VC pair_insertion_sort.620.27---------
VC pair_insertion_sort.630.28---------
VC pair_insertion_sort.640.32---------
VC pair_insertion_sort.650.12---------
VC pair_insertion_sort.66---0.11------
VC pair_insertion_sort.670.01---------
VC pair_insertion_sort.680.00---------
VC pair_insertion_sort.690.04---------
VC pair_insertion_sort.700.02---------
VC pair_insertion_sort.710.20---------
VC pair_insertion_sort.720.02---------
VC pair_insertion_sort.730.44---------
VC pair_insertion_sort.740.01---------
VC pair_insertion_sort.750.00---------
VC pair_insertion_sort.760.01---------
VC pair_insertion_sort.770.02---------
VC pair_insertion_sort.780.01---------
VC pair_insertion_sort.790.01---------
VC pair_insertion_sort.800.16---------
VC pair_insertion_sort.810.10---------
VC pair_insertion_sort.820.16---------
VC pair_insertion_sort.830.04---------
VC pair_insertion_sort.842.13---------
VC pair_insertion_sort.850.01---------
VC pair_insertion_sort.860.00---------
VC pair_insertion_sort.870.01---------
VC pair_insertion_sort.880.25---------
VC pair_insertion_sort.890.02---------
VC pair_insertion_sort.900.00---------
VC pair_insertion_sort.910.00---------
VC pair_insertion_sort.920.00---------
VC pair_insertion_sort.930.00---------
VC pair_insertion_sort.940.00---------
VC pair_insertion_sort.950.00---------
VC pair_insertion_sort.960.17---------
VC pair_insertion_sort.970.00---------
VC pair_insertion_sort.980.00---------
VC pair_insertion_sort.990.00---------
VC pair_insertion_sort.1000.01---------
VC pair_insertion_sort.1010.01---------
VC pair_insertion_sort.1020.00---------
VC pair_insertion_sort.1030.05---------
VC pair_insertion_sort.1040.06---------
VC pair_insertion_sort.1050.10---------
VC pair_insertion_sort.1060.01---------
VC pair_insertion_sort.1070.84---------
VC pair_insertion_sort.1080.00---------
VC pair_insertion_sort.1090.07---------
VC pair_insertion_sort.1100.01---------
VC pair_insertion_sort.1110.00---------
VC pair_insertion_sort.1120.01---------