Maximum subarray problem

Topics: Ghost code / Array Data Structure

Tools: Why3

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

```(* Maximum subarray problem

Given an array of integers, find the contiguous subarray with the
largest sum. Subarrays of length 0 are allowed (which means that an
array with negative values only has a maximal sum of 0).

Authors: Jean-Christophe FilliĆ¢tre (CNRS)
Guillaume Melquiond       (Inria)
Andrei Paskevich          (U-PSUD)
*)

module Spec
use int.Int
use export array.Array

use export array.ArraySum
(* provides [sum a l h] = the sum of a[l..h[ and suitable lemmas *)

(* s is no smaller than sums of subarrays a[l..h[ with 0 <= l < maxlo *)
predicate maxsublo (a: array int) (maxlo: int) (s: int) =
forall l h: int. 0 <= l < maxlo -> l <= h <= length a -> sum a l h <= s

(* s is no smaller than sums of subarrays of a *)
predicate maxsub (a: array int) (s: int) =
forall l h: int. 0 <= l <= h <= length a -> sum a l h <= s

end

(* In all codes below, reference ms stands for the maximal sum found so far
and ghost references lo and hi hold the bounds for this sum *)

(* Naive solution, in O(N^3) *)
module Algo1

use int.Int
use ref.Refint
use Spec

let maximum_subarray (a: array int) (ghost lo hi: ref int): int
ensures { 0 <= !lo <= !hi <= length a && result = sum a !lo !hi }
ensures { maxsub a result }
= lo := 0;
hi := 0;
let n = length a in
let ms = ref 0 in
for l = 0 to n-1 do
invariant { 0 <= !lo <= l && !lo <= !hi <= n && !ms = sum a !lo !hi }
invariant { maxsublo a l !ms }
for h = l to n do
invariant { 0 <= !lo <= l && !lo <= !hi <= n && !ms = sum a !lo !hi }
invariant { maxsublo a l !ms }
invariant { forall h': int. l <= h' < h -> sum a l h' <= !ms }
(* compute the sum of a[l..h[ *)
let s = ref 0 in
for i = l to h-1 do
invariant { !s = sum a l i }
invariant { 0 <= !lo <= l && !lo <= !hi <= n && !ms = sum a !lo !hi }
s += a[i]
done;
assert { !s = sum a l h };
if !s > !ms then begin ms := !s; lo := l; hi := h end
done
done;
!ms

end

(* Slightly less naive solution, in O(N^2)
Do not recompute the sum, simply update it *)

module Algo2

use int.Int
use ref.Refint
use Spec

let maximum_subarray (a: array int) (ghost lo hi: ref int): int
ensures { 0 <= !lo <= !hi <= length a && result = sum a !lo !hi }
ensures { maxsub a result }
= lo := 0;
hi := 0;
let n = length a in
let ms = ref 0 in
for l = 0 to n-1 do
invariant { 0 <= !lo <= l && !lo <= !hi <= n && 0 <= !ms = sum a !lo !hi }
invariant { maxsublo a l !ms }
let s = ref 0 in
for h = l+1 to n do
invariant
{ 0 <= !lo <= l && !lo <= !hi <= n && 0 <= !ms = sum a !lo !hi }
invariant { maxsublo a l !ms }
invariant { forall h': int. l <= h' < h -> sum a l h' <= !ms }
invariant { !s = sum a l (h-1) }
s += a[h-1]; (* update the sum *)
assert { !s = sum a l h };
if !s > !ms then begin ms := !s; lo := l; hi := h end
done
done;
!ms

end

(* Divide-and-conqueer solution, in O(N log N) *)

module Algo3

use int.Int
use ref.Refint
use int.ComputerDivision
use Spec

let rec maximum_subarray_rec (a: array int) (l h: int) (ghost lo hi: ref int)
: int
requires { 0 <= l <= h <= length a }
ensures  { l <= !lo <= !hi <= h && result = sum a !lo !hi }
ensures  { forall l' h': int. l <= l' <= h' <= h -> sum a l' h' <= result }
variant  { h - l }
= if h = l then begin
(* base case: no element at all *)
lo := l; hi := h; 0
end else begin
(* at least one element *)
let mid = l + div (h - l) 2 in
(* first consider all sums that include a[mid] *)
lo := mid; hi := mid;
let ms = ref 0 in
let s  = ref !ms in
for i = mid-1 downto l do
invariant { l <= !lo <= mid = !hi && !ms = sum a !lo !hi }
invariant { forall l': int. i < l' <= mid -> sum a l' mid <= !ms }
invariant { !s = sum a (i+1) mid }
s += a[i];
assert { !s = sum a i mid };
if !s > !ms then begin ms := !s; lo := i end
done;
assert { forall l': int. l <= l' <= mid ->
sum a l' mid <= sum a !lo mid };
s := !ms;
for i = mid to h-1 do
invariant { l <= !lo <= mid <= !hi <= h && !ms = sum a !lo !hi }
invariant { forall l' h': int. l <= l' <= mid <= h' <= i ->
sum a l' h' <= !ms }
invariant { !s = sum a !lo i }
s += a[i];
assert { !s = sum a !lo (i+1) };
assert { !s = sum a !lo mid + sum a mid (i+1) };
if !s > !ms then begin ms := !s; hi := (i+1) end
done;
(* then consider sums in a[l..mid[ and a[mid+1..h[, recursively *)
begin
let ghost lo' = ref 0 in
let ghost hi' = ref 0 in
let left = maximum_subarray_rec a l mid lo' hi' in
if left > !ms then begin ms := left; lo := !lo'; hi := !hi' end
end;
begin
let ghost lo' = ref 0 in
let ghost hi' = ref 0 in
let right = maximum_subarray_rec a (mid+1) h lo' hi' in
if right > !ms then begin ms := right; lo := !lo'; hi := !hi' end
end;
!ms
end

let maximum_subarray (a: array int) (ghost lo hi: ref int): int
ensures { 0 <= !lo <= !hi <= length a && result = sum a !lo !hi }
ensures { maxsub a result }
= maximum_subarray_rec a 0 (length a) lo hi

end

(* Optimal solution, in O(N)
Known as Kadane's algorithm *)

module Algo4

use int.Int
use ref.Refint
use Spec

let maximum_subarray (a: array int) (ghost lo hi: ref int): int
ensures { 0 <= !lo <= !hi <= length a && result = sum a !lo !hi }
ensures { maxsub a result }
= lo := 0;
hi := 0;
let n = length a in
let ms = ref 0 in
let ghost l = ref 0 in
let s = ref 0 in
for i = 0 to n-1 do
invariant { 0 <= !lo <= !hi <= i && 0 <= !ms = sum a !lo !hi }
invariant { forall l' h': int. 0 <= l' <= h' <= i -> sum a l' h' <= !ms }
invariant { 0 <= !l <= i && !s = sum a !l i }
invariant { forall l': int. 0 <= l' < i -> sum a l' i <= !s }
if !s < 0 then begin s := a[i]; l := i end else s += a[i];
if !s > !ms then begin ms := !s; lo := !l; hi := (i+1) end
done;
!ms

end

(* A slightly different variation of Kadane's algorithm *)

module Algo5

use int.Int
use ref.Refint
use export array.Array
use export array.ArraySum

(*
[| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | |]
......|###### maxsum #######|..............
............................. |## curmax ##
*)

let maximum_subarray (a: array int): int
ensures { forall l h: int. 0 <= l <= h <= length a -> sum a l h <= result }
ensures { exists l h: int. 0 <= l <= h <= length a /\ sum a l h  = result }
=
let maxsum = ref 0 in
let curmax = ref 0 in
let ghost lo = ref 0 in
let ghost hi = ref 0 in
let ghost cl = ref 0 in
for i = 0 to a.length - 1 do
invariant { forall l : int. 0 <= l <= i -> sum a l i <= !curmax }
invariant { 0 <= !cl <= i /\ sum a !cl i  = !curmax }
invariant { forall l h: int. 0 <= l <= h <= i -> sum a l h <= !maxsum }
invariant { 0 <= !lo <= !hi <= i /\ sum a !lo !hi = !maxsum }
curmax += a[i];
if !curmax < 0 then begin curmax := 0; cl := i+1 end;
if !curmax > !maxsum then begin maxsum := !curmax; lo := !cl; hi := i+1 end
done;
!maxsum

end

(* Kadane's algorithm with 63-bit integers

Interestingly, we only have to require all sums to be no greater
than max_int.  There is no need to require the sums to be no
smaller than min_int, since whenever the sum becomes negative it is
replaced by the next element. *)

module BoundedIntegers

use int.Int
use mach.int.Int63
use mach.int.Refint63
use seq.Seq
use mach.array.Array63
use int.Sum

function sum (a: array int63) (lo hi: int) : int =
Sum.sum (fun i -> (a[i] : int)) lo hi

let maximum_subarray (a: array int63) (ghost lo hi: ref int): int63
requires { [@no overflow] forall l h. 0 <= l <= h <= length a ->
sum a l h <= max_int }
ensures { 0 <= !lo <= !hi <= length a && result  = sum a !lo !hi }
ensures { forall l h. 0 <= l <= h <= length a -> result >= sum a !lo !hi }
= lo := 0;
hi := 0;
let n = length a in
let ms = ref zero in
let ghost l = ref 0 in
let s = ref zero in
let i = ref zero in
while !i < n do
invariant { 0 <= !lo <= !hi <= !i <= n && 0 <= !ms = sum a !lo !hi }
invariant { forall l' h': int. 0 <= l' <= h' <= !i -> sum a l' h' <= !ms }
invariant { 0 <= !l <= !i && !s = sum a !l !i }
invariant { forall l': int. 0 <= l' < !i -> sum a l' !i <= !s }
variant   { n - !i }
if !s < zero then begin s := a[!i]; l := to_int !i end
else begin assert { sum a !l (!i + 1) <= max_int }; s += a[!i] end;
if !s > !ms then begin
ms := !s; lo := !l; hi := to_int !i + 1 end;
incr i
done;
!ms

end
```

download ZIP archive