Die Korrektheit von imperativen Programmen

Die Leserinnen sollen mit der Problematik eines Korrektheitsbeweises von Algorithmen vertraut gemacht werden und die Begriffe ‘Spezifikation’, ‘partielle Korrektheit’ und ‘totale Korrektheit’ verstehen lernen. Sie sollen nach Durcharbeitung des Kapitels in der Lage sein, vorgegebene Korrektheitsbeweise zu kommentieren, vor allem aber mit der grundsätzlichen Problematik vertraut sein: Um die Korrektheit eines Algorithmus untersuchen zu können, bedarf es einer klaren formalen Spezifikation, die als Ausgangspunkt für ein mathematisches Beweisverfahren dient. Das Durchprobieren eines Algorithmus mit einigen ausgewählten Eingabewerten kann niemals die Korrektheit eines Algorithmus sondern höchstens dessen Inkorrektheit (Finden eines Gegenbeispiels) beweisen.