Das is einfach laut Wahrheitstabelle true, fertig aus, nix mehr begründungswürdig. Das is auch normalerweise das Ziel bei der WP-Invariante wo man hin will
also ich versuch mein problem mal etwas zu spezifizieren:
ich habe ja normal und auch in meinen Übungsunterlagen immer Aufgaben mit if bei denen Q: nicht noch so ein kleiner oder größer zeichen dabei hat und bei denen dafür die If bedingung solch ein kleiner oder größer zeichen hat.
Wenn ich jetzt das wie oben gepostet nehme:
wp(collatz, Q) = [n >= 0 ^ 0.5n = 0.25((4n + 1) - (2n + 1) (-1)^n) ^ (n % 2 == 0)]
v [n >= 0 ^ 0.5(3n + 1) = 0.25((4n + 1) - (2n + 1) (-1)^n) ^ (n % 2 == 1)]
und betrachte jetzt die fälle einzeln, kann ich ja schlecht das n in (n % 2 == 0)] durch das n davor ersetzen.
Hätte ich jetzt in der Aufgabe gar kein (n % 2 == 0)] stehen, dann könnte ich das ja viel besser ersetzen… so krieg ich irgendwie nur Müll raus…
hier mal meine rechnung:
[n >= 0 ^ 0.5n = 0.25((4n + 1) - (2n + 1) (-1)^n) ^ (n % 2 == 0)]
v [n >= 0 ^ 0.5(3n + 1) = 0.25((4n + 1) - (2n + 1) (-1)^n) ^ (n % 2 == 1)]
Fall 1:
wp(“n=(2n+0,5)-(n+0,5)*(0,25)^n;”, n%2==0)
wp(n=2n+0,5-(0,25n+0,125)^n;",n%2==0)
(2n+0,5-(0,25n+0,125)^n)%2==0
Stimmt das bis dahin?
ich würde den 2. Fall jetz genauso machen. Aber das sieht ja irgendwie unschön aus das ganze.
Oder würde mir vielleicht jemand von euch seine richtige Lösung zur Verfügung stellen?
Wäre sehr nett!
ich kann da leider nicht weiterhelfen, versteh das ganze selbst noch nicht so gut.
aber mal an euch… ich hab grad die b) aus dem Übungsblatz vom letzten mal zum wp Kalkül gerechnet. Kennt vielleicht jemand die Lösung? Weil ich komme auf sowas wie 3c=-5a.
Der Ich, hast du vielleicht noch die Lösungen vom letzten Jahr?
Wie bist du da drauf gekommen? Eigentlich musst nur noch den Term von oben vereinfachen, die eigentliche Geschichte im dem Einsetzen ist doch schon passiert. Ganz am Anfang stand was von wegen
wp(A, Q) = wp(sehr_viel_code, Q)Dann haben wir den Code eingesetzt in die Vorbedingung Q und raus kam
[n >= 0 ^ 0.5n = 0.25((4n + 1) - (2n + 1) (-1)^n) ^ (n % 2 == 0)]
v [n >= 0 ^ 0.5(3n + 1) = 0.25((4n + 1) - (2n + 1) (-1)^n) ^ (n % 2 == 1)]als weakest precondition. In dem Punkt kannst du das ‚wp‘ schon weglassen weil es ja schon eine Bedingung ist (auch wenn stark aufgebläht). Im Prinzip bist du hier auch schon fertig, du sollest es halt noch vereinfachen.
Eine Möglichkeit ist es zB die Teilbedingung n >= 0 rauszuziehen, oder die Geschichte mit dem (-1)^n zu vereinfachen (schau dir hierbei mal den Term mit dem Modulo an).
Es fällt eine ganze Menge weg, sodass am Ende nur noch n>=0 (falls nicht, bitte korrigieren) dastehen sollte.
Hey, danke für deine Antwort. Ich will es doch verstehn, aber irgendwie klappt es grad nicht.
Ich hab ja in der Aufgabe stehen:
if(n%2==0){
return n/2;
}else {
return (3n+1)/2;
}So.
laut der Folie 11-90 bilde ich ja quasi sowas:
(n%2==0^ wp(n/2, 0.25((4n + 1) - (2n + 1) *(-1)^n)) v n%2==1^wp((3n+1)/2), 0.25((4n + 1) - (2n + 1) *(-1)^n))aber wie mache ich denn jetzt weiter? ich muss ja auf jedenfall die fälle unterscheiden.
Du machst doch grad die Fallunterschiedung (also if, else), das einzige was jetzt noch kommt ist einsetzten und das Ding richtig hinschreiben.
[b ^ wp(S1, Q)] v [not_b ^ wp(S2, Q)]
= [(n%2==0) ^ wp(S1, Q)] v [(n%2==1) ^ wp(S2, Q)]
= [(n%2==0) ^ wp("return 0.5n;", Q)] v [(n%2==1) ^ wp("return 0.5(3n + 1);", Q)]
= [(n%2==0) ^ wp("c(n) = 0.5n;", Q)] v [(n%2==1) ^ wp("c(n) = 0.5(3n + 1);", Q)]
= [(n%2==0) ^ wp("c(n) = 0.5n;", (n >= 0) ^ (c(n) = 0.25((4n + 1) - (2n + 1) *(-1)^n)))] v [(n%2==1) ^ wp("c(n) = 0.5(3n + 1);", (n >= 0) ^ (c(n) = 0.25((4n + 1) - (2n + 1) *(-1)^n))))]
= [(n%2==0) ^ (n >= 0) ^ (0.5n = 0.25((4n + 1) - (2n + 1) *(-1)^n))] v [(n%2==1) ^ (n >= 0) ^ (0.5(3n + 1) = 0.25((4n + 1) - (2n + 1) *(-1)^n)))]Ab hier steht jetzt nichts mehr mit wp. D.h. dieser Klotz ist deine Vorbedingung, aber jetzt wird vereinfacht.
Irgendwie hab ich den Verdacht ich verwirr dich nur … :-/
[n >= 0 ^ 0.5n = 0.25((4n + 1) - (2n + 1) (-1)^n) ^ (n % 2 == 0)]
v [n >= 0 ^ 0.5(3n + 1) = 0.25((4n + 1) - (2n + 1) (-1)^n) ^ (n % 2 == 1)]Um es übersichtlicher zu machen mal die einzelnen Zeilen:
Zeile 1:
[n >= 0 ^ 0.5n = 0.25((4n + 1) - (2n + 1) (-1)^n) ^ (n % 2 == 0)]Da für diese Zeile gilt, dass n%2 = 0 folgt, dass n gerade ist → (-1)^n = 1
[n >= 0 ^ 0.5n = 0.25((4n + 1) - (2n + 1) * 1) ^ (n % 2 == 0)]Innere Klammer auflösen
[n >= 0 ^ 0.5n = 0.25(4n + 1 - 2n - 1) ^ (n % 2 == 0)]Ausrechnen
[n >= 0 ^ 0.5n = 0.25(2n) ^ (n % 2 == 0)] [n >= 0 ^ 0.5n = 0.5n ^ (n % 2 == 0)] --> 0.5n = 0.5n ist true [n >= 0 ^ (n % 2 == 0)]Und genauso für die 2te zeile, für die dann rauskommt
[n >= 0 ^ (n % 2 != 0)]Verodert ergibt das ganze dann
n>=0
Nein du verwirrst mich nich, ich bin von natur aus verwirrt. Sorry.
(n%2==0^ wp(n/2, 0.25((4n + 1) - (2n + 1) *(-1)^n)) v n%2==1^wp((3n+1)/2), 0.25((4n + 1) - (2n + 1) *(-1)^n))
das rote soll das sein was ich da geschrieben hab. Was ich aber nich verstehe ist wieso du da ein return bei dir dann reinschreibst.
[(n%2==0) ^ wp(S1, Q)] v [(n%2==1) ^ wp(S2, Q)]Die Zeile ist ja praktisch von den Folien kopiert. S1 steht für den Code (alles) was direkt nach dem if kommt, S2 für alles was nach dem else kommt (bis zur nächsten Klammer, ist klar).
Bei deiner Zeile sind ein paar Sachen vermixt, zum einen steht für S1 nur “n/2”, was eingentlich keine Zuweisung ist, und bei Q (der gegebenen Vorbedingung) fehlt auch ein Teil.
Das return, was an Stelle von S1 tritt, kannst du dann umschreiben in dem du sagst, das Ergebnis der Methode, also c(n) (so heißt ja die Methode), ist gleich n/2. Selbes Spiel giilt für S2.
aber warum muss das denn so lauten wie du das da oben hingeschrieben hast, wenn ich es so mache wie es auf der Folie 90 steht dann krieg ich immer
(n%2==0^ wp(n/2, 0.25((4n + 1) - (2n + 1) *(-1)^n)) v n%2==1^wp((3n+1)/2), 0.25((4n + 1) - (2n + 1) *(-1)^n))
[b ^ wp(S1, Q)] v [not_b ^ wp(S2, Q)]
okay jetz blick ich echt nich mehr durch.
dann hab ich das total falsch verstanden.
…fast, wenn du jetzt noch für Q das richtige Q einsetzt nur nicht nur einen Teil (alles was auf der Angabe steht muss rein!!) und für S1 und S2 was gleiche machts (auch hier alles!! nicht nur Teile des Codes) dann stimmts bei dir…
ehrlich gesagt wird mir nicht ganz klar was da nun fehlt ?
so?
n%2==0^ wp(n/2=0.25((4n + 1) - (2n + 1) *(-1)^n)) v n%2==1^wp((3n+1)/2)=0.25((4n + 1) - (2n + 1) *(-1)^n))
Rein soll
S1 = “return n/2;”
S2 = “return (3n+1)/2;”
Q = b[/b] ^ (c(n) = 0.25((4n + 1) - (2n + 1) *(-1)^n))
Du hast
S1 = n/2
S2 = (3n+1)/2
Q = 0.25((4n + 1) - (2n + 1) *(-1)^n)
…
Edit: warum ist da so wichtig?
Zu Q: naja, Teile der Vorbedingung wegschmeißen ohne Grund, keine gute Idee
Zu S1/2: was genau heißt return n/2 eigentlich? Das bedeutet, dass die Methode c(n) dir als Ergebnis wirklich n/2 übergibt (n wird ja vorher nicht irgendwie manipuliert). Also kann man
“return n/2;” (hier Java-Code)
auch als
c(n) = n/2 (mathematische Gleichung)
betrachten. In der Form kannst du es beim Auflösen vom wp auch direkt in dein Q einsetzten.
okee danke 
also so:
[(n%2==0) ^ wp(“c(n) = 0.5n;”, (n>=0) ^ (c(n) = 0.25((4n + 1) - (2n + 1) (-1)^n))]
v [(n%2==1) ^ wp("c(n)=0.5(3n + 1);", (n>=0) ^ (c(n) = 0.25((4n + 1) - (2n + 1) *(-1)^n))]
und jetz kann ich ja dann die fälle auseinander ziehen:
Fall 1:
wp(“c(n)=0.5n;”, (n>=0) ^ (c(n) = 0.25((4n + 1) - (2n + 1) *(-1)^n))
wp(“c(n)=0.5n;”, (n>=0) ^ (c(n) = 0.25((4n + 1) - (2n + 1) *(-1)^n))
wp("(n>=0)^0,5n = 0.25((4n + 1) - (2n + 1) *(-1)^n))
stimmt das dann so oder muss ich für jedes n c(n) einsetzen? nee nur für c(n) oder?
c(n) wird duch c(n) erstzt, stimmt also so.
Kleine Formsache noch: lass das “wp” in der letzten Zeile weg. Warum? Wenn du den Code eingesetzt hast ins wp kommt deine Vorbedingung raus, d.h. ein wp ist hier überflüssig.
Also: (n>=0)^ (0,5n = 0.25((4n + 1) - (2n + 1) *(-1)^n))
Was genau meinst du eigentlich mit Fällen?? Du kannst, der Einfachkeit halber, die wp-Statements aus dem Batzen rausnehem, auflösen, und wieder einsetzten. Das ist aber eigentliche keine Fallunterscheidung. Kurz: du brauchst keine Fallunterscheidung
ja ich dachte ich ziehe die if /else auseinander. So hatten wirs in der Übung gemacht, aber ja bei der Aufgabe ist es vermutlich einfacher es direkt einzusetzen.
((n>=0)^0,5n = 0.25((4n + 1) - (2n + 1) *(-1)^n))
((n>=0)^0,5n = n + 0,25 - (0,5n + 0,25) *(-0,25)^n)
((n>=0)^0,5n = n + 0,25 - (0,125n + 0,0625)^n)
((n>=0)^n = 2n + 0,5 - (0,25n + 0,125)^n)
Weiter kann ich das jetz aber ja nicht mehr vereinfachen oder ?
ist das dan quasi die Lösung? sieht ha ned schön aus.
Das hast du doch gemacht! Es steht doch da […] v […], auf Deutsch: if - else.
Was ist jetzt mit dem ganzen Rest?? Du hast hier nur einen Teil verwendet…
bei der aufgabe ist das endergebnis true