[ Frage ] Hoare Kalk. Wann T1 und wann T2 ?

[Jimmy]

war etwas verwirrt wegen der Musterloesung vom 24-10-2k2

http://www.logic.at/lvas/thinf1/angaben/ti1v025/4.jpg

und zwar verwendet der Prof. auf dem Weg zur Formel (1) die Regeln T3 dann T2 - Wieso aber T2 ???
Kann/Soll man da nicht T1 anwenden ? Weil laut Skriptum kommt im Ausdruck

x=15 { y <- 5x } INV......

ja das y WEDER in P (= x=15) oder in t (=5x) vor.....

ist das ein Special Fall??? oder im Endeffekt egal???

:confused:

[bubum]

...oder im Endeffekt egal???

Ist Egal. IMHO ist es sogar einfacher wenn du immer T2 statt T1 anwendest.....

mfg

[Filz]

Nachdem du T2 immer anwenden kannst, und bei T1 Fehler passieren können (und du außerdem noch Beim Überprüfen min 10Sek. Zeit verlierst) solltest du T2 nehmen.

[GetStoopid]

also egal ist es denk ich mal nicht... aber in dem fall entspricht es einfach ganz klar der regel t2?! du willst ja zuerst das begin .. end wegbekommen, und somit stoesst du auf die zuweisung (und nicht "irgendeinem beta"was dann ganz klar der regel t2 entspricht... du kannst t2 immer dann verwenden wenn beta und alpha zuweisungen sind... zumindest mach ich es immer so, und das stimmte bisher auch immer...

[Jimmy]

jep, war heute beim Prof. in der Sprechstunde..er meint auch , dass es mit T1 geht (hats dann nachgerechnet) es kommt fuer die Invariante das gleiche c raus.. und somit kann man beide Methode anwenden..

werd eh T2 verwenden, geht irgendwie fluessiger *g*
Danke aber an alle..