Forum: Die Delphi-IDE
by Meflin,
1. Jul 2013
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)
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...
Forum: Die Delphi-IDE
by Meflin,
26. Jun 2013
Sehe ich völlig anders. Compile-Time Checking von Contracts ist sicherlich ein nice to have, ist aber in der Perfektion äquivalent zur Lösung des Halteproblems (und ist damit unmöglich). Der wichtige Teil an Contracts ist also durchaus der zur Laufzeit ;) Es sei denn deine Aussage bezog sich jetzt wirklich absolut ausschließlich auf falsche Parameter. Dann kann ich nur sagen: Contracts können...
