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

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.