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
?