// Ricerca del minimo

// 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 Esempio14 {
	
	// ********************************************
	// Ricerca del minimo
	// Cerca il valore minimo tra le componenti di un vettore a.
	// Restituisce l'indice dell'elemento minimo.
	// Complessità O(n)
	
	//@ requires a.length > 0 ;
	//@ ensures \result>=0 && \result<=a.length;
	//@ ensures (\forall int k ; 0<=k && k < a.length ; a[\result] <= a[k]) ;
    public static int ricercaMinimo(int[] a) {
        int n=0;
        int minPos=0;

        n=1;
        //@ loop_invariant 0<=n && n<=a.length ;
        //@ loop_invariant 0<=minPos && minPos<n ;
        //@ loop_invariant (\forall int k ; 0<=k && k < n ; a[minPos] <= a[k]) ; 
        while (n < a.length) {
        	if (a[n] < a[minPos]) {
        		minPos = n;
        	}
            n++;
        }
        return minPos;
    }


    
    
    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;
		
		// 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);
		
		n = ricercaMinimo(a);
		
		System.out.print("posizione = ");
		System.out.println(n);

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

}