|
|
Programmverifikation
1. Begriff der Informatik: a) formale Vorgehensweise mit dem Ziel, die Korrektheit eines Programms bzw. Moduls zu beweisen; b) Forschungsgebiet, das sich mit Methoden des Korrektheitsbeweises beschäftigt. - 2. Motivation: Da mit dem gebräuchlichen Testen eines Programms die Korrektheit nicht garantiert werden kann, wurde nach Möglichkeiten gesucht, als Ersatz oder in Ergänzung die Korrektheit durch theoretische Analyse des Programmtexts zu beweisen. - 3. Voraussetzungen: a) eine formale Spezifikation der Aufgabe des Programms bzw. Moduls; b) eine formale Beschreibung der Semantik einer Programmiersprache: (1) axiomatische Semantik (Prädikatensemantik) oder (2) denotationale Semantik (Funktionensemantik). - 4. Vorgehensweise: a) Auf der Grundlage einer axiomatischen Semantik versucht man, durch syntaktische Analyse des Programmtexts zu beweisen, daß bestimmte logische Aussagen für die Ausgangsgrößen des Programms gelten unter der Voraussetzung, daß bestimmte logische Aussagen für die Eingangsgrößen gelten. Grundlage der Analyse sind Festlegungen, wie die einzelnen Sprachkonstrukte logische Aussagen transformieren; die Festlegungen bezeichnet man als die axiomatische Semantik der Programmiersprache. - b) Die denotationale Semantik einer Programmiersprache ist eine komplexe mathematische Beschreibung des Funktionenraums, der für jedes Programm der Sprache angibt, welche Funktion dieses berechnet. Es existieren aufwendige Verfahren, um aufgrund dieser Beschreibung beweisen zu können, welche Funktion ein konkretes Programm berechnet, d. h. ob es korrekt i. S. der Spezifikation ist. - 5. Vorteil: Korrektheit wird bewiesen, nicht nur unterstellt wie beim Testen. - 6. Nachteil: Programmverifikation von Hand ist extrem aufwendig; läßt sich nur bei sehr kleinen Programmen anwenden, bei größeren Programmen nicht praktikabel. Intensive Forschungsbemühungen in der Informatik, die Programmverifikation so weit wie möglich zu automatisieren.
<< vorheriger Begriff |
|
nächster Begriff>> |
|
|
|
Diese Seite bookmarken :
|
|
