man testet, ob (Teil-)Produkt seine Spezifikation erfüllt: diese ist ein Kontrakt (Vertrag):
Nachbedingungen (an Programmzustand, Resultat) erfüllt
eingebaut z. B. in Sprache Eiffel von Bertrand Meyer, http://www.eiffel.com/
Beispiel: Funktion merge (aus mergesort):
xs
und ys
jeweils aufsteigend geordnete Listen,
zs = merge(xs, ys)
:
zs
ist aufsteigend geordnete Liste
zs
ist Permutation von append(xs, ys)