class EsempioArrayOfInt { /* AI: a != null AF: restituisce a[0]+...+a[a.length-1] */ static int somma(int[] a) { if (a==null) throw new IllegalArgumentException(); int s=0; // 0 <= i <= a.length AND s == a[0]+...+a[i-1] for (int i=0; i < a.length; i++) s=s+a[i]; return s; } /* AI: a != null AF: a[i] = e, per ogni i in {0,...,a.length} */ static void inizializza(int[] a, int e) { if (a==null) throw new IllegalArgumentException(); // 0 <= i <= a.length AND a[0]==...==a[i-1]==e for (int i=0; i < a.length; i++) a[i]=e; } static void main(String[] args) { int m = AConsoleReader.readInt("Digita il numero di elementi:"); int val = AConsoleReader.readInt("Digita il valore iniziale:"); int[] b = new int[m]; inizializza(b,val); AConsoleReader.printPrompt("La somma e:"+somma(b)); }
Dal confronto con l'esempio precedente dovrebbero emergere le differenze tra il trattamento di array di elementi di tipo "statico" (int, boolean, double, etc.) e array di (riferimenti ad) oggetti.
class EsempioArrayOfBigInteger { /* AI: a != null AF: restituisce la somma di a[0],...,[a.length-1] */ static BigInteger somma(BigInteger[] a) { if (a==null) throw new IllegalArgumentException(); BigInteger s = new BigInteger("0"); // 0 <= i <= a.length AND s contiene la somma di a[0],...,a[i-1] for (int i=0; i < a.length; i++) s=s.add(a[i]); return s; } /* AI: a != null AF: a[i] = e, per ogni i in {0,...,a.length} */ static void inizializza(BigInteger [] a, BigInteger e) { if (a==null) throw new IllegalArgumentException(); // 0 <= i <= a.length AND a[0]==...==a[i-1]==e for (int i=0; i < a.length; i++) a[i]=e; } static void main(String[] args) { int m = AConsoleReader.readInt("Digita il numero di elementi:"); String strVal = AConsoleReader.readLine("Digita il valore iniziale:"); BigInteger val = new BigInteger(strVal); BigInteger[] b = new BigInteger[m]; inizializza(b,val); AConsoleReader.printPrompt("La somma e:"+somma(b)); }
Prima versione. Nello scrivere una prima versione del metodo, cerchiamo di scrivere il metodo nel modo piu' "facile" possibile, cioe' in modo che la dimostrazione della sua correttezza non richieda ragionamenti sofisticati.
Partiamo quindi dall'osservazione che: un array e' palindromo se:
a[0]==a[a.length-1] AND a[1]==a[a.length-2] AND...AND a[a.length-1]==a[0]
e produciamo il seguente metodo.
/* AI: a != null AF: restituisce true se a e' palindromo, false altrimenti */ static boolean isPal(int[] a) { if (a==null) throw new IllegalArgumentException(); boolean r = false; int i=0; // 0 <= i <= a.length AND // r == (i==0 OR (a[0]==a[length-1] AND ... AND a[i-1]==a[a.length-i])) while (i < a.length) { if (a[i]!=a[a.length-1-i]) r=false; i++; } return r; }
Seconda versione.
Osserviamo che il programma precedente puo' essere migliorato:
e' sufficiente fermarsi a meta' dell'array. Quindi:
un array e' palindromo se:
a[0]==a[a.length-1] AND
a[1]==a[a.length-2] AND
...
AND a[a.length/2-1]==a[a.length-a.length/2]
e produciamo il seguente metodo.
/* AI: a != null AF: restituisce true se a e' palindromo, false altrimenti */ static boolean isPal(int[] a) { if (a==null) throw new IllegalArgumentException(); boolean r = false; int i=0; // 0 <= i <= a.length/2 AND // r == (i==0 OR (a[0]==a[length-1] AND ... AND a[i-1]==a[a.length-i])) while (i < a.length/2) { if (a[i]!=a[a.length-1-i]) r=false; i++; } return r; }
Terza versione. Osserviamo che il metodo precedente puo' ancora essere migliorato: una volta stabilito che a non e' palindromo e' posibile ritornare immediatamente false.
/* AI: a != null AF: restituisce true se a e' palindromo, false altrimenti */ static boolean isPal(int[] a) { if (a==null) throw new IllegalArgumentException(); int i=0; // 0 <= i <= a.length/2 AND // (i==0 OR (a[0]==a[length-1] AND ... AND a[i-1]==a[a.length-i])) while (i < a.length/2) { if (a[i]!=a[a.length-1-i]) return false; i++; } return true; }
Per eventuali chiarimenti rivolgersi ai docenti.
/* AI: a != null AF: restituisce il minimo i tale che a[i]==x, -1 altrimenti (se a[i]!=x per tutti gli i) */ static int sequentialSearch(int[] a, int x)
/* AI: a != null, n>=0 AF: restituisce true se l'elemento 'e' occorre in 'a' esattamente n volte, false altrimenti */ static boolean testE(int[] a, int e, int n)
/* AI: a != null, n>=0 AF: restituisce true se in 'a' esite un elemento che occorre esattamente n volte, false altrimenti */ static boolean testA(int[] a, int n)