1. Astrazione

Ci sono vari meccanismi di astrazione nell’ingegneria del software.

Astrazione per parametrizzazione

Definisco un’astrazione (un metodo in questo caso) e la chiamo ogni volta applicandogli un parametro.

public static int abs(int p) {
	if (p<0) return -p;
	 return p;
}
a = abs(a);
...
varB = abs(varB);
...
anotherVar = abs(anotherVar);

Astrazione per specifica

Non importa come il codice di una determinata funzione venga implementato, basta che si comporti come vogliamo.

Con questo tipo di astrazione ci interessa descrivere che cosa fa un determinato modulo, non curandoci di come questo vada poi ad implementare la cosa.

/* returns absolute value of p */
public static int abs(int p) {
	// Non mi importa come viene implementato questo metodo, basta che calcoli il valore assoluto
}

Vantaggi:

• Località: la specifica può essere letta e/o scritta, senza aver bisogno di sapere come viene fatta l’implementazione

• Modificabilità: l’astrazione può essere re-implementata, senza aver effetti su chi usa la funzione

Astrazione procedurale

Definisce, mediante specifica, un’operazione complessa su dati generici: per fare ciò si usa il JML, Java Modeling Language.

È necessario definire due cose:

• Precondizione: condizioni su parametri, sotto le quali la specifica è definita

• Postcondizione: garantiscono un determinato effetto alla fine dell’esecuzione dell’astrazione, assumendo che le precondizioni siano verificate

/*requires value >=0 of parameter x
*ensures returns the square root of x */
public static float sqrt(float x)

Le precondizioni si indicano con requires, mentre le postcondizioni si indicano con ensures.

Cosa accade de x < 0? Il metodo sqrt non è definito, pertanto ogni comportamento è accettato, dato che non dovrebbe mai accarere che una precondizione non sia verificata quando si chiama il metodo.

Esistono anche postcondizioni eccezionali, che vanno a definire quando il metodo deve lanciare un’eccezione.

Programmazione per contratto

Si parla di programmazione per contratto quando vengono specificate le pre e post condizioni.

/*@ requires x >= 0.0;
 @ ensures JMLDouble.approximatelyEqualTo(x,
 @ \result * \result, eps);
 @*/
public static double sqrt(double x) { ... }

Un contratto può essere rispettato da varie implementazioni, ciò che cambia tra di esse sono proprietà non funzionali, come efficienza, RAM consumata e carico sulla rete.

Asserzioni

Ci sono notazioni matematiche per scrivere le specifiche.

Nel codice Java è possibile inserire dei controlli, che vanno a vedere se determinate specifiche di un metodo vengono rispettate: se non vengono rispettate, viene lanciata un’eccezione.

Un’asserzione è un’espressione booleana, che viene verificata a runtime:

• Se è vera, continuo con l’esecuzione

• Se è falsa genero l’errore AssertionError e il programma viene terminato.

La sintassi è assert <espressione_booleana>.

Di solito si usano solo in fase di testing, e non vengono usate per verificare le precondizioni di metodi pubblici.

//@ ensures (if x in a, returns the index at which x is located, else returns -1);
public static int search(int a[], int x) {
...
return i;
}

Possiamo aggiungere un’asserzione, prima di return i, che verifica la corretta esecuzione del metodo: assert(i == -1 || a[i] == x).