// Ricerca lineare e ricerca binaria

// Questo esempio è parzialmente annotato con precondizioni/postcondizioni, 
// come se la sua correttezza fosse dimostrata con le triple di Hoare.
// Le annotazioni sono state aggiunte usando il linguaggio JML.
// In questo corso non vediamo JML, ma dovreste essere in grado di capire
// a livello intuitivo le annotazioni che sono state aggiunte.


public class Esempio13 {
	
	// ********************************************
	// Ricerca lineare
	// Cerca un valore y nelle componenti di un vettore a
	// Complessità O(n)
	
	//@ ensures \result>=0 && \result<=a.length;
    //@ ensures (\exists int l ; 0<=l && l<a.length ; a[l]==y) ==> \result < a.length && a[\result]==y ;
	//@ ensures !(\exists int l ; 0<=l && l<a.length ; a[l]==y) ==> \result == a.length ;
    public static int ricercaLineare(int[] a, int y) {
        int n=0;
        //@ loop_invariant 0<=n && n<=a.length ;
        //@ loop_invariant (\forall int l ; 0<=l && l<n ; a[l]!=y);
        while (n < a.length && a[n] != y) {
            n++;
        }
        return n;
    }

	// ********************************************
	// Ricerca Binaria
    // Cerca un valore y nelle componenti di un vettore **ordinato** a
	// Complessità O(log n)
    
    //@ requires (\forall int i ; 0<=i && i<a.length ; (\forall int j ; i<=j && j<a.length ; a[i]<=a[j]));
    //@ ensures \result>=0 && \result<=a.length;
    //@ ensures (\exists int l ; 0<=l && l<a.length ; a[l]==y) ==> \result < a.length && a[\result]==y ;
    //@ ensures !(\exists int l ; 0<=l && l<a.length ; a[l]==y) ==> \result >= a.length || a[\result]!=y ;
    public static int ricercaBinaria(int[] a, int y) {
        int from=0, to=a.length;
        int n=0,x=0;
        
        //@ loop_invariant 0 <= from && from <= to && to <= a.length;
        //@ loop_invariant (\exists int l ; 0<=l && l<a.length ; a[l]==y) ==> (\exists int l ; 0<=l && l<a.length ; a[l]==y && from<=l && l<=to );
        //@ decreasing to-from ;
        while (from < to) {
        	// Aggiungo queste stampe per osservare meglio il funzionamento
            System.out.print("from = ");
            System.out.print(from);
            System.out.print(", to = ");
            System.out.println(to);
            
            n = (from+to)/2;
            x = a[n];
            if (x < y) {
                    from = n+1;
            } else {
                    to = n;
            }
        }
        
        return from;
    }

    
    
    public static void stampaArray(int[] a) {
    	int n=0;
    	System.out.print("{");
    	//@loop_invariant 0<=n && n<=a.length ;
    	for (n=0 ; n<a.length ; n++) {
    		if (n>0) { 
    			System.out.print(",");
    		}
    		System.out.print(" ");
    		System.out.print(a[n]);
    	}
    	System.out.println(" }");
    }
    
	public static void main(String[] args) {
		int[] a;
		int n;
		int daCercare;
		
		// Alloco un vettore
		a = new int[10];
		
		// Inizializzo a
		for (n=0 ; n<a.length ; n++) {
			a[n] = n*n - 6 * n + 4;
		}
		stampaArray(a);
		
		daCercare = 11;
		n = ricercaLineare(a, daCercare);
		
		
		System.out.print("daCercare = ");
		System.out.println(daCercare);

		System.out.print("posizione = ");
		System.out.println(n);

		if (0<=n && n<a.length) {
			System.out.print("valore = ");
			System.out.println(a[n]);
		}

		// Ora proviamo la ricerca binaria.

		// Re-inizializzo a
		for (n=0 ; n<a.length ; n++) {
			a[n] = n*n + 6 * n + 4;
		}
		stampaArray(a);
		
		// Nota: devo essere sicuro che il vettore sia ordinato in modo crescente!
		daCercare = 76;
		n = ricercaBinaria(a, daCercare);
		
		System.out.print("daCercare = ");
		System.out.println(daCercare);

		System.out.print("posizione = ");
		System.out.println(n);

		if (0<=n && n<a.length) {
			System.out.print("valore = ");
			System.out.println(a[n]);
		}

		
	}

}