Die Spezifikation kommt üblicherweise aus dem Entwurf bzw. den Anforderungen.
Zwei zentrale Eigenschaften:
Programm liefert die richtigen Ergebnisse, wenn es terminiert (partielle Korrektheit).
Programm terminiert für die zulässigen Eingaben.Beide Eigenschaften zusammen ergeben totale Korrektheit.
