Hoare Kalkül < Sonstiges < Hochschule < Informatik < Vorhilfe
|
| Status: |
(Frage) reagiert/warte auf Reaktion  | | Datum: | 14:34 So 11.11.2007 | | Autor: | Wimme |
| Aufgabe | Folgendes Programm soll mit Hilfe des Hoare Kalküls verifiziert werden:
i = 0;
res = 0;
while (i<n){
res = res + n;
i = i+1;
} |
Hallo!
Ich hoffe hier kennt sich jemand mit dem hoare Kalkül aus. Also ich bin soweit, dass ich glaube die Vorbedinung zur Schleifeninvariante gefunden zu haben: <n [mm] \geq [/mm] 0 [mm] \wedge [/mm] i=0 [mm] \wedge [/mm] res=0 >
Nun müsste die Schleifeninvariante ja sowas wie res = n [mm] \cdot [/mm] n sein.
Aber man erhält res = i [mm] \cdot [/mm] n.
Kann ich das aus meiner Vorbedingung folgern? bringt mich diese Schleifeninvariante überhaupt weiter? Ich habe ja gar nicht das gewünschte rechts stehen.
|
|
|
![[]](/images/popup.gif){kind=small}
Der Umgang mit dem Hoare-Kalkül zur Programmverifikation