Semantik und Programmverifikation

Frontmatter

1. Formale Grundlagen

Zusammenfassung

In diesem Kapitel werden diejenigen formalen Grundbegriffe eingeführt, die in den nachfolgenden Abschnitten erforderlich sind. Wir verwenden Konzepte der sortierten Prädikatenlogik erster Stufe, um funktionale Programme zu definieren, ihre Semantik zu formalisieren und Korrektheitsaussagen über diesen Programmen zu formulieren.

Christoph Walther

2. Funktionale Programme

Zusammenfassung

Bevor wir uns mit der Verifikation von Programmen auseinandersetzen, müssen wir festlegen, welche Programmiersprachen betrachtet werden sollen. Wir unterscheiden hierfür zwischen verschiedenen Programmierparadigmen, wie etwa den logischen, den imperativen und den applikativen Programmiersprachen. Kennzeichnend für logische Sprachen, wie etwa Prolog, ist

• die Repräsentation des Programmcodes sowie eines Aufrufs des logischen Programms durch (bestimmte) prädikatenlogische Formeln, sowie
• die Verwendung eines geeignet eingerichteten Automatischen Beweisers zur Berechnung eines Beweises, daß der Programmaufruf logisch aus den Formeln des Programms folgt, wobei
• aus dem Beweis das Ergebnis der Programmausführung abgelesen wird.

Christoph Walther

3. Verifikation funktionaler Programme

Zusammenfassung

Nachdem wir in Kapitel 2 die Semantik funktionaler Programme definiert haben, können wir nun daran gehen, Aussagen über solche Programme zu beweisen, also funktionale Programme zu verifizieren. Dabei unterscheiden wir zwischen

• Aussagen, die sich direkt auf ein funktionales Programm P beziehen, und
• Aussagen über die Funktion sem[[P]], die durch P definiert wird.

Christoph Walther

Backmatter