Der "Nicht-Eiffel" -Teil Ihrer Frage ist interessant. Verträge haben ihren ganzen Sinn, wenn sie in der Programmiersprache unterstützt werden, sonst ist es nur eine nette Syntax für Kommentare.
Das bringt uns zu den Sprachen, die Verträge unterstützen. Ich weiß von drei außer Eiffel:
Die ersten beiden haben ausführbare Aufträge verwenden. Vorteile: Kann als Laufzeit-Assertions verwendet werden. Nachteile: Es fehlt die Ausdruckskraft, um vollständig zu spezifizieren, was eine Funktion in einem Vertrag tut. Sie können grundsätzlich nur Gesundheitschecks schreiben.
ACSL-Verträge auf der anderen Seite sind expressiver und nicht ausführbar. Sie ermöglichen es, vollständig anzugeben, dass eine Sortierfunktion immer enden soll, und dieselben Elemente wie in dem ursprünglichen Array in der Reihenfolge zu belassen. ACSL-Verträge können für die statische Analyse verwendet werden, insbesondere für die Berechnung der schwächsten Vorbedingungen im Hoare-Stil.
Und nur mit dem letzten wirklich vertraut zu sein (Disclaimer: Ich arbeite an Frama-C, aber der ACSL Teil ist die Arbeit von vielen Menschen, von denen einige viel mehr als ich beigetragen haben), kann ich nur Erwähnen Sie "ACSL by example", eine Open-Source-C-Bibliothek mit ACSL-Verträgen, die derzeit von Fraunhofer FIRST entwickelt wird. Es ist noch nicht veröffentlicht, aber es wird als Teil des Projekts Device-soft sein. Ich bin sicher, dass Sie eine vorläufige Version bekommen könnten, wenn Sie interessiert wären. Fühlen Sie sich frei, die Person zu kontaktieren, die als Kontakt auf der letzten Webseite erwähnt wird.
Die D-Programmiersprache unterstützt standardmäßig Verträge. Es gibt Bibliotheken zum Hinzufügen von Verträgen zu Python und Ruby, und selbst C/C++ hat Unterstützung durch GNU Nana. Aber ich weiß nicht, ob jemand diese wirklich benutzt. Ich interessiere mich besonders für Java und C# /. NET. –