Wiki Agenda Contact Version française

VerifyThis 2017: Maximum-sum submatrix

solution to VerifyThis 2017 challenge 2


Authors: Jean-Christophe Filliâtre

Topics: Matrices

Tools: Why3

References: VerifyThis @ ETAPS 2017

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


VerifyThis @ ETAPS 2017 competition Challenge 2: Maximum-sum submatrix

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

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

(* note: this is a 2D-version of maximum-sum subarray, for which several
   verified implementations can be found in maximum_subarray.mlw,
   including Kadane's linear algorithm *)

module Kadane2D

  use int.Int
  use ref.Refint
  use int.Sum
  use array.Array
  use matrix.Matrix

  (* maximum-sum subarray problem is assumed *)

  function array_sum (a: array int) (l h: int) : int
    = sum (fun i -> a[i]) l h

  val maximum_subarray (a: array int) : (s: int, lo: int, hi: int)
    ensures { 0 <= lo <= hi <= length a /\ s = array_sum a lo hi /\
              forall l h. 0 <= l <= h <= length a -> s >= array_sum a l h }

  (* sum of a submatrix *)

  function col (m: matrix int) (j i: int) : int = m.elts i j

  function matrix_sum (m: matrix int) (rl rh cl ch: int) : int
    = sum (fun j -> sum (col m j) rl rh) cl ch

  let maximum_submatrix (m: matrix int) :
      (s: int, rlo: int, rhi: int, clo: int, chi: int)
    ensures { (* this is a legal submatrix *)
              0 <= rlo <= rhi <= rows m /\
              0 <= clo <= chi <= columns m /\
              (* s is its sum *)
              s = matrix_sum m rlo rhi clo chi /\
              (* and it is maximal *)
              forall rl rh. 0 <= rl <= rh <= rows m ->
              forall cl ch. 0 <= cl <= ch <= columns m ->
              s >= matrix_sum m rl rh cl ch }
  = let a = Array.make m.columns 0 in
    let maxsum = ref 0 in
    let rlo = ref 0 in
    let rhi = ref 0 in
    let clo = ref 0 in
    let chi = ref 0 in
    for rl = 0 to rows m - 1 do
      invariant { 0 <= !rlo <= !rhi <= rows m }
      invariant { 0 <= !clo <= !chi <= columns m }
      invariant { !maxsum = matrix_sum m !rlo !rhi !clo !chi >= 0 }
      invariant { forall rl' rh. 0 <= rl' < rl -> rl' <= rh <= rows m ->
                  forall cl ch. 0 <= cl <= ch <= columns m ->
                  !maxsum >= matrix_sum m rl' rh cl ch }
      fill a 0 (columns m) 0;
      for rh = rl + 1 to rows m do
        invariant { 0 <= !rlo <= !rhi <= rows m }
        invariant { 0 <= !clo <= !chi <= columns m }
        invariant { !maxsum = matrix_sum m !rlo !rhi !clo !chi >= 0 }
        invariant { forall rl' rh'. 0 <= rl' <= rh' <= rows m ->
                    (rl' < rl \/ rl' = rl /\ rh' < rh) ->
                    forall cl ch. 0 <= cl <= ch <= columns m ->
                    !maxsum >= matrix_sum m rl' rh' cl ch }
        invariant { forall j. 0 <= j < columns m ->
                    a[j] = sum (col m j) rl (rh - 1) }
        (* update array a *)
        for c = 0 to columns m -1 do
          invariant { forall j. 0 <= j < c ->
                      a[j] = sum (col m j) rl rh }
          invariant { forall j. c <= j < columns m ->
                      a[j] = sum (col m j) rl (rh - 1) }
          a[c] <- a[c] + get m (rh - 1) c
        done;
        (* then use Kadane algorithme on array a *)
        let sum, lo, hi = maximum_subarray a in
        assert { sum = matrix_sum m rl rh lo hi };
        assert { forall cl ch. 0 <= cl <= ch <= columns m ->
                 sum >= matrix_sum m rl rh cl ch
                 by array_sum a cl ch = matrix_sum m rl rh cl ch };
        (* update the maximum if needed *)
        if sum > !maxsum then begin
          maxsum := sum;
          rlo := rl; rhi := rh;
          clo := lo; chi := hi
        end
      done;
    done;
    !maxsum, !rlo, !rhi, !clo, !chi

end

download ZIP archive

Why3 Proof Results for Project "verifythis_2017_maximum_sum_submatrix"

Theory "verifythis_2017_maximum_sum_submatrix.Kadane2D": fully verified

ObligationsAlt-Ergo 1.30CVC4 1.4Z3 4.4.0
VC maximum_submatrix---------
split_goal_right
VC maximum_submatrix.00.00------
VC maximum_submatrix.10.01------
VC maximum_submatrix.20.00------
VC maximum_submatrix.30.01------
VC maximum_submatrix.40.00------
VC maximum_submatrix.50.01------
VC maximum_submatrix.60.01------
VC maximum_submatrix.70.01------
VC maximum_submatrix.80.00------
VC maximum_submatrix.9------0.01
VC maximum_submatrix.100.01------
VC maximum_submatrix.110.01------
VC maximum_submatrix.120.01------
VC maximum_submatrix.130.01------
VC maximum_submatrix.140.01------
VC maximum_submatrix.150.00------
VC maximum_submatrix.160.01------
VC maximum_submatrix.170.04------
VC maximum_submatrix.181.76------
VC maximum_submatrix.19---------
split_goal_right
VC maximum_submatrix.19.00.34------
VC maximum_submatrix.19.10.01------
VC maximum_submatrix.200.01------
VC maximum_submatrix.210.01------
VC maximum_submatrix.220.02------
VC maximum_submatrix.23---0.05---
VC maximum_submatrix.240.01------
VC maximum_submatrix.250.01------
VC maximum_submatrix.260.00------
VC maximum_submatrix.270.01------
VC maximum_submatrix.28---0.05---
VC maximum_submatrix.290.01------
VC maximum_submatrix.300.01------
VC maximum_submatrix.310.01------
VC maximum_submatrix.320.01------
VC maximum_submatrix.330.01------
VC maximum_submatrix.34---0.030.01
VC maximum_submatrix.350.00------
VC maximum_submatrix.36---------
split_goal_right
VC maximum_submatrix.36.00.00------
VC maximum_submatrix.36.10.01------
VC maximum_submatrix.36.20.00------
VC maximum_submatrix.36.30.01------
VC maximum_submatrix.36.40.00------
VC maximum_submatrix.36.50.01------
VC maximum_submatrix.36.60.00------
VC maximum_submatrix.36.7------0.02
VC maximum_submatrix.370.01------