Algebraische Spezifikation Vorlesung an der Fakult"at f"ur Mathematik und Informatik der Universit"at Leipzig 1

Dr. Rolf Hartwig gelesen im Sommersemester 1993 und Wintersemester 1996/97

1nach einer vom Autor durchgesehenen Mitschrift von stud.inf. Dirk Weigenand Quelle: http://www.informatik.uni-leipzig.de/,rhartwig/ Der Autor ist jederzeit f"ur inhaltliche Hinweise zur Verbesserung der Vorlesung als auch f"ur Hinweise zu immer noch verbliebenen Druckfehlern dankbar.

Inhaltsverzeichnis 1 Einf"uhrung 1

1.1 Spezifikationen im Software-Lebenslauf . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1 1.2 Datentypen und abstrakte Datentypen . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2 1.3 Spezifikationsmethoden . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4

2 Terme, Gleichungen, Gleichungsspezifikationen 7 3 Initialit"at 11 4 Gleichungskalk"ul und Induktion 17 5 Erweiterung von Gleichungsspezifikationen 21 6 Finale Semantik und beobachtbares Verhalten 29 7 Implementation von Spezifikationen 39 Index 43

I

Kapitel 1 Einf"uhrung Im Softwarelebenszyklus gibt es Phasen, in denen eine Spezifikation (der Anforderungen an das Produkt, des Problems, der Programme) erforderlich oder w"unschenswert ist.

1.1 Spezifikationen im Software-Lebenslauf

1. Problemspezifikation:

ffl Leistungsbeschreibung ffl Pflichtenheft ffl Anforderungsdefinition

z.B. als Grundlage eines Vertrages zwischen Auftraggeber und -nehmer. Dies ist noch keine Grundlage zum sofortigen Erstellen einer Software, sondern f"ur die Erstellung einer formalen Spezifikation. Die Beschreibung des Modells erfolgt in dieser Stufe verbal.

2. Systemspezifikation:

Ist Resultat des Systementwurfs und Grundlage des Implementierungsprozesses. Zur Beschreibung sind formale und halbformale Methoden zweckm"assig.

3. Programmspezifikation:

Anforderungsbeschreibung der Einzelprogramme des Systems nach dessen Modularisierung.

4. Datentypspezifikation:

Teil der Programmspezifikation; zweckm"assig beim Entwurf von Programmmen als Algorithmen "uber Datenstrukturen.

Aufgaben einer Spezifikation: