• Design by contract (DbC) (Progettazione per contratto) è una metodologia di progettazione software
• Il progettista deve definire specifiche precise e verificabili delle interfacce dei componenti software che va a sviluppare
• Una specifica funzionale (contratto) viene creato per ogni modulo nel sistema prima di codificarlo
• L'esecuzione del programma è vista come l'interazione fra i vari moduli vincolati da questi contratti

• Paradigma proposto nel linguaggio Eiffel (Betrand Meyer, 1986)
• Uso di asserzioni in varie fasi di sviluppo
  • Progetto: approccio pragmatico alle specifiche
  • Implementazione: guida per la programmazione
  • Documentazione: interfacce con info aggiuntive
  • Collaudo: DbC delimita i casi da testare (per affidabilità)
  • Manutenzione: DbC fa emergere prima gli errori
  • Uso finale: sollevate eccezioni se violazioni

• Precondizioni
  • Stabiliscono se è possibile chiamare un metodo
  • Prerequisiti per l’attivazione
• Postcondizioni
  • Stabiliscono se il metodo restituisce il valore atteso, cioè se produce l’effetto desiderato
  • … In relazione ai parametri (che soddisfano le precondizioni)
  • Definiscono il significato del metodo
• Divisione delle responsabilità tra moduli
  • Errore del codice chiamante (client) se precondizioni non soddisfatte
  • Errore del codice chiamato (server), se postcondizioni non soddisfatte

• Precondizioni + postcondizioni = contratto
  • … tra modulo chiamante e modulo chiamato
• Infrazione di un contratto: problema serio
  • Errore rispetto alle specifiche
  • Eccezione e/o terminazione

public double sqrt(double x) { /* ... */ }

• Precondizioni: x >= 0
• Postcondizioni: abs(result * result - x) <= 0.00001
• Codice chiamante
  • Obblighi: deve passare un numero non negativo
  • Benefici: riceve la radice del numero
• Codice chiamato
  • Obblighi: restituisce un numero r tale che r * r ≃ x
  • Benefici: può assumere che x non è negativo

• Vincolo che deve valere per ogni stato stabile di un oggetto, durante tutto il suo ciclo di vita
• Rafforzamento generale di pre- e post-condizioni
• “Criterio di sanità” dell’oggetto
• Deve essere soddisfatto dal costruttore
• Deve essere mantenuto dai metodi pubblici
• Ma non necessariamente da metodi privati o protetti

• Espressioni booleane, simili a predicati matematici
• Esprimono proprietà semantiche di classi e metodi
• Utili per collaudo e debugging, ma anche documentazione
• Violazione → AssertionError (e normalmente abort, terminazione programma)

assert age >= 0;

assert age > 0

static_assert(age>0,"Error negative age");

• Asserzioni in genere utili per:
  • Precondizioni, postcondizioni, invarianti di classe
  • Invarianti interne e di controllo del flusso
• Argomenti di metodi pubblici sbagliati → eccezione
  • IllegalArgumentException o sottoclasse
  • Asserzioni normalmente disabilitate, usate solo per debug
  • Attivate con il flag -ea del comando java
• Attivare controllo asserzioni in Eclipse
  • Menu Run ->run configuration
  • selezionare java application (pannello sn))
  • selezionare Arguments tab
  • aggiungere -ea in VM arguments.

while True:
  try:
    val = int(input("eta: "))
    break
  except ValueError:
    print("Attenzione valore inserito non numerico")

#include <iostream>
using namespace std;
int Fatt(int n) {
  if(n< 0)     throw invalid_argument("Negative paramether");
  if (n==0)    return 1;
  return n*Fatt(n-1);
}
int main() {
  long fi;  int n = -3;
  try {
    fi = Fatt(n); //cause an exception to throw
  }
  catch(invalid_argument& e) {
    cerr << "error: " << e.what() << endl;  return -1;
  }
  cout << n << "!=" << fi << endl;   return 0;
}

public static int fatt(int n) {
  if(n< 0)     throw new IllegalArgumentException("The argument can not be negative");
  if (n==0)    return 1;
  return n*Fatt(n-1);
}


public static void main(String args[]) {
  long fi;  int n = -3;
  try {
    fi = fatt(n); //cause an exception to throw
  }
  catch(IllegalArgumentException e) {
    System.out.println(e);
  }
  System.out.println(n+"! = "+fi);
}

def sqrt(x: float) -> float:
    '''
    Precondition: x >= 0
    Postcondition: abs(result * result - x) <= 0.00001
    '''
    if x < 0 raise ValueError("sqrt: arg < 0")

    # ...

    assert abs(result * result - x) <= 0.00001
    return result

/**
 * Precondition: x >= 0
 * Postcondition: abs(result * result - x) <= 0.00001
 */
public double sqrt(double x) {
    if (x < 0) throw new IllegalArgumentException("sqrt: arg < 0");

    // ...

    assert Math.abs(result * result - x) <= 0.00001;
    return result;
}

/**
* Precondition: n pari
* Postcondition: return val < n
*/
public int mezzo(int n) {
  // Precondizione
  if ( n % 2 != 0)
    throw new IllegalArgumentException("parametro n dispari");
  int m;
  m = n / 2;
  // Postcondizione
  assert m < n;
  return m;
}