4. Principio di sostituzione

Specifica di estensioni

Estensione è in Java il termine per l’ereditarietà: un’estensione C’ di una classe C è un erede di C.

Un’estensione è detta pura se non modifica la specifica dei metodi ereditati:

• essa può quindi solo estendere la specifica, aggiungendo nuove operazioni

• può modificare l’implementazione dei metodi ereditati, a patto che la specifica della super-classe rimanga inalterata

AF e RI di un’estensione

L’AF di una sottoclasse di solito è uguale a quella della super-classe.

Il RI della super-classe è ereditato senza modifiche e si aggiunge un nuovo RI.

Principio di sostituzione di Liskov

Gli oggetti della sottoclasse devono rispettare il contratto della super-classe: il contratto può essere esteso per coprire ulteriori casi, ma non può essere cambiato.

Questo garantisce che moduli che usano oggetti di un tipo devono poter usare oggetti di un tipo derivato, senza accorgersi della differenza.

Regole per la specifica di sottoclassi

Come si garantisce che il contratto dell’estensione dia compatibile con quello della super-classe?

Basta mostrare le seguenti tre proprietà della specifica dei tipi per avere la compatibilità:

• Regola della segnatura: un sottotipo deve avere tutti i metodi del supertipo, e segnature dei metodi del sottotipo devono essere compatibili.
  • Ciò garantisce che il contratto della super-classe sia ancora applicabile.
  • Esempio: il metodo non cambia prototipo

• Regola dei metodi: le chiamate ai metodi del sottotipo devono comportarsi come le chiamate ai metodi corrispondenti del supertipo.
  • Ciò verifica che il contratto dei singoli metodi ereditati sia compatibile con il contratto dei metodi originali
  • Esempio: un’estensione pura non cambia la specifica

• Regola delle proprietà: un sottotipo deve preservare tutti gli invarianti pubblici degli oggetti del supertipo.
  • Ciò verifica che la specifica nel suo complesso sia compatibile con quella originale

Regola dei metodi

Affinché la chiamata ad un metodo del sottotipo abbia lo stesso effetto, basta che la specifica sia la stessa.

Ma a volte la specifica del metodo deve essere cambiata. Allora valgono le seguenti regole:

• La precondizione può diventare più debole, cioè meno restrittiva

• La postcondizione può diventare più forte, cioè più restrittiva

Effetto degli operatori logici

• Disgiunzione (OR, ||): indebolisce una formula logica

• Congiunzione (AND, &&): rafforza una formula logica

• Implicazione (passare da B ad A→B): indebolisce una formula logica

JML ed estensioni

Come si ridefinisce in JML la specifica di un metodo?

Una sottoclasse eredita pre e post condizioni dei metodi pubblici e protetti della super-classe e i suoi invarianti pubblici.

Da un punto di vista sintattico basta fare così:

//@also
//@requires
//@ensures

Da un punto di vista semantico accade che:

• La parte //@requires della classe erede va in OR con quella della classe padre: la precondizione risulta quindi indebolita

• La parte //@ensures della classe erede va in AND con quella della classe padre: la postcondizione risulta quindi rafforzata

Eliminazione delle eccezioni

Quando si ridefinisce in una sottoclasse un metodo della superclasse è possibile eliminare le eccezioni se e solo se l’eccezione che si vuole eliminare non è usata o se il suo lancio è opzionale.