Disclaimer: Dieser Thread wurde aus dem alten Forum importiert. Daher werden eventuell nicht alle Formatierungen richtig angezeigt. Der ursprüngliche Thread beginnt im zweiten Post dieses Threads.
19.02.09 Altklausur WP-Kalkül
Hey, ich hab ne frage noch zu nem WP aus einer Altklausur (Aufgabe ist als Anhang)
iii) Weisen Sie nach, dass die von Ihnen gewählte Invariante nach jedem Durchlaufen
des Schleifenrumpfs gilt. Geben Sie zunächst explizit an, was zu zeigen ist.
Hinweis: Das Axiom “a mod 2 = (a - 2) mod 2” darf dabei für a >= 2 verwendet
werden.
Zu zeigen: [Ivb]->wp[A,Q]
Nachweis:
wp(“x-2;y=y+1”, (x mod 2= (i mod 2) ^ y>=0
…
=> ((x-2)mod 2)=(i mod 2) ^ y+1>=0
=> ((x-2)mod 2)=((i-2) mod 2) ^ y+1>=0 //wegen dem in der angabe
Aber wie mach ich jetzt weiter?
muss ich da jetzt noch die Schleifenbedingung x>1 dazu nehmen?
Attachment:
wp.PNG: https://fsi.cs.fau.de/unb-attachments/post_104571/wp.PNG
Ich hab:
zu zeigen:
{I ^ B} A {I}
Nachweis:
wp(“x = x-2; y = y+1”, x mod 2= (i mod 2) ^ y>=0 )
wp(“x = x-2;”, x mod 2= (i mod 2) ^ y+1>=0 )
wp(" ", (x-2) mod 2= (i mod 2) ^ y+1>=0 )
(x-2) mod 2= (i mod 2) ^ y >= -1
jetz würde ich begründen:
x==i dadurch wird die Modulo Op das gleiche ergebnis bringen (axiom anwenden von oben)
und y = 0
=> i mod 2= i mod 2 ^ true
=> i mod 2= i mod 2
=> true
Ich frag hier einfach gleihc mit rein: Was habt ihr denn bei der i) als Schleifeninvariante ausgewählt?
Wenn deine Auffassungsgabe in der Klausur genauso scharfsinnig ist würde ich es erst nächstes Semester versuchen… (pro-Tipp: schau in den Post über dir)
Tja, saß halt mal auf dem Schlauch – ist halt dohc noch früh am Morgen 
.
also ich hab das unterste ausgewählt, falls das oben nicht deutlich wurde.
Stimmt des denn?
Ja klar.
Ich hab einfach deinen Beitrag total überlesen und hab völlig verkehrt gedacht ;).