This is a textbook on program verification. It concentrates on those verification methods that have now become classic such as the inductive assertions method of Floyd, the axiomatic method of Hoare and Scott's fixpoint induction. The aim of the book is to present these different verification methods and to explain their mathemati cal background. The subject is treated with mathematical precision, and many examples are included. Throughout the book the same examples will reappear to illustrate how the different methods are related. The material is self-contained and accessible without prior...

Dieses Buch behandelt Grundlagen von Programmiersprachen, deren Verknupfung mit realen Rechenmaschinen und - exemplarisch - Algorithmen. Das Ziel des Buches ist es, eine solide Basis fur das Studium der Informatik zu legen. Es ist ins besondere fur Studenten im Grundstudium des Studienganges Informatik gedacht. Ein Programm ist nur dann brauchbar, wenn es das gestellte Problem korrekt lost, und dies daruber hinaus mit der gewunschten Effizienz tut. Aussagen uber die Korrektheit und Effizienz eines Programms sind nur dann moglich, wenn die verwendete Programmiersprache exakt definiert ist,...