Programming by contract

jedes (Teil-)Produkt muß seine Spezifikation erfüllen, diese ist ein Kontrakt (Vertrag):

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

  Nachbedingungen (an Programmzustand, Resultat) erfüllt

eingebaut z. B. 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 soll man

• beweisen (verifizieren) ...
• ...und wer das nicht kann, dem bleibt nur mehr oder weniger systematisches Raten, genannt testen (assert, JUnit, Eiffel ..., siehe später)