10.2

[Erdös-Index 97]

Mein Vorschlag:

Meine Lösung ist ziemlich analog zur Erklärung von Technik 3 im alten Skriptum Seite 75.
Wälht man für Q INV, die Invariante der while-schleife, so ergibt sich bei der Ableitung von P{while B do alpha}INV (der aus der Ableitung mit H2 entsteht) unter anderem der Ausdruck (INV ^ !B) -> INV. Da dieser eine Tautologie ist, kann er vernachlässigt werden.
Was übrigbleibt sind die zwei anderen Ausdrücke aus der while - Schleife und INV{beta}R , welches auch durch H2 entsteht.
Somit kann man die Hilfsregel T4 formulieren:

(P -> INV) (INV ^ B){alpha}INV INV{beta}R
_______________________________________
P{begin while B do alpha, beta end}R

Fragen Wünsche Anregungen Beschwerden? :D

[Erendis]

ich verstehe nicht genau, wie du durch die Anwendung von H2 auf diesen Ausdruck kommst:


Wälht man für Q INV, die Invariante der while-schleife, so ergibt sich bei der Ableitung von P{while B do alpha}INV (der aus der Ableitung mit H2 entsteht) unter anderem der Ausdruck (INV ^ !B) -> INV. Da dieser eine Tautologie ist, kann er vernachlässigt werden.
Was übrigbleibt sind die zwei anderen Ausdrücke aus der while - Schleife und INV{beta}R , welches auch durch H2 entsteht.
Somit kann man die Hilfsregel T4 formulieren:

(P -> INV) (INV ^ B){alpha}INV INV{beta}R
_______________________________________
P{begin while B do alpha, beta end}R

[Erdös-Index 97]

Auf Seite 104 neues Skriptum sind die Regeln H2 und H4 beschrieben. Wird eine begin schleife abgeleitet, die eine whileschleife drinnen hat dann sieht das etwa so aus wie im alten Skriptum Seite 75 im Abschnitt "Technik III".
In dem Fall,in dem die whileschleife das alpha von "begin alpha, beta end" ist, bleiben einem nach der Ableitung 4 Terme über:
(P -> INV), (INV ^ B){alpha}INV, ((INV ^ !B)->Q) und Q{beta}R

Nun muss das Q irgendwie gewählt werden. Setzt man es als INV, ist der dritte Ausdruck eine Tautologie und muss deswegen nichtmehr beachtet werden.

[ein_stein2000]

genauso hab ich es auch

[Erendis]

du hast ja zuerst H4 auf die while Schleife angewendet, und dann H2 auf den gesamten Ausdruck, also +der Ableitung mit H4. hab ich dann auch nicht neben dem Q {beta}R auch das P{alpha}Q stehen??

[ein_stein2000]

ich poste mal meine lösung, vielleicht hilft das etwas ...

[Veronika]

der Ausdruck (INV ^ !B) -> INV. Da dieser eine Tautologie ist, kann er vernachlässigt werden.

Sicher eine blöde Frage, aber kannst du mir erklären, wieso (INV ^ !B) -> INV eine Tautologie ist?
danke

[psycho]

informell: damit der ausdruck false wird, muss bei A-> B A true sein und B false. wenn aber INV false ist, ist (INV ^ !B) auch false...

[konsch]

Sicher eine blöde Frage, aber kannst du mir erklären, wieso (INV ^ !B) -> INV eine Tautologie ist?
danke


Weil:
t ^ irgendwas impliziert t .....immer true ist
und
f ^ irgendwas impliziert f ..... auch immer true ist.

Klar?

[fuxi17]

bei mir schaut das Ganze so aus:

(P -> INV) (INV and B){alpha}(INV) (INV and !B){beta}R

Solang nämlich B true ist wird die Schleife ausgeführt. Wenn jetzt B false ist dann wird beta ausgeführt. Daher ist beim Ausführen des Programmes beta die Invariable UND !B true!!!

[Saruman]

Auwehauweh, ich verstehs nicht.

Aber warum erfrischt mich das 4te Ottakringer bloß so?
Bloß so?

[ein_stein2000]

Auwehauweh, ich verstehs nicht.

Aber warum erfrischt mich das 4te Ottakringer bloß so?
Bloß so?
wennst net genau sagst wos du nit verstehst, wird dir keiner helfen können ...

[maqx]

...
Nun muss das Q irgendwie gewählt werden. Setzt man es als INV, ist der dritte Ausdruck eine Tautologie und muss deswegen nichtmehr beachtet werden.

das ist der punkt, den ich nicht versteh...
wieso kann ich tautologien weglassen???

[NeoCortex]

Wieso kann ich für Q INV wählen? Darf ich die frei wählen und sollte sie nur möglichst günstig wählen?

[ChristofNeutron]

das ist der punkt, den ich nicht versteh...
wieso kann ich tautologien weglassen???

Naja, Tautologien ergeben immer t, egal was für Werte eingesetzt werden, sind somit konstant und können weggelassen werden.

[ein_stein2000]

Wieso kann ich für Q INV wählen? Darf ich die frei wählen und sollte sie nur möglichst günstig wählen?
solltest möglichst günstig wählen, um eben eine tautologie zu erzeugen, damit du dir etwas ersparen kannst ...

[NeoCortex]

solltest möglichst günstig wählen, um eben eine tautologie zu erzeugen, damit du dir etwas ersparen kannst ...
Okay, danke...
achso, noch etwas:
der Zusatz zur Angabe "Beweisen Sie die Korrektheit der Hilfsregel durch Rückführung auf Regeln des Hoare-Kalküls" ist schon durch die Anwendung der Hoare-Regeln erfolgt?
Danke schön!

[ein_stein2000]

Okay, danke...
achso, noch etwas:
der Zusatz zur Angabe "Beweisen Sie die Korrektheit der Hilfsregel durch Rückführung auf Regeln des Hoare-Kalküls" ist schon durch die Anwendung der Hoare-Regeln erfolgt?
Danke schön!
jo ist es afaik ...

[NeoCortex]

jo ist es afaik ...Fein, dann kann ich ja beruhigt schlafen gehen ;)