The maximum segment sum problem: Find the maximum sum of any contiguous subarray. We include the empty subarray (with sum 0) as a valid segment. This is the obvious definition: Empty list maps to 0. Otherwise, we take the value of the segment starting at the current position, and take the maximum of that value with the recursive result of the tail. This is obviously correct, but has the runtime of O(n^2).

We have:

>>> mss [1, -2, 3, 4, -1, 2]  -- the segment: [3, 4, -1, 2]
8 :: SInteger
>>> mss [-2, -3, -1]          -- empty segment
0 :: SInteger
>>> mss [1, 2, 3]             -- the whole list
6 :: SInteger

Maximum sum of segments starting at the beginning of the given list. This is 0 if the empty segment is best, or positive if a non-empty prefix exists.

We have:

>>> mssBegin [1, -2, 3, 4, -1, 2]  -- the segment: [1, -2, 3, 4, -1, 2]
7 :: SInteger
>>> mssBegin [-2, -3, -1]          -- empty segment
0 :: SInteger
>>> mssBegin [1, 2, 3]             -- the whole list
6 :: SInteger

Kadane algorithm: We call the helper with the values of maximum value ending at the beginning and the list, and recurse.

>>> kadane [1, -2, 3, 4, -1, 2]  -- the segment: [3, 4, -1, 2]
8 :: SInteger
>>> kadane [-2, -3, -1]          -- empty segment
0 :: SInteger
>>> kadane [1, 2, 3]             -- the whole list
6 :: SInteger

Helper for Kadane's algorithm. Along with the list, we keep track of the maximum-value ending at the beginning of the list argument, and the maximum value sofar.

The key insight is that we need a generalized invariant that characterizes kadaneHelper for arbitrary accumulator values, not just the initial (0, 0).

The invariant states: for kadaneHelper xs meh msf where:

• meh (max-ending-here) is the maximum sum of a segment ending at the boundary
• msf (max-so-far) is the best segment sum seen in the already-processed prefix
• Preconditions: meh >= 0 and msf >= meh

  kadaneHelper xs meh msf == msf smax mss xs smax (meh + mssBegin xs)

This captures that the result is the maximum of:

• msf - the best segment entirely in the already-processed prefix
• mss xs - the best segment entirely in the remaining suffix
• meh + mssBegin xs - the best segment crossing the boundary

>>> runTPWith cvc5 correctness
Inductive lemma: kadaneHelperInvariant
  Step: Base                            Q.E.D.
  Step: 1                               Q.E.D.
  Step: 2                               Q.E.D.
  Result:                               Q.E.D.
Lemma: correctness
  Step: 1                               Q.E.D.
  Step: 2                               Q.E.D.
  Step: 3                               Q.E.D.
  Step: 4                               Q.E.D.
  Result:                               Q.E.D.
[Proven] correctness :: Ɐxs ∷ [Integer] → Bool