Zur Spefizikation eines Unterprogramms
gehören die Angaben von Definitions- und Wertebereich,
denn Unterprogramme sind partielle Funktionen:
nicht einfach Daten Daten,
sondern z. B. f : Zahl String,
oder g : Zahl × String Zeichen,
oder h : balancierter Suchbaum × Zahl
balancierter Suchbaum usw.
Ein Typ ist eine Menge von Werten
mit gemeinsamen Eigenschaften. (z. B. ganze Zahlen, Zeichen, Zeichenketten)
Das Typsystem einer Programmiersprache soll sicherstellen,
daß diese Funktionen (Unterprogramme)
nicht außerhalb ihres Definitionsbereiches angewendet werden.
Die Idealvorstellung ist:
Programm ist typkorrekt
Programm ist überhaupt korrekt,