// *********** array minimum ************

// 'result' is a keyword which stands for the function's return value

// No side-effects via parameters permitted.  Only call-by-value.

@requires n >= 1
@ensures all(k, 0:n-1, result =< a[k]) &&
                  exists(k, 0:n-1, result = a[k])

int minimum(int[] a, int n) {
    @var i, m: int
    m = a[0];
    i = 1;
    @invariant
        1 =< i =< n &&
        all(k, 0:i-1, m =< a[k]) &&
        exists(k, 0:i-1, m = a[k])

    while (i < n) {
        if (a[i] < m)
            m = a[i];
        i = i+1;
    }
    return m;
}

// *********** main program ***********

@requires n >= 1
@ensures all(k, 0:n-1, min =< a[k]) && 
                 exists(k, 0:n-1, min = a[k])

@program
@var a: int[]
@var n, min: int

min = minimum(a, n);

@end
--