10.1

[_logonoff_]

zum vergessen...

[Erdös-Index 97]

zu a)
Meiner Meinung nach ist die Schlussbedingung x<0 in N immer falsch - kleiner als 0 gibts ja garnicht.
Damit das ganz trotzdem gültig wird, muss entweder die Precondition falsch sein oder das Programm nicht terminieren.
Das Prog terminiert imho in zwei Bedingungen, eintweder x=0 oder x>0 und y=0, sonst bleibts in einer endlosschleife hängen. Also muss bei diesen beiden Fällen die Precondition falsch sein, mein Vorschlag ist also:
F: !(x=0) ^ !((x>0) ^ (y=0))

zu b)
x>0 ist nach dem Durchlauf des Programm sicher falsch, x kann nachher nur 0 sein. Also müsste F falsch sein, damit die gesamte Postcondition wahr ist.
mein Vorschlag für F: y!=2 aus folgendem Grund:
Ist die Precondition wahr, ist F falsch und somit de Postcondition wahr -> die gesamte Formel ist wahr
Ist die Precondition falsch, ist F wahr und somit die Postcondition falsch -> somit ist die Formel auch wahr, also ist sie gültig.

stimmt das so http://hades.gothic.at/iforum/images/smilies/confused.gif

[_logonoff_]

zu a)
Meiner Meinung nach ist die Schlussbedingung x<0 in N immer falsch - kleiner als 0 gibts ja garnicht.


ich hab natürlich drauf vergessen, dass x nicht kleiner 0 werden darf...


Damit das ganz trotzdem gültig wird, muss entweder die Precondition falsch sein oder das Programm nicht terminieren.


das vestehe ich nicht - muss nicht, damit die korrektheitsaussage gültig ist, alles wahr sein? M*(P alpha Q) liefert ja nur true, wenn P true ist. und eine formel heißt doch nur gültig, wenn sie unter allen variablenbelegungen gültig ist... :confused:

genauso versteh ich dann auch folgendes nicht wirklich.


Ist die Precondition falsch, ist F wahr und somit die Postcondition falsch -> somit ist die Formel auch wahr, also ist sie gültig.

abgesehen davon kann ich dir nur zustimmen.

[Erdös-Index 97]

Siehe Skriptum Seite 103, 4.11:
Wenn M(I,P) wahr ist und alpha definiert ist (d.h. terminiert), dann gilt M(M(I,alpha),Q) = wahr.
Heisst auf deutsch: damit eine korrektheitsaussage wahr ist, muss entweder Q nach durchlauf von alpha wahr sein oder "P ist wahr und alpha terminiert" muss falsch sein - das ist analog zu "A->B ist dasselbe wie !A v B".
Deswegen muss, wenn die Postcondition auf jeden fall falsch ist (wie in a) ) entweder P falsch sein oder alpha nicht terminieren damit die Korrektheitsaussage wahr ist.
isses jetzt ein bisschen klarer?

[_logonoff_]

Siehe Skriptum Seite 103, 4.11:
Wenn M(I,P) wahr ist und alpha definiert ist (d.h. terminiert), dann gilt M(M(I,alpha),Q) = wahr.
Heisst auf deutsch: damit eine korrektheitsaussage wahr ist, muss entweder Q nach durchlauf von alpha wahr sein

bis daher sonnenklar.


oder "P ist wahr und alpha terminiert" muss falsch sein - das ist analog zu "A->B ist dasselbe wie !A v B".


hui, jetzt hab ich länger überlegt, aber verstanden (hoffe ich), danke!
ich hätte das aus dem text im skriptum sonst nicht so "logisch" entnommen.
vielleicht als gedankliche stütze, damit andere nicht so lange überlegen müssen, die bedingung für die gültigkeit aus dem skriptum nochmals in PL (korrigiert mich wenn ich irre):

M*(P {alpha} Q) = (M_PL(I, P) ^ PL(M_AL(I, alpha) definiert)) impliziert Q

[ein_stein2000]

bis daher sonnenklar.



hui, jetzt hab ich länger überlegt, aber verstanden (hoffe ich), danke!
ich hätte das aus dem text im skriptum sonst nicht so "logisch" entnommen.
vielleicht als gedankliche stütze, damit andere nicht so lange überlegen müssen, die bedingung für die gültigkeit aus dem skriptum nochmals in PL (korrigiert mich wenn ich irre):

M*(P {alpha} Q) = (M_PL(I, P) ^ PL(M_AL(I, alpha) definiert)) impliziert Q
jo so ist es OK finde ich

[Pinhead]

Dürfte so stimmen hab des gleiche.

[maitscha]

...sonst bleibts in einer endlosschleife hängen. Also muss bei diesen beiden Fällen die Precondition falsch sein...


Wenn das Programm in einer Endlosschleife hängen bleiben würde, wäre dann das nicht korrekt und die Precondition muss für so einen Fall daher falsch sein?

Verhalten sich Precondition und Postcondition wie eine Implikation?

Könnte man nicht auch für Lösung a) !(x=0) Implikation (y=0) nehmen?

Warum ist die Aussage wahr, wenn Precondition und Postcondition falsch sind?

[Erdös-Index 97]

Verhalten sich Precondition und Postcondition wie eine Implikation?
in etwa, nur mit dem wichtigen zusatz ob das programm terminiert oder nicht.
also nicht Precondition -> Postcondition sondern (Precondition ^ Programm terminiert) -> Postcondition

[ein_stein2000]

in etwa, nur mit dem wichtigen zusatz ob das programm terminiert oder nicht.
also nicht Precondition -> Postcondition sondern (Precondition ^ Programm terminiert) -> Postcondition
i glaub das hab i no imma net genau kapiert ... wie kommst du da genau drauf?

M*(P {alpha} Q) = t wenn für alle I Î ENV gilt: MPL(I,P) = t (Precondition) und MAL(I,alpha) definiert (Programm terminiert), dann (impliziert) gilt MPL(MAL(I,alpha),Q) = t (Postcondition)

hab i die definiton wie sie im skriptum steht jetzt richtig gedeutet?

[Erdös-Index 97]

soweit ich sehe is richtig.
Ich denke mir dann statt A->B immer !AvB, das is irgenwie durchschaubarer für mich ;).
Also entweder "MPL(I,P) = t (Precondition) und MAL(I,alpha) definiert (Programm terminiert)" ist falsch ODER MPL(MAL(I,alpha),Q) ist wahr, dann stimmt die Korrektheitsaussage.

[Studigel]

Seh ich das richtig muss ich einfach nur irgendwas für F nehmen das nicht stimmt.

Also das Prinzip is ja einleuchtend, aber der Sinn dahinter bleibt mir verborgen.

[Primenumber]

Ich bin unschlüssig ob man F nicht einfacher gestalten kann.

alpha übersichtlicher aufgeschrieben:


begin
..while x > 0 do
....x <- y;
..begin
....x <- y;
....y <- x
..end
end


Sehen wir uns die Speicherbelegungen an: uns interessieren uns pro Variable 2 Zustände, 0 oder nicht 0 (in meinen Beispielen 1), das ergibt 4 Möglichkeiten:

I(x) = 0, I(y) = 0 ... terminiert
I(x) = 1, I(y) = 0 ... terminiert
I(x) = 0, I(y) = 1 ... terminiert
I(x) = 1, I(y) = 1 ... terminiert nicht

Reicht es also wenn man sagt F: !(x=0) ^ !(y=0) ?

[ChristofNeutron]

Reicht es also wenn man sagt F: !(x=0) ^ !(y=0) ?

Passt :) das ist ja die geschrumpfte Form von F: !(x=0) ^ !((x>0) ^ (y=0))

Noch ein Tipp, schauts euch einfach das Bsp 4.13 auf der nächsten Seite an, da wird passend für dieses Bsp argumentiert ;)

[konsch]

Es reicht doch auch, wenn meine Precondition falsch für alle Speicherbelegungen I € ENV ist.
Dann wäre mein F z.B. wie die Postcondition x<0.

Dann wäre es ja auch egal, ob mein Programm terminiert oder nicht.

Was denkt ihr?

EDIT:
Okay, okay. Habs grad verstanden. In der Angabe werden ja explizit in N erfüllbare Formeln verlangt.

[ein_stein2000]

Ich erlaube mir mal, meine Lösung hier zu posten ...

danke nochmal an fl_QuelTos, der mir im IRC-channel (der fast nie besucht wird :( ) geholfen hat