Verträge für Delphi / Design by Contract

[BUG]

Zitat von NamenLozer:

Doch, das ist theoretisch schon ein Problem. Angenommen, dein Contract wäre, dass ein kryptographischer Hash des Parameters nicht 0 sein darf. Also z.B. SHA1(Parameter) <> 0. Viel Spaß dabei, zur Compilezeit auszuwerten, welche Werte erlaubt sind.

Hashen zur Compilezeit ist nicht wirklich unmöglich (oder auch nur unüblich).

Aber ich glaube, mir ist eben des Halteproblemargument aufgegangen:
Es ist nicht aufgrund des Halteproblems nicht möglich, herauszubekommen, ob zwei Prozeduren (~> Turingmaschinen) das selbe Ergebnis liefern.
Also müsst der Programmierer im Zweifelsfall vor dem Aufruf explizit auf die gleiche Bedingung prüfen, die in dem Contract spezifiziert ist. Das wäre unschön (keine Perfektion).


Ich glaube aber, dass wirklich praktisch auftretende Problem ist, dass Contracts nur eine weitere Spezifikationen sind,
die unvollständig oder schlicht gänzlich falsch sein können.

[Namenloser]

Zitat von BUG:

Zitat von NamenLozer:

Doch, das ist theoretisch schon ein Problem. Angenommen, dein Contract wäre, dass ein kryptographischer Hash des Parameters nicht 0 sein darf. Also z.B. SHA1(Parameter) <> 0. Viel Spaß dabei, zur Compilezeit auszuwerten, welche Werte erlaubt sind.

Hashen zur Compilezeit ist nicht wirklich unmöglich (oder auch nur unüblich).

Darum geht es aber nicht. Der Parameter ist ja dynamisch. Sagen wir, der Parameter wäre der Rückgabewert einer Funktion, die alles zwischen 0 und MAXINT zurückliefern kann. Wie soll der Compiler feststellen, ob dabei was herauskommen kann, was von der kryptographischen Hashfunktion auf die 0 abgebildet wird?

[Phoenix]

Zitat von NamenLozer:

Darum geht es aber nicht. Der Parameter ist ja dynamisch. Sagen wir, der Parameter wäre der Rückgabewert einer Funktion, die alles zwischen 0 und MAXINT zurückliefern kann. Wie soll der Compiler feststellen, ob dabei was herauskommen kann, was von der kryptographischen Hashfunktion auf die 0 abgebildet wird?

Genau darum geht es letzten Endes:

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.

Wenn Du nun eine Variable aus A füllst und in B reinwirfst, dann kann Dir der Compiler eine Warnung um die Ohren hauen das dieses Ding Deinen Contract verletzt.

Du kannst nun entweder
* die Fälle von 6-10 mit einer Sonderbehandlung bedienen und nur die Werte bis 5 in B reinwerfen
* oder aber sicherstellen das A nur noch Werte zurückgibt die B auch annehmen kann
* oder aber dafür sorgen das B auch Werte bis 10 verträgt.

Machst Du nichts davon und ignorierst die Warnung einfach, DANN wirst Du möglicherweise zur Laufzeit Probleme bekommen.

Es geht ja nicht darum, vollumfänglich zur Compilezeit sicherzustellen das da nie was falsches reingegeben wird. Es geht darum, das Dir der Compiler vorab ausreichend Hinweise gibt wo es eben potentiell zu Contractverletzungen und damit zu möglichen Fehlerquellen kommen kann. So kann man nämlich vorher mögliche Problemfälle analysieren, automatisch testen und muss nicht erst warten bis es draussen irgendwo wegen einer seltsamen Eingabe mal in einem Edge-Case zu einem Fehler kommt.

[stahli]

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

[Meflin]

Zitat von Phoenix:

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.