Anwendung: Spezifikation und Programmverifikation

Eine der Hauptaufgaben der Informatik ist das Entwerfen von Algorithmen, also von effektiv ausführbaren Verfahren, die eine bestimmte Klasse von verwandten Problemen lösen. Von der höheren Schule her kennt man solche Verfahren in der Regel aus dem Geometrie-Unterricht. Typische Algorithmen sind hier das Halbieren einer Strecke oder das Fällen eines Lots nur unter Verwendung von Zirkel, Lineal und Bleistift. Die Informatik ist insbesondere an solchen Algorithmen interessiert, die mit Hilfe eines Computers ausgeführt werden können. Dazu werden sie in „Kunstsprachen“ formuliert, welche von Computern verstanden werden. Diese Kunstsprachen heißen Programmiersprachen, die in ihnen formulierten Algorithmen nennt man Programme und als Programmieren bezeichnet man das Entwerfen und Niederschreiben von Programmen. Letztere sollen natürlich eine Reihe günstiger Eigenschaften besitzen. Etwa sollen sie so geschrieben sein, dass man sie gut lesen und verstehen kann. Die entscheidende Eigenschaft aber, die Programme zu erfüllen haben, ist ihre Korrektheit, also die Eigenschaft, dass sie die Probleme, zu deren Lösung sie entworfen wurden, auch wirklich lösen. Insbesondere dürfen sie keine falschen Resultate produzieren. Um Anwendungen von den bisher behandelten mathematischen Konzepten in der Informatik zu demonstrieren, zeigen wir in diesem Kapitel ansatzweise, wie man mittels Mathematik die Korrektheit von Programmen formal beweisen kann. Diesem Gebiet ist ein großer Teil eines Informatik-Studiums gewidmet. Wir beschränken uns auf die imperative Programmierung.