Spezifikation
Algebraische Spezifikation
Abstrakte Datentypen werden festgelegt durch:
1. Syntax: Typen (types), Signaturen der Operationen (operations)
2. Semantik: Definierende Gleichungen (axioms), die Beziehungen zwischen den Operationen festlegen (und evtl. preconditions)
Die praktische Relevanz der Algebraischen Spezifikation ist eher gering, da es oft schwierig ist, Axiome zu
finden bzw. die Vollständigkeit oder Redundanz der Axiome zu überprüfen.
einige algebraische Spezifikationen: Beispiele
und noch mehr Beispiele
Modellierende Spezifikation
Abstrakte Datentypen werden festgelegt durch:
1. Typen: Wertemengen
2. Methoden: Kopf oder Signaturen inkl. pre- und postconditions (ggf. return/result)
3. Modell: mathematische Mengen, Folgen, (funktionale) Programmiersprache
4. Invariante: Modell muss bestimmte Invariante erfüllen
Die Spezifikation kann über Mittel der Prädikatenlogik, (Pseudo)-Code oder nat¨urliche Sprache erfolgen.
einige modellierende Spezifikationen: Beispiele
Anmerkungen
Links
Merkblatt zu abstrakte Datentypen und Spezifikation von Augustin