Formale Spezifikationen: Über Instruktionen hinaus, das Definieren von Softwareverhalten
Dieser Beitrag untersucht den Unterschied zwischen formalen Spezifikationen und traditionellen Programmen. Während Programme Listen von Anweisungen sind, sind formale Spezifikationen Mengen von Verhaltensweisen. Anhand eines Zählerbeispiels veranschaulicht der Autor, wie Spezifikationen alle korrekten Verhaltensweisen definieren und die Mengenlehre verwenden, wobei Generatoren (Init und Next) verwendet werden, um unendliche Mengen von Verhaltensweisen zu beschreiben. Dies steht im Gegensatz zum Konzept des Nichtdeterminismus in der Programmierung; in formalen Spezifikationen bezieht sich Nichtdeterminismus auf die verschiedenen Möglichkeiten, wie ein Verhalten erweitert werden kann, während er in Programmen sich auf unsichere Codepfade bezieht. Der Artikel betont das Verständnis formaler Spezifikationen als Mengen von Verhaltensweisen, was für das Debugging und die Interpretation von Fehlern des Modellprüfers entscheidend ist.