verifythis_2017_maximum_sum_submatrix.mlw 3.48 KB
 Jean-Christophe Filliatre committed Apr 23, 2017 1 `````` `````` Jean-Christophe Filliatre committed May 18, 2017 2 ``````(** `````` Jean-Christophe Filliatre committed Apr 23, 2017 3 `````` `````` Jean-Christophe Filliatre committed May 18, 2017 4 5 6 7 8 9 ``````{1 VerifyThis @ ETAPS 2017 competition Challenge 2: Maximum-sum submatrix} See https://formal.iti.kit.edu/ulbrich/verifythis2017/ Author: Jean-Christophe Filliâtre (CNRS) `````` Jean-Christophe Filliatre committed Apr 23, 2017 10 11 ``````*) `````` Jean-Christophe Filliatre committed May 18, 2017 12 13 14 15 ``````(* 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 *) `````` Jean-Christophe Filliatre committed Apr 23, 2017 16 17 ``````module Kadane2D `````` Andrei Paskevich committed Jun 15, 2018 18 19 20 21 22 `````` use int.Int use ref.Refint use int.Sum use array.Array use matrix.Matrix `````` Jean-Christophe Filliatre committed Apr 23, 2017 23 24 25 `````` (* maximum-sum subarray problem is assumed *) `````` Andrei Paskevich committed Jun 15, 2018 26 `````` function array_sum (a: array int) (l h: int) : int `````` Jean-Christophe Filliatre committed Apr 23, 2017 27 28 `````` = sum (fun i -> a[i]) l h `````` Andrei Paskevich committed Jun 15, 2018 29 30 31 `````` 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 } `````` Jean-Christophe Filliatre committed Apr 23, 2017 32 33 34 35 36 37 38 39 `````` (* 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 `````` Andrei Paskevich committed Jun 07, 2018 40 41 42 `````` let maximum_submatrix (m: matrix int) : (s: int, rlo: int, rhi: int, clo: int, chi: int) ensures { (* this is a legal submatrix *) `````` Jean-Christophe Filliatre committed Apr 23, 2017 43 44 45 46 47 48 49 50 `````` 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 } `````` Andrei Paskevich committed Jun 15, 2018 51 `````` = let a = Array.make m.columns 0 in `````` Jean-Christophe Filliatre committed Apr 23, 2017 52 53 54 55 56 57 58 59 60 61 62 63 `````` 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 } `````` Andrei Paskevich committed Jun 15, 2018 64 `````` fill a 0 (columns m) 0; `````` Jean-Christophe Filliatre committed Apr 23, 2017 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 `````` 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; `````` Andrei Paskevich committed Jun 11, 2017 97 `````` !maxsum, !rlo, !rhi, !clo, !chi `````` Jean-Christophe Filliatre committed Apr 23, 2017 98 99 `````` end``````