Hoare-Kalkül |
10.12.2014, 18:35 | Auf diesen Beitrag antworten » | |||||
neuling96 | Hoare-Kalkül x,k,result sind vom typ int
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] ) Aus ( i && k=<x && k<x) -> ( && k+1=<x[/latex]) ist wahr da k<x folgt k+1=<x |
|||||
|
|
Verwandte Themen
Die Beliebtesten » |
|
Die Größten » |
|
Die Neuesten » |
|