/* 
 * checked Sep 2023 with command
 *      frama-c -pp-annot -wp -wp-rte -wp-model Typed Kadane.c
 * using frama-c 27.1 (Cobalt)
 * and   Alt-Ergo 2.4.3
 */

#include <limits.h>
//#define INT_MIN       0x80000000



/*@
// compute a[p]+...+a[q]
logic integer sum(integer p,integer q,int *a) =
    ( q < p
    ? 0
    : q == p 
    ? a[p]
    : sum(p,q-1,a) + a[q]
    );
*/



/*@
assigns \nothing;
ensures e1: a <= \result && b <= \result && (\result == a || \result == b);
*/
int max(
    int a,
    int b)
{
    if (a < b)
        return b;
    else
        return a;
}



///// Empty subarrays admitted ///////////////////////////////////////////////////////////////////////////////////////////
/*@
requires r1: 0 <= n;
requires r2: \valid(a + (0..n-1));
assigns      \nothing;
ensures  e1: \forall integer p,q; 0 <= p <= n && -1 <= q <= n-1 ==> sum(p,q,a) <= \result;
ensures  e2: \exists integer p,q; 0 <= p <= n && -1 <= q <= n-1 &&  sum(p,q,a) == \result;
*/
int mss_empty(
    int n,
    const int a[n])
{
    int best = 0;
    int cur = 0;
    int j;

    /*@ 
    loop assigns j, cur, best;
    loop invariant i1: \forall integer p;   0 <= p <=j                   ==> sum(p,j-1,a) <= cur;
    loop invariant i2: \exists integer p;   0 <= p <=j                   &&  sum(p,j-1,a) == cur;
    loop invariant i3: \forall integer p,q; 0 <= p <=j && -1 <= q <= j-1 ==> sum(p,q  ,a) <= best;
    loop invariant i4: \exists integer p,q; 0 <= p <=j && -1 <= q <= j-1 &&  sum(p,q  ,a) == best;
    loop invariant i5: 0 <= j <= n;
    loop invariant i6: 0 <= cur <= best;
    loop variant n-j;
    */
    for (j=0; j<n; ++j) {
        //@ assert a1: sum(j+1,j,a) == 0;
        cur = max(0,cur+a[j]);
        best = max(best,cur);
    }   
    return best;
}



///// No empty subarrays admitted ////////////////////////////////////////////////////////////////////////////////////////
/*@
requires r1: 0 < n;
requires r2: \valid(a + (0..n-1));
assigns      \nothing;
ensures  e1: \forall integer p,q; 0 <= p <= q <= n-1 ==> sum(p,q,a) <= \result;
ensures  e2: \exists integer p,q; 0 <= p <= q <= n-1 &&  sum(p,q,a) == \result;
*/
int mss_nonempty(
    int n,
    const int a[n])
{
    int best = INT_MIN;
    int cur = 0;
    int j;

    /*@ 
    loop assigns j, cur, best;
    loop invariant i1: (\forall integer p;   0 <= p      <= j-1 ==> sum(p,j-1,a) <= cur ) || ( j == 0 && cur  == 0);
    loop invariant i2: (\exists integer p;   0 <= p      <= j-1 &&  sum(p,j-1,a) == cur ) || ( j == 0 && cur  == 0);
    loop invariant i3: (\forall integer p,q; 0 <= p <= q <= j-1 ==> sum(p,q  ,a) <= best) || ( j == 0 && best == INT_MIN);
    loop invariant i4: (\exists integer p,q; 0 <= p <= q <= j-1 &&  sum(p,q  ,a) == best) || ( j == 0 && best == INT_MIN);
    loop invariant i5: 0 <= j <= n;
    loop variant n-j;
    */
    for (j=0; j<n; ++j) {
        //@ assert a1: a[j] == sum(j,j,a);
        cur = max(a[j],cur+a[j]);
        best = max(best,cur);
    }
    return best;
}