Zėŋōfōbìå

17 gennaio 2009

Design by Contract

Filed under: C#, DbC, informatica — Tag:, — Zeno @ 19:41

Chiacchierando con JP sul suo blog, cercando di parlare male dei linguaggi che ci danno da vivere, siamo incappati nella questione del DbC.

Design By Contract (DbC) è una tecnica di programmazione adottata per la prima volta dal linguaggio Eiffel, che permette di definire delle condizioni a contorno del codice che debbano essere garantite durante tutta la sua esecuzione. I linguaggi e le estensioni che ammettono il DbC in genere permettono di definire:

– precondizioni : condizioni in entrata di funzione, possono essere dei limiti sulle variabili in ingresso.

– postcondizioni : garanzie fornite in uscita di funzione, che definiscono, per esempio, l’insieme dei valori d’uscita ed eventuali side effect.

– invarianti : certezze che devono essere mantenute durante l’esecuzione (per esempio il limite sui side effects)

Interessante il fatto che, in presenza di ereditarietà, le precondizioni degli ancestor possono essere strette, le postcondizioni allargate.

Questa tecnica sembra essere pronta per una rinascita, dal momento che sia il C++ che C# si stanno evidentemente preparando ad estendersi in questa direzione.

C++0x, infatti, incorpora i “concept”, che sono una estensione dei templates, certamente utili per fornire, tramite tecniche di metaprogrammazione, robusti metodi formali per garantire la correttezza del codice.

C#, a sua volta, pare che nella versione 4 incorpori una libreria, chiamata Code Contract Library, che è già disponibile al download. (Allego il contractsmanual  )

Ovviamente, simulare il DbC usando l’equivalente delle ASSERT del C, è possibile, in parte limitante, certamente inefficace: se la garanzia formale di correttezza venisse garantita staticamente i vantaggi sarebbero enormi. Un buon DbC effettuerà una parte di controlli staticamente, il resto runtime.

Come funziona il controllo statico? Questa è la domanda che più mi incuriosisce e mi immagino che la risposta sia sufficientemente interessante da farmi provare questa tecnica appena possibile.

Installando la CCL (Microsoft Research), oltre all’installazione della libreria e della documentazione pdf, viene integrato in VS2008 uno strumento atto alla gestione del DbC. In particolare, nelle propietà del progetto, viene aggiunta una nuova sezione, che permette di abilitare:

– dynamic check (con la possibilità di definire delle asserzioni implicite)

– static check.

Se si costruisce un metodo che ha tra le precondizioni un valore maggiore di 0 e gli si passa un valore negativo il DbC statico identifica il problema. (Spesso basterebbe aver modo di definire i range dei tipi, come in Ada , io credo, e avere un controllo statico sui boundaries. ).

Se per esempio una funzione con una postcondizione che limita l’ouput ad un intero minore di 10 viene passata come argomento ad una funzione che tra le precondizioni vuole un intero maggiore di 10, possiamo immaginare che esiste un possibile controllo statico che blocchi la compilazione di fronte a questa incongruenza.

Ho provato ad installare la libreria e a scrivere questo snippet:

internal double logarithm(double c)
{
  CodeContract.Requires(c  > 0);
  return Math.Log(c);
}

internal double negative(double a)
{
  CodeContract.Ensures(CodeContract.Result<double>() <= 0 );
  if (a > 0)
    return (-a);
  else
    return a;
}

Mi aspetterei un errore alla riga dove scrivo :

double c=logarithm(negative(123.0));

E in effetti ho un warning: requires unproven

Cioè viene detto che non è certo che i requisiti in ingresso del logaritmo siano provati.

Ovviamente ottengo l’errore runtime, ma, francamente mi aspettavo un errore un po’ più visibile.

Probabilmente la tecnologia è ancora troppo sperimentale, o forse non ho usato la keyword giusta, ma d’altra parte, mi pare che non sia ancora possibile scrivere un programma che sappia esprimersi sulla correttezza di un altro programma. ;-)

L’implementazione della libreria, per la parte runtime, è molto semplice, non aggiunge più overhead di quello di un’assert e l’impatto nella versione di release è praticamente nullo.

Credo quindi che abbia senso utilizzarla fin da adesso, se non altro per favorire la documentazione.

Annunci

7 commenti »

  1. Ciau. :D

    Ma se tanto ottieni l’errore a runtime una semplicissima assert non è meglio? :D

    PS: il nuovo standard C++ prevede anche le static_assert. :D

    Commento di jp — 18 gennaio 2009 @ 9:46

  2. Conosco le static_assert, è una delle librerie più antiche di boost. :-)
    La questione dell’assert invece è vera.
    Ad oggi un’assert è sostanzialmente equivalente. Magari con .net 4.0 ci sarà un controllo statico sulle assert… Magari usando questa libreria.
    Di solito Microsoft, prima di integrare delle funzionalità nei linguaggi, rilascia sotto forma di Research Product un branch del linguaggio.
    L’ha fatto con http://en.wikipedia.org/wiki/C%CF%89, che ha permesso l’uscita di LINQ.
    Forse le CCL sono un’anteprima di quello che sarà C# version++. ;-)
    Io mi auguro che si vada verso il Design By Contract, ha perfettamente senso che le assert (così come i test case, se vogliamo) vengano integrate nel linguaggio e non siano appannaggio solo di librerie, di ide e di quant’altro.

    Commento di Fabrizio — 20 gennaio 2009 @ 13:47

  3. Leggendo http://www.cpptalk.net/concept-axioms-vt57960.html:

    Compilers aren’t required to do anything with axioms other than parse
    them. The compiler could complain about your axiom being wrong, or it
    could “optimize” the code as above, or both, or nothing.
    Axioms are a way to pass on semantic information that only the author
    of the concept can know (“extrinsic” semantic properties) to the
    compiler, optimizer, and other software development tools. Use it
    where it helps, abuse it at your peril.

    Commento di Fabrizio — 20 gennaio 2009 @ 16:54

  4. […] DbC. Intanto pare proprio che la libreria Code Contract Library di cui parlavo nell’articolo Design By Contract verrà inclusa nella versione 4 di C#. Poi viene spiegato che una ragione per usare questa tecnica […]

    Pingback di Contract Checking « Zėŋōfōbìå — 20 gennaio 2009 @ 18:03

  5. Confido che il flag -pedantic del G++ effettui un “enformcement” intensivo e tratti le violazioni dei concept come degli errori. :D

    Ovviamente l’approccio del C# è molto più elegante e preciso. :D

    Commento di jp — 22 gennaio 2009 @ 10:19

  6. Era “enforcement” ma la dislessia impera… :D

    Commento di jp — 22 gennaio 2009 @ 12:00

  7. […] di aggiungere controlli statici e runtime sul linguaggio definiti dall’utente. Io credo che la direzione sia questa, C# 4.0 includerà alcune funzionalità di questo tipo, C++0x prevede le asserzioni statiche, i […]

    Pingback di Contratti e futuro « Zėŋōfōbìå — 29 gennaio 2009 @ 10:28


RSS feed for comments on this post. TrackBack URI

Rispondi

Effettua il login con uno di questi metodi per inviare il tuo commento:

Logo WordPress.com

Stai commentando usando il tuo account WordPress.com. Chiudi sessione / Modifica )

Foto Twitter

Stai commentando usando il tuo account Twitter. Chiudi sessione / Modifica )

Foto di Facebook

Stai commentando usando il tuo account Facebook. Chiudi sessione / Modifica )

Google+ photo

Stai commentando usando il tuo account Google+. Chiudi sessione / Modifica )

Connessione a %s...

Blog su WordPress.com.

%d blogger hanno fatto clic su Mi Piace per questo: