Fernandos sagt: Hier fehlt eindeutig ein Hinweis darauf das Vorbedingung als auch der Artikel mit der Nachbedingung vom Hoare-Kalkül stammen!
