package esercizio7;

public class TE_Giugno_21 {
	//@ requires a != null;
	//@ requires a.length > 0;
	//@ ensures \result == (\exists int k; 0<=k && k<a.length; a[k] > b && a[k] % 2 == 0);
	boolean check(int[] a, int b) {
		boolean result = false;
		int i = 0;
		/*@ loop_invariant result == (\exists int j; 0<=j && j<i; a[j] > b && a[j] % 2 == 0) && i>=0 && i<=a.length; @*/
		while(i < a.length) {
			int x = a[i];
			if (x > b && x % 2 == 0) {
				result = true;
			}
			i++;
		}
		return result;
	}
}
