Verträge für Delphi / Design by Contract

[stahli]

[OT]... Danke! Jetzt habe ich endlich ungefähr verstanden, worüber Ihr die ganze Zeit redet. :thumb:[/OT]

[Meflin]

Zitat:

Zitat von Phoenix (Beitrag 1220256)

Du hast eine Funktion A die gemäß Contract einen beliebigen Wert zwischen 1 und 10 zurückliefern kann.
Du hast eine andere Funktion B, die einen Parameter hat der per Contract nur Werte zwischen 0 und 5 annehmen darf.

Das Problem ist auch nicht unbedingt die Stelle zwischen "Nachbedingung A" und "Vorbedingung B", sondern die zwiwschen "Methode A" und "Nachbedingung A". Nehmen wir z.B. eine Methode wie (Pseudocode)

Code:

function randInt(max: Int): Int = {
    return Random.nextInt(max);
}
ensures: result <= max

Kann das dein konkreter Compile-Time Analyzer korrekt erkennen, oder liefert er, wovon ich in diesem Beispiel spontan ausgehen würde, ein false positive (im Sinne einer Warnung: Nachbedingung ist nicht sichergestellt). Dann will ich das nicht wirklich haben, weil wenn dann die statische Analyse zu einem Haufen Warnungen führt, die keine sein sollten, neigt man ja schnell wieder dazu, solche Warnungen gleich allgemein tendentiell eher zu ignorieren. Und selbst wenn es in diesem konkreten Beispiel funktioniert, gibt es doch genug (oder bessergesagt unendlich viele) Fälle, in denen es einfach nicht funktionieren kann.

Zur Compilezeit hilft mir aber eine Analyse hauptsächlich, wenn sie entweder zu 100% ausschließen kann, dass ein Vertrag verletzt wird (denn dann kann ich den Vertrag eliminieren) oder aber erkennen kann, dass ein Vertrag zwangsläufig verletzt wird. Den Mehrwert von Erkenntnissen in der Welt dazischen zur Compilezeit wage ich zu bezweifeln. Denn wenn ich o.g. Beispiel dann so schreibe, dass der Vertrag immer erfüllt wird, dann führt das zu absolut sinnbefreitem Code.

Apropos: die bisher genannten Beipsiele sprechen für mich eher gegen das verwendete Typsystem als für Verträge. Denn wenn es ein gutes Typsystem wäre, könnte ich dann nicht Dinge wie "kann oder kann nicht nil sein" oder aber "Zahl im Wertebereich X" auch direkt über die Typen ausdrücken ;) ?

[Phoenix]

Die korrekte Funktion der Methode und die Voraussetzung das sie ihren Contract einhält würdest Du mit Unit-Tests abdecken.

Daher ist die Prüfung des 'Innenverhältnisses' des Vertrages nicht so relevant. Das 'Aussenverhältnis' ist das, was für eine solche Codeanalyse wirklich relevant ist.

Wenn die Nachbedingung nicht passt weil Dein Random.NextInt(max) sich falsch verhält und Werte > max liefert, dann wird das klar erst zur Laufzeit auffallen. Aber in aller Regel wird sowas eben entsprechend gut getestet sein damit das nicht passiert.

[himitsu]

Zitat:

Zitat von jaenicke (Beitrag 1219786)

Auch Addons kenne ich dafür nicht

Da es in Delphi leider "keine" Möglichkeit gibt, um einen PreCompiler reinzuhängen, wird es sowas auch nie geben können.

Wobei ich mich grade frage, wie das Eurekalog und vorallem AQTime machen?

[jaenicke]

Zitat:

Zitat von himitsu (Beitrag 1237895)

Zitat:

Zitat von jaenicke (Beitrag 1219786)

Auch Addons kenne ich dafür nicht

Da es in Delphi leider "keine" Möglichkeit gibt, um einen PreCompiler reinzuhängen, wird es sowas auch nie geben können.

Gibt es durchaus. Siehe DLangExtensions usw.
Und über die Tools-API ist glaube ich nun mittlerweile noch mehr möglich.