Programmieren = Beweisen

{ true }

x := 0 ;

while X(n) do { I(n) }

n := n+1

{ false }

abstrakte Invariante I

Eine Eigenschaft X gilt für alle natürlichen Zahlen gdw.

ein Programm, das ein Gegenbeispiel sucht, terminiert nicht :

Suche nach einem Gegen-

beispiel für "n.X(n).

Vorherige Folie

Nächste Folie

Zurück zur ersten Folie

Graphik-Version anzeigen