Hallo Leute,
ich bin neu in diesen Forum und wusste nicht ,in welche Kategorie diese Frage am besten passt.
Nun ; ich muss eine Schleife verifizieren;
< n>= 0 > VB
i = 0;
res = 0;
while(i<n){
i = i +1 ;
res = rest + iii;
}
< res (n*(n+1)/2)^2 > NB (der quardrierte kleine Gauß ^^ halt)
Ich komme einfach nicht auf die Invariante .Meine Idee wäre ; a ) i=n b)i<=res . Kann mir wer nen Tipp geben und am besten in zwei drei worten erkären ,wie man druf kommt.In der Vorlesung wurde es bei uns nur minimal erwähnt und an einfachen bespielen gezeigt ,wo man es direkt sieht.Die schweren(zumindest für mich xD) Sachen wurde gar nicht erkärt ,jedoch in der Hausaufgabe abverlangt.
Was ist das, Java-Script? Sogar da ergibt “< n>= 0 > VB” für mich keinen sinn. Damit man dir helfen kann, musst du dein Problem genauer beschreiben. Am besten in Prosa ohne Formelzeichen.
Ja, hab’s mal in “Theoretisches” verschoben, es geht bei dieser Frage ja nicht um eine Programmiersprache (abgesehen davon, dass das schon praktisch gültiger Java-Code ist…).
Ich hab’ zwar kurz überlegt, aber das ganze ist bei mir schon zu lange her, als dass ich “DIE” Antwort geben könnte. Deswegen alles unter Vorbehalt:
Soweit ich weiß, ist die Schleifeninvariante bis zu einen gewissen grad “beliebig” - man könnte true als Schleifeninvariante angeben. Nein - siehe EDIT2
Soweit ich weiß, muss die Schleifeninvariante einfach nur am Anfang und am Ende der Schleife erfüllt sein. Ja, aber man will noch mehr - siehe EDIT2
Soweit ich weiß, könnte man in diesem Fall einfach die Nachbedingung als Schleifeninvariante verwenden.
Inbsesondere beim letzten wäre ich auf Gegenargumente gespannt…
EDIT: Eigentlich bin ich mir beim letzten sogar ziemlich sicher, allerdings natürlich nicht mit ‘n’ sondern mit ‘i’:
res = (i*(i+1)/2)^2
EDIT2: Damit ergibt sich nämlich aus Schleifeninvariante+Abbruchbedinung=Nachbedingung - also genau das, was man will - wobei man die Abbruchbedingung als while(!(i==n)) schreiben müßte. Ein bißchen was dazu steht auch unter http://en.wikipedia.org/wiki/Loop_invariant …
Wenn die Nachbedingung als Schleifeninvariante gültig ist, dann ist das richtig. Die Invariante muss aus der Nachbedingung hervorgehen und die Vorbedingung muss aus der Schleifeninvariante ableitbar sein.
Hmnaja, die Wiki-Seite ist … ziemlich dünn -_- So ein “wichtiger” Punkt (von dem ich aber nicht sicher bin, ob es auch ein richtiger Punkt ist :D), wie die Abhängigkeit zwischen Invariante, Nachbdingung und Abbruchbedinung der Schleife, ist dort nicht mal angedeutet…
Die Abhängigkeit ist aber richtig (da bin ich mir sicher ), denn die Geschichte mit den Invarianten macht man ja nur, um die Korrektheit beweisen zu können. Und das ganze baut sich rückwärts auf.
Das Fällt dann in die Kategorie „Formaler Entwurf korrekter Software“.
Mir ging es vor allem darum, dass nicht klar ersichtlich was gemeint ist wenn man < … > VB schreibt. Im code gibts auch auf einmal eine Variable rest die nicht deklariert ist und eventuell nur ein Schreibfehler von res ist. Wenn sowas nicht klar ist ist jeder Versuch zu Helfen sinnlos.
Naja, es ist offensichtlich, dass das „rest“ eigentlich „res“ heißen soll. Und aus dem Kontext geht auch hervor, dass in der ersten Zeile mit VB „Vorbedingung“ gemeint und in der letzten mit NB die „Nachbedingung“. In der Nachbedingung fehlt auch ein = zwischen res und der Formel. Aber das ist alles ersichtlich.
Man muss sich ja nicht künstlich dumm stellen, oder?
*** Edit ***
Je mehr ich darüber nachdenke, desto klarer wird mir, dass die Schleifeninvariante [tex]res = \left( \frac{i\left( i + 1 \right)}{2}\right)^2[/tex] sein muss. Um die Korrektheit der Bedingung zu zeigen, müsste man die Regeln des in der Vorlesung verwendeten Kalküls anwenden. Dass das strikt rückwärts ist, stimmt so nicht, mit dem Hoare-Kalkül geht man vorwärts vor.
Alternativ kann die Schleifeninvariante auch ganz einfach per vollständiger Induktion bewiesen werden.
Die Nachbedingung gilt auf jeden Fall, da die Abbruchbedingung der Schleife i=n ist. Daher gilt die Invariante für den letzten Durchlauf. Für den ersten Durchlauf gilt die Invariante auch, das sieht man, wenn man einfach 1 für i einsetzt und den Wert ausrechnet.
war bei mir ähnlich … aus kurzen Vietnamkriegs-ähnlichen Flashback-Bruchstücken setzte sich nach und nach eine (trotzdem noch unvollständige) Erinnerung zusammen …
[QUOTE=cmrudolph;75990]
Die Nachbedingung gilt auf jeden Fall, da die Abbruchbedingung der Schleife i=n ist.[/QUOTE]
Darauf ist auf der Englischen Wikipedia-Seite ja bezug genommen, und das hatte ich ja auch so angedeutet (da muss man wohl pedantisch sein) : Die Bedingung, damit die Schleife weiterläuft, ist i<n. Die Abbruchbedingung ist demnach i>=n. Aaaber: Damit die Implikation „Invariante ^ Abbruchbedingung → Nachbedingung“ gilt, müßte die Abbruchbedingung i==n sein (und die Weiterlauf-Bedingung demnach while(i!=n)).
Ich danke euch.Damit hat sich eigentlich das ergeben, was ich mir gedacht habe.Die Kalküle sind so eine Sache gelernt, Klausur geschrieben, vergessen…Fuer mich sah diese Invariante zu simpel aus, aber wenn mehrere Leute (scheinbar mit Ahnung), das sagen, dann wird es so sein.
Richtig. i=n ist also „voreilig“ angenommen. Auch wenn man es „mit bloßem Auge“ sofort sieht, müsste es noch bewiesen werden. Mit der Eigenschaft, dass i pro Iteration um genau 1 wächst, ist das herleitbar.
Geht mir ähnlich. Ich hätte schwören können, dass wir damals das Hoare-Kalkül gemacht haben, aber ich bin mir auch sicher, dass wir rückwärts gearbeitet haben, was eher zum wp-Kalkül passt… Vielleicht haben wir auch beides gemacht? Denn die Hoare-Regeln kommen mir auch noch bekannt vor…
*** Edit ***
Kommt drauf an, was man später mal macht. Es gibt schon Bereiche, in denen Verifikation von Algorithmen gefordert wird. Und dann braucht man sowas.
So simpel ist sie ja gar nicht, der Beweis ist sicherlich gar nicht soo einfach. Aber das musst du selbst probieren (mit den dir an die Hand gegebenen Kalkül-Regeln).
), denn die Geschichte mit den Invarianten macht man ja nur, um die Korrektheit beweisen zu können. Und das ganze baut sich rückwärts auf.