Max.java
Max.java
—
Plain Text,
289 bytes
File contents
class Max {
//@ ensures (\forall int j; 0 <=j && j < a.length; a[j] <= \result);
static int max(int[] a) {
int m_index = 0;
for (int i = 1; i< a.length; i++) {
if (a[i] > a[m_index]) {
m_index = i;
}
}
return a[m_index];
}
}