Im Script auf Seite 48 bzw. im Reynold auf Seite 56 werden zwei Funktionen p_f und p_t mit:

p_t true = top p_t false = bottom
p_f false = top p_f true = bottom

definiert.

Kann mir gerade nicht erklären, was dann:
(p_f [q]_assert)
bedeutet.

du meinst p_t o [q]_assert ? ganz einfach: [q]_assert liefert true oder false, welche auf p_t anwendbar sind (denn p_t: {true,false}->{bottom,top}…diese beiden Gleichungen zur Semantik von spec sind einfach eine andere Formalisierung, wie im Skript auch erwähnt, sie ist einfach in bestimmten Zusammenhängen nüztlicher als die andere

Hmm… ok, was die Funktionen aussgen ist mir klar, allerdings kann ich die verkürzten Formen von DR SEM EQ: Partial… und DR SEM EQ:Total… unter "Eine andere Formalisierung" auf Seite 48 leider immer noch nicht richtig lesen… Kann mir das jemand ausformulieren?

ok,ich versuch es mal:
(1) partielle Korrektheit

angenommen c terminiert nicht dann müsste ja insgesamt true herauskommen(wegen partieller Kor…):
der linke teil ergibt bottom (wegen der erweiterung ()_doppelbottom)und dann ist die "ungleichung" ja erfüllt (denn bottom <= irgendwas gilt ja immer) das ist schon einmal geschafft . ]
falls c terminiert muss der Zustand auf dem c gearbeitet hat [q]_assert wahr machen FALLS der ausgangszustand [p]_assert wahr macht:
also wenn der Ausgangszustand [p]_assert nicht wahr macht ergibt der rechte teil immer Top (schau dir p_t an) und unsere ungleichung ist dann immer erfüllt. goil!!
nun der letzte Fall:
falls der Ausgangszustand [p]_assert wahr macht ergibt rechte teil bottom, nun muss der linke Teil auch bottom ergeben, und siehe da, dass macht er nur wenn der Zustand, den wir nach der Anwendung von c erhalten, [q]_assert wahr macht, wegen p_f(true)=bottom

ich hoffe das hilt und du kannst die totale Korrektheit selbst erklären

Ich versuch es mal mit der totalen Korrektheit:

1) c terminiert nicht.
Insgesammt muß dann false herauskommen. Wenn c nicht terminiert, ist die rechte Seite false. D.h. die linke Seite muß true sein, da sonst die Gesamtgleichung true und nicht false wäre. Dies ist der Fall, wenn [p]_assert true ist.

Was ist jetzt in dem Fall, dass [p]_assert false ist? (So wie ich das sehe ergibt sich dann true für die Gesamtgleichung.) Muß dieser Fall überhaupt betrachtet werden? Eigentlich ist dann die Korrektheit gar nicht mehr definiert, oder?

2) c terminiert.
Es kommt nur true heraus, wenn [q]_assert auch zu true ausgewertet wird, was der Definition von totaler Korrektheit entspricht.

Aber wieder: Was ist mit dem Fall [p]_assert = false? [p]_assert ist für den Fall das c terminiert für das Ergebniss der Gesamtgleichung eigentlich egal, oder?

Was ist jetzt in dem Fall, dass [p]_assert false ist? (So wie ich das sehe ergibt sich dann true für die Gesamtgleichung.) Muß dieser Fall überhaupt betrachtet werden? Eigentlich ist dann die Korrektheit gar nicht mehr definiert, oder?

du hast recht, dann kommt true heraus, ist aber in der ersten Definition auch so angegeben (da steht ein "==>"), also falls die Vorbedingung nicht erfüllt ist, braucht uns der Rest nicht zu interessieren, wir wollen ja nur, dass unsere Programm korrekt arbeitet, falls es unter den richtigen Vorraussetzungen benutzt wird

Aber wieder: Was ist mit dem Fall [p]_assert = false? [p]_assert ist für den Fall das c terminiert für das Ergebniss der Gesamtgleichung eigentlich egal, oder?

hier wieder fast das gleiche: falls [p]_assert false dann gilt das, was ich oben geschrieben habe, wenn true muss c terminieren und die Nachbedingung true ergeben, und genau das macht ja der rechte Teil der Gleichung

Super, danke für die Erklärung!

Hab das doch noch nicht ganz verstanden:

(p_f o {i}_assert)_doppelbottom o {c}_comm =< p_f o {i and b}_assert

Ist mir immer noch unklar. Auch die "o" versthe ich nicht.

P.S. Eckige Klammern läßt das Forum bei mir gerade nicht zu, darum diee geschweiften.

Ich versuch mich doch mal an einer Erklärung:

(p_f o {i}_assert) ist, wenn ich das "o" jetzt richtig deute eine Hintereinaderausführung der zwei Funktionen [-]_assert und p_f. D.h. das ganze ist gleichbedeutend mit p_f({i}_assert) (ok, sieht etwas kryptisch aus…). Soweit klar (wenn richtig). Aber die Commands sind mir noch nicht klar.

(p_f o {i}_assert)_doppelbottom o {c}_comm

{c}_comm wird ja entweder zu einem <top> (terminiert ?) oder einem <bottom> (terminiert nicht) ausgewertet.

1) {c}_comm = <bottom>
Dann wird dann durch f_doppenbottom der ganze Formelteil zu bottom.

2) {c}_comm = <top>
Dann wird mit der Ausführung von (p_f o {i}_assert) fortgefahren. {i}_assert ergibt einen Wert aus {true, false}, welcher dann von p_f auf {<top>,<bottom>} abgebildet wird.


Für die Formel

(p_f o {i}_assert)_doppelbottom o {c}_comm =< p_f o {i and b}_assert

würde das heißen:
1) {c_comm} terminiert nicht
-> die like Seite wird <bottom>, damit ist die Gesamtgleichung erfüllt.

2) {c_comm} terminiert
-> (p_f o {i}_assert) wird ausgewertet
-> wenn {i}_assert == true, dann p_f == <bottom>
d.h. die Gesamtgleichung müßte dann immer true ergeben. Das
würde, wie in einem der vorigen Beiträge, der Bedeutung von
partieller Korrektheit entsprechen.
-> wenn {i}_assert == false, dann p_f == <top>
d.h. um die Gesamtformel true werden zu lassen muss auch der
rechte Teil true werden.
->Der rechte Teil wird nur true, wenn die Auswertung von
{i and b}_assert zu false ausgewertet wird. Was insofern Sinn
ergibt, da die Invariante dann auf beiden Seite der
false ergibt.

Aber richtig einleuchtend ist das noch nicht.

Aber die Commands sind mir noch nicht klar.

(p_f o {i}_assert)_doppelbottom o {c}_comm

{c}_comm wird ja entweder zu einem <top> (terminiert ?) oder einem <bottom> (terminiert nicht) ausgewertet.

Aehmm, wenn ich es richtig sehe, dann ist {c}_comm doch eine Funktion, die ein Sigma zurueckgibt…

Für die Formel

(p_f o {i}_assert)_doppelbottom o {c}_comm =< p_f o {i and b}_assert

Wo steht diese Formel? Im Skript?

D.h. das ganze ist gleichbedeutend mit p_f({i}_assert) (ok, sieht etwas kryptisch aus…). Soweit klar (wenn richtig).

stimmt

{c}_comm wird ja entweder zu einem <top> (terminiert ?) oder einem <bottom> (terminiert nicht) ausgewertet.

{c}_comm kann man für sich schon mal gar nicht auswerten,
{c}_comm ist nichts anderes als eine Funktion SIGMA nach SIGMA_bottom

{c}_comm auf einen Zustand angewendet liefert also einen Folgezustand oder bottom (Nichttermination)

darauf wirkt dann die nächste Funktion {q}_assert,
die von SIGMA auf {true,false} abbildet,
(mit der Trickkiste doppelbottom: bottom wird auf bottom abgebildet)

und dann kommt die Funktion pf,
die von {true,false} auf {top, bottom} abbildet,

1) {c}_comm = <bottom>
Dann wird dann durch f_doppenbottom der ganze Formelteil zu bottom.

{c}_comm ist eine Funktion, bottom ein Zustand, das geht nicht,

es kann aber der Fall {c}_comm (sigma)= <bottom> auftreten, dass meinst du sicher,

2) {c}_comm = <top>
Dann wird mit der Ausführung von (p_f o {i}_assert) fortgefahren. {i}_assert ergibt einen Wert aus {true, false}, welcher dann von p_f auf {<top>,<bottom>} abgebildet wird.

{c}_comm (sigma)= sigma2 != <bottom>

dann wird die Nachbedingung geprüft (wieso schreibst du i und nicht q?) und es kommt am Ende top oder bottom raus

Für die Formel

(p_f o {i}_assert)_doppelbottom o {c}_comm =< p_f o {i and b}_assert

würde das heißen:
1) {c_comm} terminiert nicht
-> die like Seite wird <bottom>, damit ist die Gesamtgleichung erfüllt.

bis auf die Sprechweise '{c}_comm(sigma) terminiert nicht' richtig

2) {c_comm} terminiert
-> (p_f o {i}_assert) wird ausgewertet
-> wenn {i}_assert == true, dann p_f == <bottom>
d.h. die Gesamtgleichung müßte dann immer true ergeben. Das
würde, wie in einem der vorigen Beiträge, der Bedeutung von
partieller Korrektheit entsprechen.

wenn der linke Teil der Formel bottom ist dann ist alles ok, ja

-> wenn {i}_assert == false, dann p_f == <top>
d.h. um die Gesamtformel true werden zu lassen muss auch der
rechte Teil true werden.
->Der rechte Teil wird nur true, wenn die Auswertung von
{i and b}_assert zu false ausgewertet wird. Was insofern Sinn
ergibt, da die Invariante dann auf beiden Seite der
false ergibt.

Aber richtig einleuchtend ist das noch nicht.

das entspricht genau der Ursprungsdefintion 2.1,
entweder terminiert c nicht ODER die Nachbedingung ist erfüllt ODER die Vorbedingung ist falsch,
dass sind die 3 Fälle in denen partielle Korrektheit gilt,

die Formel drückt genau das aus, nur eben umständlich dafür sehr kurz formuliert

Für die Formel

(p_f o {i}_assert)_doppelbottom o {c}_comm =< p_f o {i and b}_assert

Wo steht diese Formel? Im Skript?

~Seite 48, nach der normalen Definition der partiellen und totalen Korrektheit

Danke!

Ich werd mir wohl nochmal die Bedeutung von {c}_comm genau anschauen müssen… Ich dachte ich hätte es verstanden.

i statt q, weil ich an der Formel zur while-Anweisung auf Seite 51 herumgedacht habe (unten beim Beweis).

darauf wirkt dann die nächste Funktion {q}_assert,

Ok. D.h. die drei Funktionen p_f, {i}_assert und {c}_comm werden von rechts nach links hintereinader ausgeführt (-> "o"), und die Klammerung mit doppelbottom macht nur deutlich welcher Teil evtl. gar nicht mehr ausgewertet wird, wenn {c}_comm (sigma)= <bottom>

Nur nochmal zum Verständniss:

{c}_comm (sigma)= <bottom>

{-}_comm wird auf c angewendet, und ordnet c eine Funktion zu, die einen Zustand sigma auf einen Zustand sigma' abbildet. In diesem Fall ist also sigma der Zustand vor der "Ausführung" von c (also praktisch das sigma' des Befehls vor c oder soetwas wie ein Startzustand), und sigma' ist <bottom>.

ja, hört sich alles richtig an