package esercizio7;

public class CheckFunction {
	
	// controlla se un array contiene un numero pari maggiore di b;
	//@ requires v!= null && v.length < 10;
	//@ ensures \result <==> (\exists int j; j>=0 && j<v.length; v[j]>b && v[j]%2==0);
	//@ code_bigint_math
	static boolean check(int[] v, int b) {
		boolean ris = false;
		/*@ loop_invariant i>=0 && i<= v.length && v!= null && 
		    (ris <==> (\exists int j; j>=0 && j<i; v[j]> b && v[j]%2==0));
		 */
		for(int i = 0; i < v.length; i++) {
			if (v[i] > b && v[i] % 2 == 0 && ! ris)
				ris = true;
		}
		return ris;
	}
	
	public static void main(String[] args) {
		int[] a1 = {};
		System.out.println(check(a1, 2) );
	}
}
