Nachweis der Unvollständigkeit

{ R(x) }

while not( Z0(x) or Z1(x) ) do

x := f(x)

{ Z0(x) }

Dieses Programm ist

offensichtlich korrekt,

aber es kann nicht mit

dem Hoare Kalkül

bewiesen werden !

Ist die Datenstruktur nicht ausdrucksstark genug, dann ist der

Kalkül nicht vollständig. Das folgende Beispiel ist von M.Wand:

Vorherige Folie

Nächste Folie

Zurück zur ersten Folie

Graphik-Version anzeigen