## 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,

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
```