Zėŋōfōbìå

20 gennaio 2009

Contract Checking

Filed under: C#, DbC, informatica — Tag:, — Zeno @ 18:03

Guardando il webcast di PDC2008 relativo al Contract Checking and Automated Test Generatione with Pex mi sono chiariti una serie di aspetti relativi al DbC. Intanto pare proprio che la libreria Code Contract Library di cui parlavo nell’articolo Design By Contract verrà inclusa nella versione 4 di .NET 4.0 come core component. Poi viene spiegato che una ragione per usare questa tecnica è che fornendo maggiori informazioni sulla “semantica” del programma (vedi gli axioms del C++0x) si può aiutare il compilatore a fare scelte performanti, ma anche  generare in automatico dei test case. In particolare viene proposto Pex.

L’uso dei Contract serve quindi per:

  • run time checking
  • static checking
  • documentation generation

Il webcast specifica bene il significato di alcuni “contract”:

Requires

  • Ciò che deve essere vero all’entrata di un metodo

Ensures:

  • Ciò che deve essere vero all’uscita del metodo
  • Può specificare un comportamento quando viene lanciata un’eccezione

Invariants:

  • Ciò che deve essere vero per tutti i metodi della classe (inclusi i tipi derivati)

Interessante il fatto che impostando un contratto su un metodo virtuale della classe, anche gli override lo ereditano.

Come per gli Assert del C, la release non viene appesantita dai contracts.

Annunci

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.

Blog su WordPress.com.