Design by contract

Autori: Vincenzo Manzoni, Andrea Rota

Sommario

Introduzione al Design by contract come modalità di progettazione del software. Nell'articolo saranno anche introdotti alcuni linguaggi specifici per il Dbc.

Introduzione

Il Design by contract (o brevemente DBC) è una modalità particolare per la progettazione del software, che vede al centro un contratto tra un "cliente" e un "fornitore".

Cosa è un contratto?

Un contratto è un accordo tra un cliente e un contrattore (o fornitore). Il contratto ha alcune peculiarità:

lega tra di loro due parti, cliente e fornitore;
è scritto;
specifica obblighi e benefici per entrambe le parti;
non contiene clausole nascoste.

L'oggetto del contratto per noi sarà il software; il contratto potrà essere stipulato sulla classe o sul singolo metodo. Stipulare un contratto sul software significa crare un doppio vincolo fra chi scrive il software e chi lo utilizza.

L'utilizzatore, o cliente, si impegna a rispettare le condizioni per il corretto utilizzo del software che sono scritte nel contratto (per esempio che gli input siano corretti o all'interno di un certo range). Queste condizioni sono chiamate precondizioni e sono solitamente decise da chi scrive il software.
Il programmatore, o fornitore, si impegna perché l'output del suo software rispetti le condizioni che sono scritte nel contratto, purché il cliente abbia rispettato tutti i vincoli nell'uso del prodotto. Queste condizioni sono chiamate postcondizioni e sono solitamente decise da chi commissiona e usa il software.

Gli obblighi del cliente diventano vantaggi per il fornitore e viceversa.

Sostanzialmente la stipula del contratto aiuta il programmatore a ridurre la complessità dei casi d'uso del suo software, sgravandolo da responsabilità qualora il suo prodotto sia usato non correttamente e aiuta il cliente ad usare correttamente il software. La scrittura dei vincoli viene fatta usando predicati logici.

Esempio
Il contratto prevede che il metodo int fattoriale(n) accetti numeri positivi e restituisca la funzione n!. Il cliente si impegna a passare n positivo e il fornitore a calcolare il fattoriale correttamente. Se il numero passato n è negativo, il fornitore non è tenuto a nessuna garanzia sulla correttezza dei risultati.

Precondizioni

La domanda che un programmatore si pone spesso è: "Devo controllare che gli input passati dall'utente siano corretti?". La risposta che la tecnica DBC dà è: "No, il controllo delle precondizioni è responsabilità del cliente". Nel caso presentato nell'esempio precedente, il cliente avrebbe dovuto scrivere:

 if(numero>=0){
  fattNumero = fattoriale(numero);
 } else {
  // azione di segnalazione/correttiva
  printf("Il numero inserito è negativo!"); 
 }

Le precondizioni possono essere più o meno restrittive; ecco un breve elenco di esempi di vincoli ordinati per restrittività:

TRUE: nessuna precondizione. Il funzionamento corretto del software è garantito per ogni input.
n>0: precondizione intervallare. Il funzionamento corretto del software è garantito solo per i valori di input interni all'intervallo.
n=1 or n=3: precondizione puntuale. Il vincolo sugli input è ristretto a singoli valori di input.
FALSE: il funzionamento corretto non viene garantito per nessun input.

Postcondizioni

Le postcondizioni vanno valutate esclusivamente alla fine della computazione.

Invarianti

Sono condizioni che devono valere dalla creazione dell'oggetto alla sua morte e sono riferite a proprietà caratteristiche dell'oggetto. Ad esempio se l'oggetto è un orologio, il contatore delle ore dovrà essere compreso fra 0 e 23 e il contatore dei minuti fra 0 e 59.

Vantaggi nell'utilizzo dei contratti

Esistono dei vantaggi nell'utilizzo dei contratti:

le classi vengono documentate in modo accurato e questo favorisce la manutenibilità del software;
il programmatore può concentrarsi sul problema da risolvere e non sul controllo della correttezza degli input (che potrà essere fatto ad uno stadio successivo);
descrizione accurata di ciò che si intende per comportamento corretto di un programma, utile in fase di testing: diremo che un programma A è corretto se partendo da uno stato che soddisfa il predicato P delle precondizioni si arriva ad uno stato che soddisfa il predicato Q delle postcondizioni (Hoare Triple, v. Risorse in rete);
se cliente e fornitore rispettano i contratti, viene garantita maggiormente la correttezza del software.

A questi si aggiungono anche dei vantaggi tecnici non indifferenti:

Sviluppo diventa maggiormente focalizzato sulle specifiche
Il dbc fornisce quasi automaticamente piani di test per black-box
I malfunzionamenti vengono individuati vicino alla loro causa, così che è facile individuare i difetti del software e correggerli.

Linguaggi per il DBC

Esistono vari linguaggi che permettono di usare tecniche DBC per la modellazione e la scrittura del codice; fra questi ricordiamo Gnu Nana, Jml, Eiffel e le JDK 1.4 assertions.

Gnu Nana

GNU Nana è una libreria libera che fornisce un supporto al controllo delle asserzioni e al logging per i compilatori GNU C e GNU C++. Fornisce l'implementazione di alcune idee di Eiffel, VDM, Z e Anna in GNU C/C++.

(Liberamente tradotto da http://www.gnu.org/software/nana/nana.html)

Esempio
Sia square_root una funzione intera che ritorna la radice quadrata arrotondata all'intero più basso di un numero intero x.

 int square_root(int x)
 /*@
  assume x>0;
  return y>0,
         y<=x*x,
         y<(x+1)*(x+1);
 @*/

dove assume indica una precondizione e return indica una postcondizione.

JML

Vedere l'articolo JML di Giorgio e Vincenzo.

Eiffel

E' un vero e proprio linguaggio di programmazione che contiene istruzioni per la gestione delle precondizioni, delle post condizioni e degli invarianti.

Ecco un esempio:

 -- classe che modella un conto bancario
 class CONTOBANCARIO
  disponibilità: INTEGER
  disponibilità_min: INTEGER is 1000

  -- costruttore
  make (versamento_iniziale: INTEGER) is do
   disponibilità:=versamento_iniziale
  end

  -- precondizioni sul costruttore
  require
   pre1: versamento_iniziale>=disponibilità_min

  -- postcondizioni sul costruttore
  ensure
   post1: disponibilità=versamento_iniziale

JDK 1.4 Assertion

Permettono di annegare nel codice Java dei controlli che vengono eseguiti a runtime: la sintassi è:

 assert(condizioni)

ad esempio

 public int fattoriale(int n) {
   assert(n>0);
   ...
 }

Se le condizioni non si verificano l'assert fallisce: differentemente dalle eccezioni, il meccanismo delle JDK Assertion può essere spento quando si ha sufficiente fiducia nel codice: in questo modo il codice viene eseguito più rapidamente. Gli svantaggi delle JDK Assertion è che non dispongono di una semantica propria (se non quella mutuata da Java), non sono visibili direttamente dall'interfaccia e non è possibile distinguere se una assert riguarda una precondizione, una postcondizione o un invariante. Le JDK Assertion inoltre non dispongono di un meccanismo di documentazione.

Risorse in rete

Wikipedia ha una voce relativa al Design By Contract, con un elenco dei tool per i vari linguaggi.
Un'interessante pagina di Wikipedia sulla Hoare logic, argomento fortemente connesso con il DBC e il testing.
Eiffel Software, http://www.eiffel.com/, la casa produttrice dei tool basati sul linguaggio Eiffel
GNU Nana Project, http://www.gnu.org/software/nana/nana.html, il sito ufficiale delle librerie Nana per GNU C e C++.

DesignByContract