Hoare < Formale Sprachen < Theoretische Inform. < Hochschule < Informatik < Vorhilfe
|
| Status: |
(Frage) überfällig  | | Datum: | 21:06 Di 06.06.2006 | | Autor: | Fahnder |
| Aufgabe | | Zeigen Sie mittels Verifikationskalkül von Hoare die partielle Korrektheit. |
Hi!
Ich habe diese Frage in keinem Forum auf anderen Internetseiten gestellt.
Also leider habe ich gar keine Ahnung, wie man das Hoare anwendet. vielleicht könnte mir jemand das Pinzip mal erklären
Der Algorithmus ist
1 [mm] \to [/mm] y
0 [mm] \to [/mm] z
while z 6= n do
z + 1 [mm] \to [/mm] z
y · z [mm] \to [/mm] y
endwhile
y [mm] \to [/mm] fak
Dabei ist fak die n!-Fakultät
|
|
| |
|
| Status: |
(Mitteilung) Reaktion unnötig  | | Datum: | 13:45 So 20.08.2006 | | Autor: | fnatter |
Hoare ist einfache Logik.
z.B.
if (x>y)
diff = x-y;
else
diff = y-x;
du sollst beweisen dass das Programm korrekt ist, d.h. dass diff>=0
ist.
=> Vorbedingung: keine
Nachbedingung: diff >= 0
dann musst du beide "zweige" überprüfen, d.h.
- wenn x>y ist dann muss x-y positiv sein => ok
- wenn x<=y ist (die Umkehrung von x>y) dann muss y-x positiv sein => ok
=> fertig
Bei Schleifen arbeitest du mit Schleifeninvarianten, d.h. einer Bedingung
die beider jeder Schleifeniteration wahr ist.
z.B.
Eingabe: c
a = c
b = 0;
while (a>0) {
a--;
b++;
}
hier wäre inv= "a+b == c".
Dein beispiel ist etwas komplizierter, aber mit den einfachen Regeln zu lösen! Schau dir erstmal einfache Hoare-Beispiele (so wie das oben
angegebene) an!
Viel Erfolg!
|
|
|
| |
|
| Status: |
(Mitteilung) Reaktion unnötig | | Datum: | 04:11 Mi 23.08.2006 | | Autor: | Palin |
Ich glaube dein Problem ist es die Schleifen Invariante zu finden, da gibt es auch die Möglichkeit das Hoare Kalkul von hinten zu lösen.
du weist zum schluß ist y = fak(n) und n=z;
Ich mache es mal an einen andern bsp. deutlich
Ausgabe: res
Vorb. x>=0 und y >=0 und y|x (y telit x)
Nachb. y*res=y
Quellcode:
z=x;
res=0;
while(z != 0){
res=res+1;
z=z-y;
}
Am anfang Haben Haben wir unsere vorbedingungen also;
{x>=0 und y>=0 und y|x}
Bevor wir zur ersten Zeile kommen mussen wir sie um eine aussage ergenzen die auf jeden fall wahr ist zb 1=1, in unseren bsp. x=x.
Nun haben wir
{x>=0 und y>=0 und y|x und x=x }
Da nun im Quellcode
z =x;
folg für unsere "Zeile"
{x>=0 und y>=0 und y|x und Z=x }
Genauso machen wir es bei der näachsten Zeile
{x>=0 und y>=0 und y|x und Z=x und 0=0}
res = 0;
{x>=0 und y>=0 und y|x und Z=x und res=0}
Nun kommen wir zur Schleife und das Problem ist die Invariante raus zubekommen.
wir wissen nur {x>=0 und y>=0 und y|x und Z=x und res=0}, nun geh ich hin und schau mir meistens an was nach der Schleife steht.
hier also unser ergebnis y*res = x, ich weis vor der Schleife ist res = 0 und nach der Schleife ist z=0. Nun muss ich das noch in einen Zusammen hang bringen um die Schleifen Invariante zu bekommen, bei unseren bsp.
Vor der Schleife mit res =0 und z=x => y*res +z = y*0 +z =x
Nach der Schleife mit res = x/y und z = 0 => y*res+z = y*res+0=x
Das bestimmen der SChleifeninvariante ist meist sowas wie geziletes Raten, probier es ein paar mal und du wirst ein gefüh darfüt bekommen.
Ich schreib noch mal eben den rest des Kalkuls hin damit du ein Besp. hast.
Letzter Schrit war:
{x>=0 und y>=0 und y|x und Z=x und res=0}
=> {x>=0 und y>=0 und y|x und y*res+z =x}
while(z!=0){
{x>=0 und y>=0 und y|x und z!=0 (folgt aus der Schleife) y*res+z =0}
res um ein größer machen => z um y kleiner
{x>=0 und y>=0 und y|x und z!=0 und y*(res+1)+(z-y) =x}
res = res+1;
ersetzen res = res+1
{x>=0 und y>=0 und y|x und z!=0 und y*(res)+(z-y) =x}
z =z-y
Ersetzen
{x>=0 und y>=0 und y|x und z!=0 und y*(res)+ z =x}
}
Nach der Schleif z=0
{x>=0 und y>=0 und y|x und z=0 und y*(res)+ z =x}
{ z=0 und y*(res) =x}
{y*res =x}
MFG Palin
|
|
|
|
