probleme mit hilfsregeln bei hoare-k.

[andy]

beispiel (24.10.02)

x=15 {begin y <-- 5x; z <-- x+y end} INV

wieso wird hier t2 angewandt und nicht t1?

[Jumper]

Du kannst auch T1 nehmen (weil Hoare ist wie Sequentialkalkül vollständig und korrekt), da wird das ganze aber nur komplizierter und umständlicher, deswegen nimmst T2, weil du so "nur" deine Prämisse Q näher erklärst (also im Beweis der Invariante z.B. x durch x+3 ersetzt) und dann dir eine einfache Form übrig bleibt. Also bei begin w<--w+x; v<--v+y end kommt man so am Einfachsten und am Schnellsten zum Ziel.

[andy]

also wenn man t1 oder t2 nehmen kann, dann t2 nehmen
weils mit t1 zu komplizierter wird

stimmt das so?

[Jumper]

Nein, das wäre falsch, aber wenn du eben diesen Fall hast, dass dein Alpha dies Form hat (w<--w+x) und dein Beta diese Form hat (v<--v+y) dann gehe so vor, dann hast du weniger Aufwand bei den Ableitungen.

[Kampi]

@jumper: ich glaube nicht, dass das falsch ist. man könnte auch t1 nehmen, aber der prof salzer hat in den übungspdf immer t2 genommen, und ich glaube, dass das wegen der einfachheit ist.
ich sehe das so wie andy.
mfg. kampi

[Jumper]

Das habe ich damit gemeint, dass es serwohl geht nur mehr Aufwand bedeutet.

[Kampi]

ja, hast recht, ich habs überlesen. ich glaub ich leg mich vor der prüfung lieber noch mal aufs ohr :-)