Programmieren = Beweisen

{ true }

x := 0 ;

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

n := n+1

{ false }

Remains to prove :

I(0)

I(n) Þ I(n+1)

I(n) Þ X(n)

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).

Datentyp Axiome

Vorherige Folie

Nächste Folie

Zurück zur ersten Folie

Graphik-Version anzeigen