Kompilierung von Vertrag in der Entwurfsprüfung?

Question

Ich habe gelesen, dass Compiler DBC bei der Kompilierung durchsetzen kann .. Wie es tut es?

Answer 1

Soweit ich weiß, die stärkste statische DbC Sprache so weit ist Spec # von Microsoft Research . Es verwendet ein leistungsfähiges statischen Analyse-Tool namens Boogie denen wiederum eine leistungsstarke Theorembeweisers / Constraint Solver genannt verwendet < a href = "http://Research.Microsoft.Com/projects/z3/" rel = "noreferrer"> Z3 entweder die Erfüllung oder Verletzung von Verträgen zur Entwurfszeit.

beweisen

Wenn das Theorem Prover beweisen können, dass ein Vertrag immer verletzt werden, das ist ein Übersetzungsfehler. Wenn der Satz Prover beweisen kann, dass ein Vertrag nie verletzt werden, das ist eine Optimierung. Die Vertragsüberprüfungen werden von der endgültigen DLL entfernt

Als Charlie Martin weist darauf hin, Verträge im Allgemeinen erweist entspricht das Halteproblem zu lösen und somit nicht möglich. So wird es eine Menge von Fällen, wo der Theorembeweisers weder beweisen noch den Vertrag zu widerlegen. In diesem Fall wird eine Laufzeitüberprüfung ausgesendet, so wie in anderen, weniger leistungsfähigen Vertragssystemen.

Bitte beachten Sie, dass Spec # wird nicht mehr weiterentwickelt. Der Vertrag Motor wird in eine Bibliothek, die so genannten -Code Contracts for .NET extrahiert wurde, der wird ein Teil sein von .NET 4.0 / Visual Studio 2010. Allerdings wird es keine Sprachunterstützung für Verträge sein.

Answer 2

kann der Compiler verwenden statische Analyse in Ihrem Programm zu schauen und festzustellen, ob es das tut das Richtige. Als einfaches Beispiel kann der folgende Code versuchen, die Quadratwurzel einer negativen Zahl zu (C ++):

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

Wenn die Compiler, dass sqrt wissen, soll nie mit einer negativen Zahl, könnte es moniert dies als Problem genannt werden, weil sie weiß, dass von Benutzereingaben zu lesen könnte eine negative Zahl zurück. Auf der anderen Seite, wenn Sie dies tun:

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

dann kann der Compiler sagen, dass dieser Code nicht immer sqrt mit einer negativen Zahl nennen.

Answer 3

Design by Contract ist ein sehr abstrakter Begriff, da es viel Spezifikation Formalismen mit unterschiedlicher Ausdruckskraft sein kann. Darüber hinaus gibt es eine Grenze, um die Fähigkeiten der statischen Analyse gegenwärtig zu überprüfen und Spezifikationen zu erzwingen. Es ist eines der aktivsten akademischen und industriellen Forschungsfelder in der Informatik.

In der Praxis ist es wahrscheinlich, dass Sie einige Teilmengen von Verträgen und Überprüfung verwenden, und das hängt von der Sprache, die Sie verwenden, und auf dem Plugins oder Programme, die Sie installieren.

In der Regel statische Analyse versucht, ein Modell des Vertrages, und ein Modell des aktuellen Programms zu bauen, und sie vergleichen. Zum Beispiel, wenn der Vertrag eine Funktion nicht zulässt aufrufe, wenn ein Objekt in dem Zustand S ist, wird es versuchen, in jeder Aufruf-Sequenz zu bestimmen, ob Sie in dem Zustand S könnten am Ende.

Answer 4

Welche Compiler und welche Sprache? Eiffel kann es bis zu einem gewissen Grad tun. Aber denken Sie daran, dass vollständig Durchsetzung Design-by-Vertrag würde in der Lage, meint das Halteproblem (Nachweis zu lösen. Annehmen, dass Sie einen Compiler, die es tun könnten, dann würde der Compiler in der Lage sein, eine beliebige Funktion mit einer echten Ausgangsbedingung zu identifizieren dass nicht die Austrittsbedingung erreichen wegen einer Endlosschleife oder Endlosschleife. So reduziert sie auf Anhalten.)

Was in der Regel damit gemeint ist, ist, dass, wenn Sie einen Anruf

  foo(a);

und irgendwo anders definieren

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

dann kann der Compiler prüfen, ob eine ist, in der Tat, im offenen Intervall zu gehen (0..128).

Answer 5

Einige Sprachen wie D maßen leistungsstarke Kompilierung konstantes Falten haben und Zeitbedingung kompilieren Überprüfung (für D static assert(boolCond, msg);, IIRC C / C ++ können #if und pragma oder #error verwenden)