Grundlagen der Systementwicklung

Material

Folien

Data-Oriented Specification Development

Introduction. PDF
History, Signatures for Interface Descriptions. PDF
Functional Models: Interpretation of Interfaces through Structures. PDF
Algebraic Specifications, Maude, Order-sorted Signatures and Specifications. PDF
Equational Deduction, Confluence, Canonical Term Algebras. PDF
Constructor Subsignatures, Equational Simplification modulo Equations. PDF
Konfluenz und Terminierung. PDF
Parametrisierung. PDF
Change of Data Structures. PDF
Transitionssysteme. PDF
State-Based Systems in Maude. PDF
TLA. PDF
TLA: Verfeinerung und Strukturierung. PDF
MTLA. PDF
Maude und TLA. PDF

Skript

Vor fünf Jahren entstand ein Skript zur Vorlesung, das hier als PDF-Datei oder als Druckvorlage ( gzip-te Postscript-Datei, zweispaltig) zur Verfügung steht.

Warnung:

Das Skript ist noch nicht korrigiert. Für Hinweise auf Fehler und Verbesserungsvorschläge sind wir dankbar.
Der Teil über die Spezifikationssprache Z im Skript ist für die Vorlesung nicht relevant.
Es wird Maude statt CASL verwendet (die Folien geben hier die korrekte Auskunft, es handelt sich vor allem um syntaktische Änderungen).

Weiterführende Unterlagen

Maude: Maude-Schnelleinstieg: Extra-Seite auf diesem Server mit Informationen zu Maude

Literatur

J. Loeckx, H. Ehrich, M. Wolf: Specification of Abstract Data Types. Wiley & Teubner, 1996.
M. Wirsing: Algebraic specification. In J. van Leeuwen (ed.): Handbook of Theoretical Computer Science. Elsevier, Amsterdam, 1990.
C. Morgan: Programming from Specifications. Prentice Hall, 3. Auflage, 1998.
Z. Manna, A. Pnueli: The temporal logic of reactive and concurrent systems - specification. Springer-Verlag, New York, 1992 (vergriffen, in der Bibliothek vorhanden).
L. Lamport: TLA - The Temporal Logic of Actions.; Zusammenfassung von TLA, von der TLA-Homepage entliehen, gibt einen Kurzüberblick über die Sprache.
SML: Empfehlenswert ist vor allem Larry Paulsons Buch ML for the working programmer (Cambridge Univ. Press, 2. Auflage, 1996). Weitere Informationen, insbesondere zu dem am CIP-Pool installierten SML-Interpreter, enthält die Homepage von SML/NJ.

GSE < Lehrstuhl < Institut < Universität

Axel Rauschmayer