1.7 Erzeugungsprinzip und Datenstrukturinvarianten
Wir hatten in Informatik I bereits die Wichtigkeit induktiv aufgebauter Datenstrukturen gesehen. Besonders interessant wird die induktive Erzeugung im Zusammenhang mit Datenstrukturinvarianten.
Man legt fest, daß nach außen nur diejenigen Elemente der Trägermengen eines Moduls verfügbar sind, die durch endlichmalige Anwendung seiner öffentlichen Methoden erzeugt werden können.
Damit können Eigenschaften der verfügbaren Modulelemente durch Induktion über die Anzahl der Erzeugungsschritte gezeigt werden. Insbesondere erfüllen alle verfügbaren Elemente die Datenstrukturinvariante des Moduls, wenn die öffentlichen Methoden sie erhalten.