Registrierung Kalender Mitgliederliste Teammitglieder Suche Häufig gestellte Fragen Zur Startseite

Informatiker Board » Themengebiete » Praktische Informatik » Hoare-Kalkül » Antwort erstellen » Hallo Gast [Anmelden|Registrieren]

Antwort erstellen
Benutzername: (du bist nicht eingeloggt!)
Thema:
Nachricht:

HTML ist nicht erlaubt
BBCode ist erlaubt
Smilies sind erlaubt
Bilder sind erlaubt

Smilies: 21 von 33
smileWinkDaumen hoch
verwirrtAugenzwinkerngeschockt
Mit ZungeGottunglücklich
Forum Kloppebösegroßes Grinsen
TanzentraurigProst
TeufelSpamWillkommen
LehrerLOL HammerZunge raus
Hilfe 
aktuellen Tag schließen
alle Tags schließen
fettgedruckter Textkursiver Textunterstrichener Text zentrierter Text Hyperlink einfügenE-Mail-Adresse einfügenBild einfügen Zitat einfügenListe erstellen CODE einfügenPHP CODE farbig hervorheben
Spamschutz:
Text aus Bild eingeben
Spamschutz

Der letzte Beitrag
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