[Imprint][Data Privacy Statement][E-Mail]

Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Specification kadane
enrich
   int-array-ops

with
   

   
   
   
   
   procedures maxSubArraySum# int-array :  : int  ;
   variables  a : int-array;
              size : nat;
              res : int;
              max_so_far : int;
              max_ending_here : int;
   
   

   

   

   

   declarations max-sub-array-sum
                : maxSubArraySum#(a; ; res)
                  {let size = # a, max_so_far = 0, max_ending_here = 0, n = 0
                   in {while n < size
                       do {/* kadane-correct
                              : invariant   0 ≤ max_ending_here ∧ max_ending_here ≤ max_so_far ∧ n ≤ size ∧ maximum-sum(subarray(a, 0, n), max_so_far)
                                          ∧ (∃ m. maximum-suffix-sum(subarray(a, 0, n), m, max_ending_here))
                              wfbound size - n; 
                           */; 
                           max_ending_here := max_ending_here + a[n]; 
                           if max_ending_here < 0
                           then max_ending_here := 0
                           else if max_so_far < max_ending_here then max_so_far := max_ending_here; 
                           n := n + 1}; 
                       res := max_so_far}
                  }
                ;
end enrich