// Vorbedingung: x>=1
result = x;
while(k<x) {
result = result +k;
k= k+1;
}
// Nachbedingung: result=[latex] \sum_{i=1}^{x} i[/latex]
Ein Teil der invariante lautet
Dann lautet meine Gesamte invariante i && k=<x
1) Beweis der invariant
( i && k=<x && k<x)
{result = result +k; k= k+1;}
( i && k=<x [/latex])
ergibt nach Anwendung der Zuweisungsregel folgende Beweisverpflichtung
( i && k=<x && k<x)
{result = result +k; }
( result = x+\sum_{i=1}^{k} i && k+1=<x )
ergibt nach Anwendung der Zuweisungsregel folgende Beweisverpflichtung
( k=<x && i && k+1=<x ) b.z.w
( i && k+1=<x[/latex] )
