Prozeßsysteme

Zusammenfassung

Im vorangehenden Kapitel wurde bereits auf den Zusammenhang zwischen Spezifikation und Implementation eingegangen. Dabei wurde der spezielle Fall betrachtet, in dem lediglich die Zustandsdarstellung geändert wird, die Struktur der Modulklassen und ihrer Operationen aber bis auf die Formulierung der Initialisierungs-, PRE-, NBL- und EFFECTS-Prädikate unverändert bleibt. Damit kann die Spezifikation hinsichtlich der Zustandsdarstellung in eine maschinennahe Form gebracht werden. Im Rahmen einer Implementierung müssen darüber hinaus die NBL- und EFFECTS-Prädikate in eine Form gebracht werden, die den durch die Maschinenbefehle vorgegebenen Möglichkeiten entspricht. Im allgemeinen erfordert dies, einzelne Aktivitäten der Spezifikation in der Implementation durch mehrere zu ersetzen, die in geeigneter Reihenfolge auszuführen sind. Dadurch wird die funktionale Struktur verändert und man bezeichnet diese Vorgehensweise als funktionale Verfeinerung. Die Betrachtung der dabei auftretenden Probleme bildet den Schwerpunkt dieses Kapitels.