Maximum Subarray Problem

Below is the solution built during the lecture. You have to adapt it into a variant where *empty segments are not allowed*.

To do that, you have to

- add a precondition (with requires) to state that the array is not empty;

- update the specification (the two ensures);

- update the code;

- update the loop invariants.

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

(*
            lo              cl    hi            i
     +-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+
   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