Hoare-Kalkül

10.12.2014, 18:35

neuling96

Hoare-Kalkül

x,k,result sind vom typ int

code:
1: 2: 3: 4: 5: 6: 7:	// 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 $[latex] result = x+\sum_{i=1}^{k-1} i[/latex]$

Dann lautet meine Gesamte invariante $[latex] result = x+\sum_{i=1}^{k-1}[/latex]$ i && k=<x
1) Beweis der invariant
( $[latex] result = x+\sum_{i=1}^{k-1}[/latex]$ i && k=<x && k<x)
{result = result +k; k= k+1;}
( $[latex] result = x+\sum_{i=1}^{k-1}[/latex]$ i && k=<x [/latex])

ergibt nach Anwendung der Zuweisungsregel folgende Beweisverpflichtung
( $[latex] result = x+\sum_{i=1}^{k-1}[/latex]$ 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 && $[latex] result = x+\sum_{i=1}^{k-1} i && && k<x)<br /> {}<br /> ( [latex] result +k = x+\sum_{i=1}^{k+1}[/latex]$ i && k+1=<x ) b.z.w
( $[latex] result = x+\sum_{i=1}^{k-1}[/latex]$ i && k+1=<x[/latex] )

Aus ( $[latex] result = x+\sum_{i=1}^{k-1}[/latex]$ i && k=<x && k<x) ->
( $[latex] result = x+\sum_{i=1}^{k} i [/latex]$ && k+1=<x[/latex])

ist wahr da k<x folgt k+1=<x

Neue Frage »

Antworten »

Hoare-Kalkül

Verwandte Themen