/*
 * Run With java -ea FindMax
 */

class FindMax {

    /** Return the maximum number in non-empty array v */
    public static int findMax(int v[]) {
        int max = Integer.MIN_VALUE;

        // Precondition: v[] is not empty
        assert v.length > 0 : "v[] is empty";
        // Precondition: max <= v[i] for every i
        for (int i = 0; i < v.length; i++)
            assert max <= v[i] : "Found value < MIN_VALUE";

        // Locate the real maximum value
        for (int i = 0; i < v.length; i++)
            if (v[i] > max)
                max = v[i];

        // Postcondition: max >= v[i] for every i
        for (int i = 0; i < v.length; i++)
            assert max >= v[i] : "Found value > max";
        return max;
    }

    // Test harness
    public static void main(String argv[]) {
        int t[] = new int[5];

        t[0] = 4;
        t[1] = -4;
        t[2] = 145;
        t[3] = 0;
        t[4] = Integer.MIN_VALUE;
        System.out.println("Max value is " + findMax(t));
    }
}