Compilare il controllo del tempo in Design per contratto?

Question

Ho letto che il compilatore può imporre dbc al momento della compilazione .. Come lo fa?

Answer 1

Per quanto ne so, il linguaggio DbC statico più potente finora è Spec # di Microsoft Research . Utilizza un potente strumento di analisi statica chiamato Boogie che a sua volta utilizza un potente Teorema Prover / Constraint Solver chiamato < a href = "http://Research.Microsoft.Com/projects/z3/" rel = "noreferrer"> Z3 per dimostrare l'adempimento o la violazione dei contratti in fase di progettazione.

Se il Teorema Prover può provare che un contratto sarà sempre violato, si tratta di un errore di compilazione. Se il Teorema Prover può dimostrare che un contratto non verrà mai violato , si tratta di un'ottimizzazione: i controlli del contratto vengono rimossi dalla DLL finale.

Come sottolinea Charlie Martin, dimostrare i contratti in generale equivale a risolvere il problema dell'arresto e quindi non è possibile. Quindi, ci saranno molti casi in cui il Teorema Prover non può né provare né confutare il contratto. In tal caso, viene emesso un controllo di runtime, proprio come in altri sistemi di contratto meno potenti.

Si noti che Spec # non è più in fase di sviluppo. Il motore del contratto è stato estratto in una libreria, denominata Contratti di codice per .NET , che farà parte di .NET 4.0 / Visual Studio 2010. Tuttavia, non ci sarà supporto linguistico per i contratti.

Answer 2

Il compilatore può utilizzare analisi statica per esaminare il programma e determinare se esegue cosa giusta. Come semplice esempio, il codice seguente potrebbe provare a prendere la radice quadrata di un numero negativo (C ++):

double x;
cin >> x;
cout << sqrt(x) << endl;

Se il compilatore sa che sqrt non deve mai essere chiamato con un numero negativo, potrebbe segnalarlo come un problema perché sa che la lettura dall'input dell'utente potrebbe restituire un numero negativo. D'altra parte, se lo fai:

double x;
cin >> x;
if (x >= 0) {
    cout << sqrt(x) << endl;
} else {
    cout << "Can't take square root of negative number" << endl;
}

allora il compilatore può dire che questo codice non chiamerà mai sqrt con un numero negativo.

Answer 3

Design by Contract è un termine molto astratto, poiché possono esserci molti formalismi di specifica con diversi poteri espressivi. Inoltre, esiste attualmente un limite alle capacità dell'analisi statica di controllare e applicare le specifiche. È uno dei campi di ricerca accademica e industriale più attivi nell'informatica.

In pratica, è probabile che utilizzerai alcuni sottogruppi di contratti e controlli, e ciò dipende dalla lingua che stai utilizzando e dai plug-in o dai programmi installati.

In generale, l'analisi statica cerca di costruire un modello del contratto e un modello del programma effettivo e confrontarli. Ad esempio, se il contratto non ti consente di invocare una funzione quando un oggetto si trova nello stato S, proverà a determinare se in qualsiasi sequenza di invocazione potresti finire nello stato S.

Answer 4

Quale compilatore e quale lingua? Eiffel può farlo in una certa misura. Ma ricorda che applicare completamente il progetto per contratto significherebbe essere in grado di risolvere il problema dell'arresto (prova: supponi di avere un compilatore che potrebbe farlo. Quindi il compilatore dovrebbe essere in grado di identificare una funzione arbitraria con una vera condizione di uscita che non è in grado di raggiungere la condizione di uscita a causa di un loop infinito o di una ricorsione infinita. Quindi si riduce all'arresto.)

Ciò che di solito si intende con questo è che se hai una chiamata

  foo(a);

e da qualche altra parte definiscono

  function foo(a:int) is
     assert 0 < a && a < 128
     ...
  end

quindi il compilatore può verificare che a sia, in effetti, sarà nell'intervallo aperto (0..128).

Answer 5

Alcune lingue come D hanno una costante di tempo di compilazione ragionevolmente potente e il controllo delle condizioni di tempo di compilazione (per D static assert (boolCond, msg); , IIRC C / C ++ possono usare #if e pragma o #error )