Schleifeninvariante < Algor.+Datenstr. < Theoretische Inform. < Hochschule < Informatik < Vorhilfe
|
| Aufgabe | divide(a,b)
int r := a;
int d := 0;
while [mm] r\le [/mm] b do
r := r-b;
d := d+1;
return [d,r];
Es soll eine geeignete Vor- und Nachbedingung gefunden werden sowie eine Schleifeninvariante. Benutzen Sie ihre Bedingungen um die Korrektheit des Algorithmus nachzuweisen. |
Hallo Leute,
ich habe hier Probleme beim Nachweis der Korrektheit.
Meine Ergebnisse bis jetzt:
Vorbedingung = {a [mm] \ge [/mm] 0 ; b>0}
Schleifeninvariante: P(a=r+b*d)
Nachbedingung = {d= [mm] \lfloor \frac{a}{b}\rfloor [/mm] ; r=mod( [mm] \frac{a}{b} [/mm] )}
Jetzt muss ich doch die Gültigkeit der Invariante vor Eintritt in die Schleife, in der Schleife und nach der Schleife zeigen oder?
Kann man es so machen z.B.
vor Schleifeneintritt:
{ [mm] a\ge0, [/mm] b>0}
r := a ; d := 0
$ [mm] \{ a=a'=r+d*b=r'+d'*b'\}$
[/mm]
Ich habe gelesen, dass man irgendwie P [mm] \wedge [/mm] B nachweisen muss, aber mein B in dieser while- Schleife [mm] (r\le [/mm] b ) gilt doch überhaupt nicht mehr nach Schleifenaustritt. :-(
Kann mir vielleicht jemand weiterhelfen?
Vielen Dank im Voraus!
|
|
| |
|
| Status: |
(Mitteilung) Reaktion unnötig  | | Datum: | 12:20 Do 19.12.2013 | | Autor: | matux |
$MATUXTEXT(ueberfaellige_frage)
|
|
|
|
