[Vari] Design By Contract

[banryu79]

Volevo sapere se qualcuno di voi ha mai realizzato qualcosa con Eiffel in particolare o comunque applicando la metodologia citata nel titolo; nel caso qualcuno abbia avuto esperienza in materia, sarei curiosio di conoscere la sua opinione: cosa ne pensa, come si è trovato, il confronto rispetto a prima, ecc...

Mi sto documentando a spizzichi (ho cominciato leggendo questo (http://se.ethz.ch/~meyer/publications/computer/contract.pdf)) in parte perchè incuriosito dall'argomento e in parte perchè stimolato dalla lettura di discussioni in questo forum tipo questa (http://www.hwupgrade.it/forum/showthread.php?t=2162169&highlight=Design+contract) e per essermi a mia volta scontrato in passato con problemi analoghi. (Inoltre alcune letture sulla programmazione concorrente in Java mi hanno fatto conoscere le postcondition e gli invariants e la loro importanza anche in questo ambito specifico, almeno per questo linguaggio e probabilmente in modo analogo per tutti quelli di derivazione OO, penso).

Grazie a chiunque volesse condividere la sua esperienza e le sue opinioni in merito :)

[shinya]

Se ti interessa puoi anche vedere come si gestisce la cosa in D: http://www.digitalmars.com/d/2.0/dbc.html

Le impressioni te le dirò più avanti quando avrò più dimestichezza col linguaggio :D

[banryu79]

Se ti interessa puoi anche vedere come si gestisce la cosa in D: http://www.digitalmars.com/d/2.0/dbc.html

Le impressioni te le dirò più avanti quando avrò più dimestichezza col linguaggio :D
Ok, grazie.

Provo a sviluppare un po' l'argomento; parto con la prima considerazione che si sta formando nella mia testa e che riguarda l'uso delle asserzioni logiche (assertions), uno strumento fondamentale della metodologia DBC.

Non ho mai programmato abitualmente con le asserzioni (le ho provate ma non ho mai approfondito e le ho snobbate), mea culpa, per carità, però leggendo di questi strumenti, dei modi in cui vengono utilizzati e dei loro scopi in questa metodologia, mi sembra interessante cominciare a introdurli come elemento d'uso quotidiano nel software che scrivo.
Ho l'impressione che mi potrebbe succedere quello che mi è successo quando ho cominciato ad usare uno strumento simile: lo unit test.

Dopo aver sperimentato lo unit test per sviluppare un piccolo modulo in una mia applicazione ho capito quanto mi servisse uno strumento del genere: un sacco (ma veramente tante!) di sviste/errori e mancanze rilevate praticamente subito e corrette tanto facilmente. Ore risparmiate.
Maggior fiducia nel codice prodotto, e nel fatto di poterlo "rimaneggiare" con più tranquillità, poichè i DO e DO NOT da rispettare erano chiaramente scritti e altrettanto spietatamente eseguiti ad ogni build.

Ho il sospetto che potrebbe essere così anche con le asserzioni.

Il fatto di chiedere a chi ha provato sulla propria pelle il DBC le proprie esperienze e opinioni è un mio tentativo di farmi un'idea di massima su quanto possa incidere sulla produttività in fase di scrittura del codice e se porta anche qualche beneficio in termini di progettazione di un modello di un sistema software e/o alla sua trasposizione nella forma di codice sorgente in un linguaggio di programmazione OO.

Questo per via del fatto che tale metodologia supporta la definizione e il controllo espliciti delle invariati di stato di un oggetto.
(Da cui, a seguire, le considerazioni in ambito di progettazione di un sistema software ad oggetti, e poi anche in ambito di programmazione concorrente, sempre in un linguaggio che supporta la prospettiva OO mettendo a disposizione a livello di linguaggio costrutti quali le classi).

Inoltre sono anche curioso di sapere se è usato o meno, perchè non ne sento parlare tanto in relazione ad altre metodologie.

[banryu79]

Piccolo up... :stordita:

Avrei una curiosità, per i programmatori Java: avete mai provato a seguire le linee guida della Sun (ei fu) relative all'uso di assert ed eccezioni (http://download.oracle.com/javase/1.4.2/docs/guide/lang/assert.html) per adottare una sorta di design-by-contract "informale" nella stesura delle vostre classi?

So che per questo linguaggio esistono delle librerie/framework appositi che tentano di dare supporto a questo stile di programmazione, ma qualcuno ha esperienza di un uso circostanziato di 'assert' magari affiancato allo unit test?

[cdimauro]

In tutta onestà preferisco l'approccio TDD.

Le finalità alla fine sono le stesse, ma preferisco tenere separato il codice di produzione dal controllo del suo comportamento. Quindi tutte le assert e i controlli li faccio esclusivamente nel codice dei test.

[banryu79]

Le finalità alla fine sono le stesse, ma preferisco tenere separato il codice di produzione dal controllo del suo comportamento. Quindi tutte le assert e i controlli li faccio esclusivamente nel codice dei test.
In tutta onestà credo di no, almeno non completamente, stando a quanto dice Meyer (nell'articolo linkato al post #1).

Non credo che si equivalgano per un tot di considerazioni:
- nel DBC propriamente detto esiste il concetto di "contratto", che è direttamente supportato dal linguaggio e specificato chiaramente e verificato nel codice che implementa la classe/metodo che fornisce il dato servizio.
Inoltre anche il chiamante di un servizio (cliente) è tirato in ballo, dato che gli viene richiesto di soddifare dei prerequisiti a fronte dei quali avrà garanzia di ottenere il servizio atteso dal chiamato (fornitore).
Il rispetto del contratto viene verificato a runtime* ogni volta che l'applicazione gira realmente; il "contratto" fa parte dell'applicazione, anzi sembra quasi che il "contratto" sia l'applicazione (e la specifica del contratto fa parte del sorgente stesso).

* salvo il fatto di poter disabilitare i controlli una volta distribuito il prodotto (di solito questi check sono ad uso e consumo degli sviluppatori, in Eiffel) per motivi di performance.
In Java, in modo analogo, i controlli delle assert sono disabilitati di default.

- col TDD la verifica dei test non avviene ad ogni runtime dell'applicazione, viene eseguita "solo" ad ogni build. Non essendoci la nozione di un "contratto" in termini di pre/post condizioni e di invarianti non c'è neanche l'obbligo di esplicitare questo contratto, e neppure sono presenti, strumenti appositi per supportare il "contratto" in modo diretto (questo supporto, in Eiffel, ad esempio ha conseguenze anche sul meccanismo di subclassing).


In sostanza, mi par di capire, la mancanza di un "contratto" (così come inteso dal DBC) esplicitatamente definito e supportato dalla metodologia del TDD rende appunto il TDD una cosa diversa dal DBC, anche se hanno sicuramente degli aspetti in comune, e sicuramente condividono alcuni obiettivi:

...help improve the reliability of software systems.
Reliability is here defined as the combination of correctness and robustness or more prosaically, as the absence of bugs.



Per quello mi sto chiedendo se ha senso, e in tal caso in che modo, affiancare entrambi gli stili...

[sirus]

Ho avuto la possibilità di utilizzare Eiffel nel corso di Software Engineering 2 al PoliMi, corso che quell'anno si è svolto in collaborazione con l'ETH di Zurigo (l'università dove lavora Meyer).

Sono sempre stato scettico sul DBC ed il corso di Software Engineering 2 non mi ha assolutamente fatto cambiare idea. Il DBC implementato in Eiffel non permette di specificare molte delle condizioni che un programmatore che adotta tale design pattern vorrebbe introdurre. Se devo utilizza il DBC per controllare condizioni banali preferisco farlo attraverso metodi più tradizionali.

Inoltre, avere un contratto e non avere la possibilità di verificare che il codice scritto rispetti effettivamente tale contratto (e non è possibile a meno di semplificazioni a mio modo di vedere un po' assurde) non porta vantaggi.

Per quanto mi riguarda il DBC è bocciato.

[banryu79]

Ciao sirus,
intanto grazie mille della testimonianza! :)

Vorrei chiederti ulteriori delucidazioni, quando dici:

Il DBC implementato in Eiffel non permette di specificare molte delle condizioni che un programmatore che adotta tale design pattern vorrebbe introdurre. Se devo utilizza il DBC per controllare condizioni banali preferisco farlo attraverso metodi più tradizionali.

Non riesco bene a capire a cosa ti riferisci.
Se hai tempo & voglia e la possibilità di ripescare roba tipo esercizi svolti all'epoca (dalla memoria del tuo pc o dalla tua testa :D) potresti postarmi un esempio che illustra questa problematica?


Inoltre, avere un contratto e non avere la possibilità di verificare che il codice scritto rispetti effettivamente tale contratto (e non è possibile a meno di semplificazioni a mio modo di vedere un po' assurde) non porta vantaggi.

Beh, questo in effetti sembra interessante, nonchè una bella rogna :D
Mi rendo conto che per capire meglio le cose dovrei addentrarmi di più nell'argomento (aka studiare qualche kilata di roba, e provare direttamente la faccenda [la seconda, non lavorando veramente "on the field", è un po' dura]).

Ad essere sincero, il mio interesse casca più che altro nella possibilità di definire (per poi controllare) esplicitamente le invarianti di una classe.

Sto cercando più che altro di digerire questo aspetto, perchè mi sembra importante. Io programmo in Java, e le invarianti di una classe, una volta definite, posso controllarle dotando la classe stessa di un metodo non-pubblico che esegue il controllo, da richiamare al termine di ogni costruttore e metodo pubblico, subito prima dell'istruzione di ritorno dl controllo al chiamante, e da usare solo come argomento di una istruzione assert.

Le precondizioni invece vengono gestite con controlli che lanciano eccezioni oppure con le assert, a seconda che ci si trovi in un metodo pubblico o non-pubblico.

Resterebbero le postcondizioni, ovvero i controlli sul risultato prodotto e garantito che il chiamato fornisce al chiamante. Qui, in Java non essendoci un supporto "nativo" del DBC a volte può capitare di dover usare una tecnica un po' troppo "rognosa" a mio avviso (vedere link al post #4).
Anche perchè secondo le linee guida che ho letto andrebbero verificate sia nei metodi pubblici che in quelli non-pubblici.

E sto avendo la probabilmente malsana idea di sostituire il controllo delle postcondizioni almeno per i metodi non-pubblici con la copertura di unit tests che verificano la correttezza del risultato atteso.
Non è la stessa cosa, ma è una sorta di controllo più rilassato.
Sto insomma maturando l'idea di usare alcune idee del DBC (in primis il controllo delle invarianti) affiancate allo unit testing nella speranza/convinzione di ottenere maggiori benefici rispetto al solo uso dello unit testing.

Uno di questi benefici, per me, è quello derivante dal fatto che espicitando le invarianti di una classe e introducendone un controllo esplicito, dovrei avere vita più facile nel non commettere certi errori quando, a distanza di tempo, devo rimettere le mani sulla classe per apportare delle modifiche, ad esempio.

Un'altro vantaggio è dato dal fatto che l'individuazione delle invarianti è una cosa molto importante se la classe che si sta scrivendo deve condividere dati mutabili tra più threads, per tutta una serie di ragioni.

Un'ultima ragione è che mi sembra di "intuire" l'importanza del fatto di avere coscienza delle invarianti di una classe, sia che la si abbia già scritta sia che la si debba ancora scrivere ed esista solo nella nostra testa, in un dato momento.

[banryu79]

Se ti interessa puoi anche vedere come si gestisce la cosa in D: http://www.digitalmars.com/d/2.0/dbc.html

Ciao, ho letto e ho visto che il DBC in D è supportato a livello di linguaggio sostanzialmente nello stesso modo che in Eiffel.

[sirus]

Partiamo con una premessa, il DBC adottato senza la possibilità di verificare tutte le condizioni che si scrivono e l'effettiva aderenza del codice alle condizioni poste è, secondo me, uno spreco di risorse. Proseguiamo.

Non riesco bene a capire a cosa ti riferisci.
Se hai tempo & voglia e la possibilità di ripescare roba tipo esercizi svolti all'epoca (dalla memoria del tuo pc o dalla tua testa :D) potresti postarmi un esempio che illustra questa problematica?
Per essere un minimo "credibili" pre-condizioni, invarianti e post-condizioni si scrivono attraverso un linguaggio logico, generalmente logica proposizionale oppure logica del prim'ordine. La logica proposizionale è un giocattolo se si vogliono valutare condizioni "rilevanti", la logica del prim'ordine è più adatta. Tuttavia, i tempi di valutazione della logica del prim'ordine possono essere grandi e la possibilità di valutare la condizione non è sempre garantita. Volendo alzare il tiro c'è anche la logica temporale (le logiche di ordine superiore al primo mi pare non siano teorie complete, ma non ci metterei la mano sul fuoco) ma la quantità di semplificazioni necessarie per "trattarla" è alta e per verificare la soddisfacilibilità di un insieme di condizioni (anche banali) ci si spendono ore su ore.

Avendo la possibilità di verificare effettivamente condizioni semplicistiche preferisco utilizzare il TDD piuttosto che appesantire la fase di design con lo sviluppo di pre-condizioni, invarianti e post-condizioni visto che la loro verifica a-priori non è trattabile.
Dico che non è trattabile perché ci sono paradigmi di programmazione come quella riflessiva (e se non sbaglio anche quella generica) che non possono essere verificati. Data la diffusione di questi metodi di programmazione direi che l'utilità del DBC e la verificabilità del codice hanno poco senso.

Un'altro vantaggio è dato dal fatto che l'individuazione delle invarianti è una cosa molto importante se la classe che si sta scrivendo deve condividere dati mutabili tra più threads, per tutta una serie di ragioni.
Per questo ci vorrebbe la logica temporale, non quella proposizionale. Tanti auguri se vuoi fare qualche cosa di serio. :D

[cdimauro]

Torno nuovamente sulla discussione, visto che ho qualche minuto di respiro. :D E chiarisco perché parlavo di similitudine fra DBC e TDD a livello di finalità.

Il mio scopo con la TDD è di testare che il comportamento di un "oggetto" (inteso non soltanto come "classe" nella OOP, ma più astrattamente come entità che nasce per assolvere a determinati requisiti) sia quello che mi aspetto.

Pertanto scriverò dei test per mi aiutino a modellare tutto ciò. In buona sostanza e prendendo in prestito un po' di matematica, coi test posso controllare che a seguito di un certo input x la mia funzione f restituisca la y che mi aspettavo; questo per gli input e gli output che mi aspetto.

Tutto ciò nel DBC si traduce nella scrittura di codice di pre e post-condizione, e delle invarianti che tengono "sotto controllo" il contratto, appunto.

Le invarianti con la TDD non si possono controllare, ma nemmeno ha senso farlo a mio avviso: quel che conta è che il codice si comporti per come mi aspetto che faccia.

D'altra parte, e come diceva sirus, ci sono casi non controllabili / testabili dal DBC, mentre con la TDD invece non ci sono problemi in tal senso.

Altra cosa importante, con la TDD ho codice e test ben separati. Questo mi aiuta a capire cosa fa il codice perché non c'è altro in mezzo. I test mi aiutano, invece, a capire come usarlo. Soprattutto non mi devo preoccupare di togliere il codice di test quando vado in produzione, come col DBC: non c'è bisogno, essendo tutto separato.

Spero di essere stato chiaro, ma vado di fretta. :stordita:

[banryu79]

Dato lo scarso tempo per via del lavoro, rispondo "a rate".
Partiamo con sirus:

Per essere un minimo "credibili" pre-condizioni, invarianti e post-condizioni si scrivono attraverso un linguaggio logico, generalmente logica proposizionale oppure logica del prim'ordine. La logica proposizionale è un giocattolo se si vogliono valutare condizioni "rilevanti", la logica del prim'ordine è più adatta.

Ci ho messo un po' perchè ho dovuto prima capire di cosa parlavi quando ti riferivi a "logica proposizionale" e "linguaggio del primo ordine".
In questa maniera sono riuscito a capire quello che stai dicendo e ti ringrazio per aver riportato più in dettaglio i limiti del DBC che hai riscontrato nella tua esperienza.


Tuttavia, i tempi di valutazione della logica del prim'ordine possono essere grandi e la possibilità di valutare la condizione non è sempre garantita. Volendo alzare il tiro c'è anche la logica temporale (le logiche di ordine superiore al primo mi pare non siano teorie complete, ma non ci metterei la mano sul fuoco) ma la quantità di semplificazioni necessarie per "trattarla" è alta e per verificare la soddisfacilibilità di un insieme di condizioni (anche banali) ci si spendono ore su ore.

Avendo la possibilità di verificare effettivamente condizioni semplicistiche preferisco utilizzare il TDD piuttosto che appesantire la fase di design con lo sviluppo di pre-condizioni, invarianti e post-condizioni visto che la loro verifica a-priori non è trattabile.

Da tutto il tuo discorso, quello che mi par di capire è che il DBC da solo, come paradigma, è solo metà della mela.
Per ottenere l'altra metà bisogna investire le neccessarie risorse e tempo, che sono beni scarsi, dunque economici, il che, di conseguenza, pone la questione se "il gioco vale la candela".


Dico che non è trattabile perché ci sono paradigmi di programmazione come quella riflessiva (e se non sbaglio anche quella generica) che non possono essere verificati. Data la diffusione di questi metodi di programmazione direi che l'utilità del DBC e la verificabilità del codice hanno poco senso.

Forse invece è comunque verificabile, anche se non solo col DBC come hai sottolineato.
Girando per il web armato di curiosità ho scoperto (beh, sia chiaro, per me è una scoperta perchè prima lo ignoravo :D) un paradigma chiamato "Verified Design by Contract" [qui (http://en.wikipedia.org/wiki/Formal_verification)].
Quel "Verified" forse è la metà della mela mancante; e sembra che per realizzarla servano processi automatizzati per fare quello che hai descritto tu sopra, ovvero specificare e poi verificare la soddifacibilità di un insieme di condizioni poste in un sistema logico del primo ordine (o altro, non saprei).

Seguendo il link precedente ho trovato questo prodotto (http://en.wikipedia.org/wiki/Perfect_Developer); per chi fosse curioso qui si trova una breve descrizione (http://www.eschertech.com/products/step_by_step_guide.php) delle varie fasi del processo di sviluppo di una applicazione software realizzata utilizzando tale strumento.



Per questo ci vorrebbe la logica temporale, non quella proposizionale. Tanti auguri se vuoi fare qualche cosa di serio. :D

No, non mi riferivo a nessuna verifica delle condizioni di soddisfacibilità di un insieme di condizioni formalizzate con la logica temporale, anche perchè fino a poche ore fa non avevo neanche idea di cosa si trattasse :p

Mi riferivo invece all'importanza che ha per un programmatore la chiara e precisa percezione delle invarianti di una classe in Java, in ottica di programmazione multithreading (ci sono varie ragioni, ma questo è un'altro discorso).

[marco.r]

Partiamo con una premessa, il DBC adottato senza la possibilità di verificare tutte le condizioni che si scrivono e l'effettiva aderenza del codice alle condizioni poste è, secondo me, uno spreco di risorse.
Proseguiamo.

Per essere un minimo "credibili" pre-condizioni, invarianti e post-condizioni si scrivono attraverso un linguaggio logico, generalmente logica proposizionale oppure logica del prim'ordine.

Non la farei cosi' drammatica. Per come la vedo io il design by contract non equivale necessariamente alla verifica formale, anzi.
Quest'ultima prevede di poter verificare un modello, ma non solo ci sono delle difficolta' di base nel mappare codice e modello, non sempre questo ce l'hai, oppure non puoi sapere se e' corretto.
L'approccio di linguaggi tipo Eiffel e' piu' pragmatico, e permette di verificare a runtime (piuttosto che staticamente come di solito accade con i metodi formali) che le condizioni previste sono puntualmente verificate.
Alcune verifiche sono effettivamente difficili da fare ma questo e' vero pure per gli altri metodi, per cui.


La logica proposizionale è un giocattolo se si vogliono valutare condizioni "rilevanti", la logica del prim'ordine è più adatta. Tuttavia, i tempi di valutazione della logica del prim'ordine possono essere grandi e la possibilità di valutare la condizione non è sempre garantita. Volendo alzare il tiro c'è anche la logica temporale (le logiche di ordine superiore al primo mi pare non siano teorie complete, ma non ci metterei la mano sul fuoco) ma la quantità di semplificazioni necessarie per "trattarla" è alta e per verificare la soddisfacilibilità di un insieme di condizioni (anche banali) ci si spendono ore su ore.

Il problema del tempo e' relativo. Si stanno facendo parecchi progressi a riguardo e ormai tecniche che usano metodi non esaustivi per la validazione del modello cominciano ad essere consolidate. Il problema e' semmai trovare un modello adatto per rappresentare la computazione o almeno un aspetto di essa.


Avendo la possibilità di verificare effettivamente condizioni semplicistiche preferisco utilizzare il TDD piuttosto che appesantire la fase di design con lo sviluppo di pre-condizioni, invarianti e post-condizioni visto che la loro verifica a-priori non è trattabile.

Mah, alla fine non c'e' una enorme differenza. Gli unit test non li vedo molto differenti dalla verifica delle post-condizioni, visto che non fai che controllare il "risultato" (in senso generico) dell'esecuzione di un pezzo di codice. La differenza sta che in un caso fai la verifica su di un numero limitato di casi, mentre in quell'altro ti porti il peso della verifica a run-time. Ognuno dei due ha i suoi pregi, e infatti non sono completamente alternativi. Una cosa che manca agli unittest e' la verifica delle pre-condizioni, che e' implicita nella corretta scrittura degli input dello unit test (anche se idealmente uno utilizza il sistema di tipi del linguaggi per limitarle)

[nuovoUtente86]

Premetto di essere d' accordo con quanto detto su da marco ed in più vorrei soffermarmi su questo punto:
Avendo la possibilità di verificare effettivamente condizioni semplicistiche preferisco utilizzare il TDD piuttosto che appesantire la fase di design con lo sviluppo di pre-condizioni, invarianti e post-condizioni visto che la loro verifica a-priori non è trattabile.
Dico che non è trattabile perché ci sono paradigmi di programmazione come quella riflessiva (e se non sbaglio anche quella generica) che non possono essere verificati. Data la diffusione di questi metodi di programmazione direi che l'utilità del DBC e la verificabilità del codice hanno poco senso.

circa il quale direi che piuttosto che l' impossibilità della verifica, a runtime, delle condizioni, il problema vero (che può verifcarsi appunto nei casi di caricamento e binding dinamico) è la conoscenza del contratto target da parte del chiamante. In questa ottica è molto interessante l' implementazione, per il linguaggio Java, del framework JContractor che risolve i problemi già evidenziati in questa discussione. L' idea di base, semplificando molto, è quella di definire in file separati il contratto e garantirne il rispetto attraverso la tecnica del bytecode-instrument. Ciò consente anche di contrattualizzare librerie di terze parti.

[banryu79]

Ciao Cesare, grazie per i tuoi interventi.


...
Pertanto scriverò dei test per mi aiutino a modellare tutto ciò. In buona sostanza e prendendo in prestito un po' di matematica, coi test posso controllare che a seguito di un certo input x la mia funzione f restituisca la y che mi aspettavo; questo per gli input e gli output che mi aspetto.

Tutto ciò nel DBC si traduce nella scrittura di codice di pre e post-condizione, e delle invarianti che tengono "sotto controllo" il contratto, appunto.

Sì, però tra le due metodologie vedo delle differenze.
Unit Test:
eseguiti a build-time e quando viene esplicitamente lanciata la test suite dal programmatore (mai eseguiti a runtime).
DBC:
eseguiti ad ogni runtime dell'applicazione mentre viene sviluppata/testata.
Unit Test:
la casistica di input posta a controllo è esclusivamente quella specificamente indicata nel sorgente delle unit test.
DBC:
l'input (pre-condizioni) controllato è esattamente e sistematicamente quello che effettivamente l'applicazione riceve, ad ogni runtime.

Per gli output (post-condizioni) di può fare un discorso analogo.
Per le invarianti il discorso è diverso.


Le invarianti con la TDD non si possono controllare, ma nemmeno ha senso farlo a mio avviso: quel che conta è che il codice si comporti per come mi aspetto che faccia.

Il controllo delle invarianti può avere scarso o nullo senso nella TDD, ma prima di procedere c'è da chiarire un malinteso. Fin'ora ho sempre parlato di Unit Test e non di TDD. Sono consapevole del fatto che le due cose non si equivalgono. E quando mi sono posto l'interrogativo se avesse senso affiancare entrambi gli "stili" mi riferivo al DBC e al solo unit test, così come quando ho riportato di aver avuto un'esperienza diretta dell'uso dei test per sviluppare un mio modulo in una applicazione; parlavo sempre di applicazione di unit testing.
Non mai sperimentato la TDD, di cui ho solo letto l'indispensabile per avere idea di cosa sia, e seguito con interesse i thread di pair programming in Diamonds.

Ritornando a ciò che hai scritto nel quote qua sopra, riflettendoci, il mio pensiero è che invece in certe condizioni ha molto senso controllare esplicitamente le invarianti.
Come già detto, penso sia importante ad esempio in ambito di programmazione multithreaded.
Se con le verifiche dello unit testing penso di assicurarmi che le invarianti della mia classe (eplicite o meno, di cui ho consapevolezza o meno) siano sempre rispettate [in tutti i momenti in cui le invarianti, in quanto tali, devono esserlo] rischio delle brutte sorprese (e questo vale anche per il TDD).

Comunque lascio fuori la TDD perchè, al pari del DBC, non vuole essere solo uno strumento di controllo, ma una metodologia che guida il processo di sviluppo del software: di conseguenza o uno ne adotta una o adotta l'altra.



D'altra parte, e come diceva sirus, ci sono casi non controllabili / testabili dal DBC, mentre con la TDD invece non ci sono problemi in tal senso.

Ho l'impressione che la TDD per certe cose si dimostri più "flessibile" del DBC.
Ma che comunque sia una metodologia diversa, che adotta mezzi diversi e dunque con finalità diverse (penso siamo comunque tutti d'accordo sul fatto che l'obiettivo ad "alto livello" sia sempre quello: garantire il più possibile la correttezza del software).


Altra cosa importante, con la TDD ho codice e test ben separati. Questo mi aiuta a capire cosa fa il codice perché non c'è altro in mezzo. I test mi aiutano, invece, a capire come usarlo. Soprattutto non mi devo preoccupare di togliere il codice di test quando vado in produzione, come col DBC: non c'è bisogno, essendo tutto separato.

Con il DBC supportato a livello di linguaggio non ti devi preoccupare del codice strettamente legato al controllo dei termini del "contratto": è disattivabile nel senso che poi in produzione non gira, dunque è a costo zero, tanto quanto i test.
Per quanto riguarda la chiarezza del codice direi che non c'è problema neanche nel DBC, quando supportato a pieno dal linguaggio: i controlli dei termini del contratto sono isolati in appositi "blocchi" dichiarativi che rendono cristallina la distinzione tra pre/post-condizioni/invarianti e codice "esecutivo".
Come in tutti gli idiomi, sarà solo questione di prenderci la mano, o meglio, di farci l'occhio.

[cdimauro]

Che le due metodologie siano diverse non v'è dubbio (parlavo, appunto, di "finalità" quando le presentavo come "simili"), e condivido la tua analisi. ;)