Spezifikationen

Zusammenfassung

Um formal mit Datenstrukturen und Algorithmen umgehen zu können, verwenden wir sogenannte Spezifikationen: Für eine Menge S von Sortensymbolen, eine S-sortierte Signatur Σ und eine endliche Menge Φ geschlossener Σ-Formeln ist das Tripel S=(S,Σ,Φ) eine Spezifikation.¹ Die Formeln in Φ werden die Axiome von S genannt. Eine Σ-Algebra M ist ein Standardmodell der Spezifikation S genau dann, wenn M ein Standardmodell von Φ ist. S ist eine zulässige Spezifikation genau dann, wenn S ein bis auf Σ-Isomorphie eindeutiges Standardmodell besitzt.