Hoare-Kalkül

Neue Frage »

Auf diesen Beitrag antworten »
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 »


Verwandte Themen

Die Beliebtesten »
Die Größten »
Die Neuesten »