Maximum Subarray Problem

Given an array of integers, compute the maximum sum found in any *contiguous* segment of the array.

See Jon Bentley's Programming Pearls, chapter 8.

use int.Int
use array.Array
use array.ArraySum

(*
      0     lo              cl    hi            i                   length a
     +-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+
   a | | | | | | | | | | | | | | | | | | | | | |?|?|?|?|?|?|?|?|?|?|
     +-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+
           |<----- maxsum ------>|
                           |<----- curmax ---->|
*)

let maximum_subarray (a: array int) : (s: int)
  ensures { forall l h. 0 <= l <= h <= length a -> sum a l h <= s }
  ensures { exists l h. 0 <= l <= h <= length a /\ sum a l h  = s }
=
  (* the maximum in a[0..i[ is a[lo..hi[ *)
  let ref maxsum = 0 in
  let ghost ref lo = 0 in
  let ghost ref hi = 0 in
  (* the maximum ending on i is a[cl..i[ *)
  let ref curmax = 0 in
  let ghost ref cl = 0 in
  for i = 0 to length a - 1 do
    invariant { forall l. 0 <= l  <= i -> sum a l  i <= curmax }
    invariant {           0 <= cl <= i /\ sum a cl i  = curmax }
    invariant { forall l h. 0 <= l  <= h  <= i -> sum a l  h  <= maxsum }
    invariant {             0 <= lo <= hi <= i /\ sum a lo hi  = maxsum }
    curmax <- curmax + a[i];
    if curmax < 0 then (
      curmax <- 0; cl <- i+1
    );
    if curmax > maxsum then (
      maxsum <- curmax; lo <- cl; hi <- i+1
    )
  done;
  return maxsum