10.3

[kambo]

hier meine Lösung....

edit
hab die Lösung verbessert
/edit
lg
kambo

[piet]

Danke
Du hast nicht zufällig noch ein paar Lösungs-PDFs bei dir daheim rumliegen? ;)

[NeoCortex]

Danke für die tolle ausgearbeite Lösung! :thumb:

Nur, sollte das erste P nicht y > a sein?


edit: ok, blödsinn, ich denke, ich hab's schon verstanden. Wegen der Invariante x + y > a sowie y > a folgt ja, dass y > 0 sein muss in N.
Oder? :confused:

[kambo]

Nur, sollte das erste P nicht y > a sein?


edit: ok, blödsinn, ich denke, ich hab's schon verstanden. Wegen der Invariante x + y > a sowie y > a folgt ja, dass y > 0 sein muss in N.
Oder? :confused:
hmmm.......ehrlich gesagt verstehe ich nicht, was du meinst http://hades.gothic.at/iforum/images/smilies/confused.gif
"Das erste P" ist y>0 was wir schon am Anfang feststellen können.

[NeoCortex]

hmmm.......ehrlich gesagt verstehe ich nicht, was du meinst http://hades.gothic.at/iforum/images/smilies/confused.gif
"Das erste P" ist y>0 was wir schon am Anfang feststellen können.


Naja, ich der Angabe steht ja y > a {begin ..... end} x > a
und ich hab mich halt gefragt, wie du von y > a auf y > 0 kommst, ob du das aus der gegebenen Invarante x + y > a ableitest.
Wenn ja bleibt nur die Frage, warum dann x > a bleibt? :confused:

[kambo]

S*****
ich hab nicht gesehen dass die Invariante schon gegeben ist!! Außerdem habe Angabe falsch abgeschrieben :hewa:
Also die Beweise der Gültigkeit sind falsch.....

ich habe mir folgendes überlegt:

Invariante : x + y > a (a=2)

(1)
(( P and (x = 0)) impliziert I

((y > a ) and (x=0)) impliziert (x+y>2) die rechte Seite ist gültig in N, da in den natürlichen Zahlen 0 + 3 > 2 gilt (a=2 , y=3 => y>a)

Man muss nicht die in der Angabe gegebene Bedingung x>a berücksichtigen , oder?

[NeoCortex]

ich habe mir folgendes überlegt:

Invariante : x + y > a (a=2)

(1)
(( P and (x = 0)) impliziert I

((y > a ) and (x=0)) impliziert (x+y>2) die rechte Seite ist gültig in N, da in den natürlichen Zahlen 0 + 3 > 2 gilt (a=2 , y=3 => y>a)

Man muss nicht die in der Angabe gegebene Bedingung x>a berücksichtigen , oder?
Muss man dazu überhaupt Zahlen einsetzen, bzw. wie kommst du auf a=2?

Mein Vorschlag:

P AND (x = 0)) impliziert I
y > a AND x = 0 impliziert x + y > a

da x 0 ist enthält man ja die Aussage y > a impliziert y > a also eine Tautologie.

Oder lieg ich da jetzt ganz daneben?

[kambo]

Muss man dazu überhaupt Zahlen einsetzen, bzw. wie kommst du auf a=2? __________________________________________________ _________
Bei Korrektheitsassagen der Gestalt
PRE { while B do begin v <-- v + a; w <-- w - b end } POST über den natürlichen Zahlen eignet sich oft a*w + b*v = c als Invariante, bla bla bla
__________________________________________________ _____________

dh.
v <--v + a ; w <-- w - b entspricht:
x <--x + 2 ; y <-- y - 1 (siehe Angabe)
=> a = 2


Mein Vorschlag:

P AND (x = 0)) impliziert I
y > a AND x = 0 impliziert x + y > a

da x 0 ist enthält man ja die Aussage y > a impliziert y > a also eine Tautologie.

Oder lieg ich da jetzt ganz daneben? klingt logisch....

ich habe meine Lösung verbessert........bitte um Kommentare

[NeoCortex]

__________________________________________________ _________
Bei Korrektheitsassagen der Gestalt
PRE { while B do begin v <-- v + a; w <-- w - b end } POST über den natürlichen Zahlen eignet sich oft a*w + b*v = c als Invariante, bla bla bla
__________________________________________________ _____________

dh.
v <--v + a ; w <-- w - b entspricht:
x <--x + 2 ; y <-- y - 1 (siehe Angabe)
=> a = 2



Ich denke, deine Rechnung stimmt, wenn du in die Invariantenformel einsetzt. Die Frage ist halt nur, ob man das überhaupt muss, Zahlen zu finden, denn die Invariante habe ich ja schon gegeben. Diese While-Schleifen-Gleichung ist ja eigentlich dazu da, eine Invariante festzulegen.

Auf die anderen beiden Gültigkeitsaussagen komme ich nämlich auch ohne Zahlen:

(2)
(I AND B) impliziert I [y - 1 | y] [x + 2 | x]
x + y > a AND y != 0 impliziert (x + 2) + (y - 1) > a
x + y > a AND y != 0 impliziert x + y + 1 > a GÜLTIG, da durch + 1 nicht kleiner wird

(3)
x + y > a AND !B impliziert x > a
x + y > a AND !(y != 0) impliziert x > a
x + y > a AND y = 0 impliziert x > a
x + 0 > a impliziert x > a Was wieder eine Tautologie wäre.

Weiß halt nicht, ob das so genügt.

[ein_stein2000]

hm .. als beweis hab ich die zahlen eingesetzt, sonst hab ichs gleich ..

[ChristofNeutron]

Weiß halt nicht, ob das so genügt.

Ich denk schon, dass das reicht. Ich bin unabhängig davon auf das gleiche gekommen :)



__________________________________________________ _________
Bei Korrektheitsassagen der Gestalt
PRE { while B do begin v <-- v + a; w <-- w - b end } POST über den natürlichen Zahlen eignet sich oft a*w + b*v = c als Invariante, bla bla bla
__________________________________________________ _____________

dh.
v <--v + a ; w <-- w - b entspricht:
x <--x + 2 ; y <-- y - 1 (siehe Angabe)
=> a = 2


Ich bin mir ziemlich sicher, dass das a aus der Angabe, nicht das a von diesem zitierten Bsp ist.
Generell ist es besser, wenn möglich, allgemein zu beweisen, d.h.Variablen als solche stehen lassen.

[owaye]

................... :distur: