Formale Spezifikation

Eine formale Spezifikation ist die Beschreibung eines Computerprogramms mittels einer Notation, deren Semantik eindeutig definiert ist (einer sogenannten formalen Sprache). Ziel ist die formalisierte, präzise Beschreibung der zu lösenden Aufgabe in einem in sich konsistenten und geschlossenen Modell, um dieses weiterzuverarbeiten.

Mit Hilfe von Zusatzwerkzeugen kann die Einhaltung der Regeln der formalen Sprache und die Integrität des Modells geprüft werden. Weitere Werkzeuge können eine Transformation des Modells in andere formale Sprachen bewirken, z. B. Programmiersprachen, die wiederum mit Compilern in auf Computern ausführbaren Maschinencode übersetzt werden können.

Die Z-Notation ist ein Beispiel für eine formale Spezifikationssprache. Andere sind die Specification Language(VDM-SL) der Vienna Development Method und die Abstract Machine Notation (AMN) der B-Methode.