<html><head><meta name="color-scheme" content="light dark"></head><body><pre style="word-wrap: break-word; white-space: pre-wrap;">
// Algoritmi per ordinare un vettore.
//
// Dato un vettore { a[0], .. , a[n-1] }, si richiede di
// calcolarne una permutazione { b[0], .. , b[n-1] } tale che
// b[0] &lt;= b[1] &lt;= b[2] ... &lt;= b[n-1].

// 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 Esempio15 {
	
	// *********************
	// ** Selection Sort
	//
	// Idea: trova il minimo tra a[1]..a[n] e scambialo con a[1].
	// Poi trova il minimo tra a[2]..a[n] e scambialo con a[2].
	// Etc.
	//
	// ComplessitÃ&nbsp;: n+(n-1)+(n-2)+...+1 = O(n^2)
	
	// Postcondizione: vettore ordinato
	//@ ensures (\forall int k ; 0&lt;=k &amp;&amp; k &lt; a.length ; (\forall int l ; k&lt;=l &amp;&amp; l &lt; a.length ; a[k]&lt;=a[l])) ;
	static void selectionSort(int[] a) {
		// Invariante: ogni elemento da 0 fino a i Ã¨ minore di tutto quello che lo segue nell'array 
		//@ loop_invariant 0&lt;=i &amp;&amp; i&lt;=a.length ;
		//@ loop_invariant (\forall int k ; 0&lt;=k &amp;&amp; k &lt; i ; (\forall int l ; k&lt;=l &amp;&amp; l &lt; a.length ; a[k]&lt;=a[l])) ;
		for (int i=0 ; i&lt;a.length ; i++) {
			int minPos = i;
			// Invariante: a[minPos] Ã¨ il minimo in a[i]..a[j] (escluso)
			//@ loop_invariant i&lt;j &amp;&amp; j&lt;=a.length ;
			//@ loop_invariant i&lt;=minPos &amp;&amp; minPos &lt; a.length ;
			//@ loop_invariant (\forall int k ; i&lt;=k &amp;&amp; k &lt; j ; a[minPos]&lt;=a[k]) ;
			for (int j=i+1 ; j&lt;a.length ; j++)
				if (a[j] &lt; a[minPos])
					minPos = j;
			// Scambia
			int tmp = a[i];
			a[i] = a[minPos];
			a[minPos] = tmp;
		}
	}

	// *********************
	// ** Merge Sort
	//
	// Idea:
	// Se il vettore Ã¨ di 0 o 1 elementi Ã¨ giÃ&nbsp; ordinato. 
	// Altrimenti, separa gli elementi in due parti uguali (tranne al piÃ¹ un elemento).
	// Ordina le due metÃ&nbsp; ricorsivamente.
	// Fondi le due metÃ&nbsp; in un unico vettore preservando l'ordinamento.
	//
	// ComplessitÃ&nbsp;:
	// Dobbiamo fare: separazione, 2 chiamate ricorsive, fusione
	// Quindi T(n) = costo_separazione(n) + 2*T(n/2) + costo_fusione(n)
	// Vedremo che la separazione e la fusione costano entrambe O(n).
	// Supponiamo che il costo totale di separazione+fusione sia &lt;= k*n
    // Quindi T(n) &lt;= k*n + 2*T(n/2)
	// Quindi T(n) &lt;= k*n + 2*( k*n/2 + 2*T(n/4) )
	//             &lt;= k*n + k*n + 4*T(n/4)	
	// Quindi T(n) &lt;= k*n + k*n + k*n + 8*T(n/8)
	// ...
	// Quindi T(n) &lt;= k*n + k*n + k*n + ... 
	// Sopra dopo log_2(n) addendi l'argomento di T(n/...) diventa &lt;=1 e quindi siamo al caso base che costa O(1)
	// Conclusione: T(n) &lt;= k*n*log(n) e la complessitÃ&nbsp; Ã¨ quindi O(n*log(n)).
	
	
	// ** Procedura merge
	// Fonde due vettori ordinati in uno solo.
	// Idea:
	// Guarda quale dei due vettori inizia con l'elemento piÃ¹ piccolo.
	// Sposta quell'elemento in un terzo vettore, togliendolo dal vettore originale.
	// Ripeti fino a quando i vettori non sono entrambi vuoti.
	// Alla fine, il terzo vettore contiene la fusione ordinata dei primi due.
	
	// Precondizione: vettori ordinati
	//@ requires (\forall int k ; 0&lt;=k &amp;&amp; k &lt; a.length ; (\forall int l ; k&lt;=l &amp;&amp; l &lt; a.length ; a[k]&lt;=a[l])) ;
	//@ requires (\forall int k ; 0&lt;=k &amp;&amp; k &lt; b.length ; (\forall int l ; k&lt;=l &amp;&amp; l &lt; b.length ; b[k]&lt;=b[l])) ;
	// Postcondizione: vettore ordinato (di lunghezza pari alla somma degli input)
	//@ ensures  (\forall int k ; 0&lt;=k &amp;&amp; k &lt; \result.length ; (\forall int l ; k&lt;=l &amp;&amp; l &lt; \result.length ; \result[k]&lt;=\result[l])) ;
	//@ ensures \result.length == a.length + b.length ;
	static int[] merge(int[] a, int[] b) {
		int[] res = new int[a.length + b.length];
		int ia=0, ib=0, ires=0 ;
		// Invariante: la parte finale dei due vettori a e b e la parte finale del vettore risultato res sono ordinati
		//@ loop_invariant ires == ia+ib ;
		//@ loop_invariant 0&lt;=ia &amp;&amp; ia&lt;=a.length ;
		//@ loop_invariant 0&lt;=ib &amp;&amp; ib&lt;=b.length ;
		//@ loop_invariant (\forall int k ; 0&lt;=k &amp;&amp; k &lt; ires ; (\forall int l ; k&lt;=l &amp;&amp; l &lt; ires ; res[k]&lt;=res[l])) ;
		//@ loop_invariant (\forall int k ; 0&lt;=k &amp;&amp; k &lt; ires ; (\forall int l ; ia&lt;=l &amp;&amp; l &lt; a.length ; res[k]&lt;=a[l])) ;
		//@ loop_invariant (\forall int k ; 0&lt;=k &amp;&amp; k &lt; ires ; (\forall int l ; ib&lt;=l &amp;&amp; l &lt; b.length ; res[k]&lt;=b[l])) ;
		while (ia&lt;a.length || ib&lt;b.length) {
			if (ia&gt;=a.length) {
				res[ires] = b[ib];
				ires++; ib++;
			} else if (ib&gt;=b.length) {
				res[ires] = a[ia];
				ires++; ia++;
			} else if (a[ia] &lt;= b[ib]) {
				res[ires] = a[ia];
				ires++; ia++;
			} else {
				res[ires] = b[ib];
				ires++; ib++;
			}
		}
		//@ assert ires == res.length ;
		return res;
	}
	
	// Postcondizione: vettore ordinato (della stessa lunghezza degli input)
	//@ ensures a.length == \result.length ;
	//@ ensures (\forall int k ; 0&lt;=k &amp;&amp; k &lt; \result.length ; (\forall int l ; k&lt;=l &amp;&amp; l &lt; \result.length ; \result[k]&lt;=\result[l])) ;
	static int[] mergeSort(int[] a) {
		if (a.length &lt;= 1)
			return a;

		int half = a.length / 2;
		int i=0;
		
		int[] fst = new int[half];
		//@ loop_invariant 0&lt;=i &amp;&amp; i&lt;=half ;
		for ( ; i&lt;half ; i++)
			fst[i]=a[i];
		fst = mergeSort(fst);
		
		int[] snd = new int[a.length - half];
		//@ loop_invariant half&lt;=i &amp;&amp; i&lt;=a.length ;
		for ( ; i&lt;a.length ; i++)
			snd[i-half]=a[i];
		snd = mergeSort(snd);
		
		return merge(fst,snd);
	}
		
	// ***********************************
	// *** Nota conclusiva
	//
	// Nelle specifiche di sopra (pre/post-condizioni) non abbiamo mai richiesto che
	// l'output sia una permutazione dell'input. Questo Ã¨ stato fatto per semplicitÃ&nbsp;
	// ma ovviamente Ã¨ una proprietÃ&nbsp; fondamentale di ogni algoritmo di ordinamento!
	// Ãˆ facile verificare che effettivamente valga. Il selection sort si limita a
	// scambiare elementi (e quindi l'output Ã¨ una permutazione). Il merge sort
	// si limita a separare e rifondere, e questo non elimina nessun elemento dai
	// vettori, nÃ© ne aggiunge di nuovi.
	
	
	
    public static void stampaArray(int[] a) {
    	int n=0;
    	System.out.print("{");
    	//@loop_invariant 0&lt;=n &amp;&amp; n&lt;=a.length ;
    	for (n=0 ; n&lt;a.length ; n++) {
    		if (n&gt;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&lt;a.length ; n++) {
			a[n] = n*n - 6 * n + 4;
		}
		System.out.print("Vettore  : ");
		stampaArray(a);
		selectionSort(a);
		System.out.print("Ordinato : ");
		stampaArray(a);
		
		// Inizializzo a
		for (n=0 ; n&lt;a.length ; n++) {
			a[n] = n*n - 6 * n + 4;
		}
		System.out.print("Vettore  : ");
		stampaArray(a);
		a=mergeSort(a);
		System.out.print("Ordinato : ");
		stampaArray(a);
	}
				
}
</pre></body></html>