Postcondizione
In programmazione, una postcondizione è una condizione o un predicato che deve essere sempre vero immediatamente dopo l'esecuzione di una sezione di codice o dopo un'operazione in una specifica formale. Le postcondizioni sono solitamente verificate utilizzando asserzioni all'interno dello stesso codice. Spesso, le postcondizioni sono solo incluse della documentazione del relativo segmento di codice.
Ad esempio: il risultato di un fattoriale è sempre un numero intero maggiore o uguale ad 1. Quindi, un programma che calcola il fattoriale di un numero in input avrà come postcondizione che il risultato dopo il calcolo sia un intero e che sia maggiore od uguale ad 1. Un altro esempio: un programma che calcola la radice quadrata di un numero in input deve avere come postcondizioni che il risultato sia un numero e che il suo quadrato sia uguale all'input.
Postcondizioni nella programmazione ad oggetti[modifica | modifica wikitesto]
Nella programmazione ad oggetti, le postcondizioni, unitamente alle precondizioni ed alle invarianti, sono componenti del modello di progettazione del software a contratto.
Le postcondizione di una routine è la dichiarazione delle proprietà che sono garantite al completamento dell'esecuzione della routine stessa.[1] Poiché è collegata al contratto della routine, la postcondizione assicura al potenziale chiamante che, nel caso in cui la routine venisse chiamata in uno stato in cui le sue precondizioni fossero soddisfatte, le proprietà dichiarate dalla postcondizione siano assicurate.
Esempio in Eiffel[modifica | modifica wikitesto]
Il seguente esempio scritto in Eiffel imposta il valore dell'attributo hour di una classe sulla base del valore fornito dal chiamante a_hour. La postcondizione segue la parola chiave ensure. In questo esempio la postcondizione garantisce, nel caso in cui le precondizioni vengano soddisfatte (ad esempio, quando a_hour rappresenti una valida ora del giorno), che dopo l'esecuzione di set_hour l'attributo della classe hour avrà lo stesso valore di a_hour. Il tag "hour_set:" descrive la clausaola della postcondizione e serve ad identificarla in caso di violazione durante l'esecuzione.
set_hour (a_hour: INTEGER)
-- Set `hour' to `a_hour'
require
valid_argument: 0 <= a_hour and a_hour <= 23
do
hour := a_hour
ensure
hour_set: hour = a_hour
end
Postcondizioni ed ereditarietà[modifica | modifica wikitesto]
In presenza di ereditarietà, le routine che discendono dalla classe (sottoclassi) ereditano anche il contratto, che comprende precondizioni e postcondizioni attualmente in essere. Ciò significa che ogni implementazione o ridefinizione delle routine ereditate deve attenersi al contratto ereditato. Le postcondizioni possono essere modificate nelle routine ridefinite, ma solo se vengono rafforzate.[2] Ciò significa che la ridefinizione può solo aumentare i benefici che fornisce agli utilizzatori, e mai diminuirli.
Note[modifica | modifica wikitesto]
- ^ Meyer, Bertrand, Object-Oriented Software Construction, second edition, Prentice Hall, 1997, p. 342.
- ^ Meyer, 1997, pp. 570–573.