## VerifyThis 2017: Maximum-sum submatrix

solution to VerifyThis 2017 challenge 2

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

**Catégories:** Matrices

**Outils:** Why3

**Références:** 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

Obligations | Alt-Ergo 2.3.3 | CVC4 1.5 | Z3 4.11.2 | ||

VC for maximum_submatrix | --- | --- | --- | ||

split_goal_right | |||||

array creation size | 0.00 | --- | --- | ||

loop invariant init | 0.01 | --- | --- | ||

loop invariant init | 0.00 | --- | --- | ||

loop invariant init | 0.01 | --- | --- | ||

loop invariant init | 0.00 | --- | --- | ||

precondition | 0.01 | --- | --- | ||

loop invariant init | 0.01 | --- | --- | ||

loop invariant init | 0.01 | --- | --- | ||

loop invariant init | 0.00 | --- | --- | ||

loop invariant init | --- | --- | 0.02 | ||

loop invariant init | 0.01 | --- | --- | ||

loop invariant init | 0.01 | --- | --- | ||

loop invariant init | 0.01 | --- | --- | ||

index in matrix bounds | 0.01 | --- | --- | ||

index in array bounds | 0.01 | --- | --- | ||

index in array bounds | 0.00 | --- | --- | ||

loop invariant preservation | 0.45 | --- | --- | ||

loop invariant preservation | 0.41 | --- | --- | ||

assertion | 1.27 | --- | --- | ||

assertion | --- | --- | --- | ||

split_goal_right | |||||

assertion | 2.17 | --- | --- | ||

VC for maximum_submatrix | 0.01 | --- | --- | ||

loop invariant preservation | 0.01 | --- | --- | ||

loop invariant preservation | 0.01 | --- | --- | ||

loop invariant preservation | 0.02 | --- | --- | ||

loop invariant preservation | --- | 0.05 | --- | ||

loop invariant preservation | 0.01 | --- | --- | ||

loop invariant preservation | 0.01 | --- | --- | ||

loop invariant preservation | 0.00 | --- | --- | ||

loop invariant preservation | 0.01 | --- | --- | ||

loop invariant preservation | --- | 0.05 | --- | ||

loop invariant preservation | 0.01 | --- | --- | ||

out of loop bounds | 0.01 | --- | --- | ||

loop invariant preservation | 0.01 | --- | --- | ||

loop invariant preservation | 0.01 | --- | --- | ||

loop invariant preservation | 0.01 | --- | --- | ||

loop invariant preservation | --- | 0.03 | 0.01 | ||

out of loop bounds | 0.00 | --- | --- | ||

postcondition | --- | --- | --- | ||

split_goal_right | |||||

VC for maximum_submatrix | 0.00 | --- | --- | ||

VC for maximum_submatrix | 0.01 | --- | --- | ||

VC for maximum_submatrix | 0.00 | --- | --- | ||

VC for maximum_submatrix | 0.01 | --- | --- | ||

VC for maximum_submatrix | 0.00 | --- | --- | ||

VC for maximum_submatrix | 0.01 | --- | --- | ||

VC for maximum_submatrix | 0.00 | --- | --- | ||

VC for maximum_submatrix | --- | --- | 0.04 | ||

out of loop bounds | 0.01 | --- | --- |