Programm-Transformationen

Zusammenfassung

Wir wollen in diesem Kapitel eine Familie von Techniken diskutieren, die SETL besonders attraktiv macht, wenn es um die Konstruktion effizienter und korrekter Programme geht. Zunächst sollen Breitbandsprachen eingeführt werden; dann wollen wir SETL als Breitbandsprache identifizieren und zeigen, wie man davon mit Hilfe von Programm-Transformationen profitieren kann. Die Transformationen befassen sich im wesentlichen mit der Aufrechterhaltung von Invarianten, die auf verschiedene Weisen identifiziert werden. Sie lassen sich klassifizieren in top-down-Techniken, bei denen mengentheoretische Ausdrücke algebraisch manipuliert werden, und bottom-up-Techniken, bei denen ein Differentiationskalkül im Hintergrund steht. Beide Klassen von Transformationen werden durch ausführliche Beispiele illustriert: die algebraische Technik dient dazu, einen Algorithmus zur Speicherbereinigung herzuleiten, die Differentiationstechnik dazu, Algorithmen zur Berechnung des Zentrums eines freien Baums und von Zyklen in Graphen herzuleiten. Abschließend machen wir einige Bemerkungen im Hinblick auf neuere Entwicklungen.