formale Spezifikation

1. Begriff: im Software Engineering eine Methode der Spezifikation, bei der die Aufgaben eines Moduls (schwieriger: eines Softwaresystems) formal definiert werden, z.B. axiomatisch.

2. Vorteil: Exakte Vorgabe für die Implementierung; ausgehend von einer formalen Spezifikation kann u.U. ein formaler Beweis geführt werden, dass die Implementierung mit der Spezifikation übereinstimmt. (Programmverifikation).

3. Nachteil: Nur für kleinere Aufgaben und von formal geschulten Informatikern einsetzbar, sehr aufwendig.

4. Bedeutung: In der Informatik intensive Forschungsaktivitäten; in der Praxis noch geringe Bedeutung.