Programming by contract

man testet, ob (Teil-)Produkt seine Spezifikation erfüllt:

Kontrakt (Vertrag):

• wenn Vorbedingungen (an Programmzustand, Argumente) erfüllt,
• dann nach Arbeit des Produktes:

  Nachbedingungen (an Programmzustand, Resultat) erfüllt

eingebaut in Sprache Eiffel von Bertrand Meyer, http://www.eiffel.com/

Beispiel: Funktion merge (aus mergesort):

• wenn xs und ys jeweils aufsteigend geordnete Listen,
• dann gilt für zs = merge(xs, ys) :
  • zs ist aufsteigend geordnete Liste
  • zs ist Permutation von append(xs, ys)

Erfüllung des Kontrakts kann man

• testen (assert, JUnit, Eiffel)
• ...oder beweisen!