Terminierung

/* Gauss's theorem */

{ N > 0 }

begin

k := 0;

sum := 0;

while k < N do [ N-k ]

{ sum = k*(k+1) div 2 and k <= N }

begin

k := k+1;

sum := sum + k

end

end

{ sum = N*(N+1) div 2 }

6. Remains to prove

k < N Þ k+1 £ N

4

4

4

4

Verification conditions

1. ..... ü

2. ...... ü

3. ...... ü

4. ...... ü

5. ...... ü

Vorherige Folie

Nächste Folie

Zurück zur ersten Folie

Graphik-Version anzeigen