[Java] Verifikation von einem kleinen Programm

riverlove · 18. November 2007

Verifikation von einem kleinen Programm

Hey.. habe mehrere aufgaben letzte woche erhalten und darunter ist eine verifikation mit dem hoale kalkül.. ich verstehe es einfach nich :/ habe das jetzt mehrere stunden angeschaut aber irgendwie steckt für mich nich wirklich sinn dahinter. behindert ist das.

und zwar ist das programm:

Code:

Gegeben sei folgendes JAVA-Programm P, welches f¨ur eine Eingabe n ∈ IN =
{0, 1, 2, . . .} die Summe Pn
j=1 j2 berechnet:
i = n;
res = 0;
while (i > 0) {
res = res + i ∗ i;
i = i − 1;
}

die aufgabe dazu:

Code:

Vervollständigen Sie die Verifikation des Algorithmus P im Hoare-Kalkül, indem
Sie die unterstrichenen Teile ergäanzen. Hierbei dürfen zwei Zusicherungen
nur dann direkt untereinander stehen, wenn die untere aus der oberen folgt.
Hinter einer Programmanweisung darf nur eine Zusicherung stehen, wenn dies
aus einer Regel des Hoare-Kalküls folgt. Kennzeichnen Sie ihre benutzte Invariante
deutlich.

Also paar notizen erstmal.. eingabe= n; ausgabe = res; Vorbedingung = n >= 0; Nachbedingung= res = Summe von j=1 bis n für j^2

ahhh behindert. hilfeee

hab mal angefangen:

Code:

[RIGHT]< n >= 0 >
<n >= 0 und n = n>
[/RIGHT]
i = n;
[RIGHT]<n >= 0 und i = n >[/RIGHT]

so weiter komm ich nicht :/ verstehe das einfach nich

kann jemand das? ich glaub wenn man da durchblickt ist das noch nich mal schwierig.. ^^
danke bw ist selbstverständlich

Anzeige

Nützliche Suchen

[Java] Verifikation von einem kleinen Programm

Videos zum Themenbereich