LastMinute: Invariante in Methoden mit mehreren Schritten

Benutzeravatar
rosh08
Erstie
Erstie
Beiträge: 14
Registriert: 10. Apr 2010 17:50
Wohnort: Frankfurt am Main

LastMinute: Invariante in Methoden mit mehreren Schritten

Beitrag von rosh08 »

Aus der Praxis kennen wir viele Lösungen zu den Programmierproblemen, die nicht am Stück in einer Schleife umgefasst werden, sondern zB nach der Schleife wird noch evtl. paar weitere Schritte benötigt, um das Endergebnis zurückzuliefern, wie kann man in solchen Fällen EINE Invariante erwähnen, die vor, während und nach der Schleife stimmt und somit für den Korrektheitsbeweis gilt??

Ein Beispiel der vom letzten Semester (überarbeitet) …
Geben sind 2 Strings s1 und s2, gesucht ist eine Methode, die s1 mit s2 lexikographische vergleicht (d.h. bestimmt ob s1 in einem Wörterbuch vor dem s2 kommt oder nachher?)


Vielleicht denkt man sich zuerst schnell so ein Entwurf als Lösung aus, die doch richtig ist aber man keine richtige Invariante dafür nennen kann!

Code: Alles auswählen

int compareS(String s1, String s2) {

        for (int i =0; i<s1.length() || i<s2.length; i++){ 
            if (s1.charAt(i) < s2.charAt(i)) return -1;
            if (s1.charAt(i) > s2.charAt(i)) return 1; 
        }
        
        // If one of the String is a Substring of the other
        if(i == s1.length() && i == s2.length()) return 0;
        if(i == s1.length()) return -1;
        if(i == s2.length()) return 1;
    }
Natürlich man kann nach wieder Überlegung die weiteren Abbruchbedingungen da unten mit in die Schleife einpacken (mit korrektem Reihenfolge) und somit die Aufgabe iterativ lösen und eine gültige Invariante für die Schleife erwähnen, aber nur als ein Lösungsbeispiel, das für die nicht-beweisbedürftigen Fälle OK ist aber hier unbrauchbar, denn eine Invariante zu bestimmen ist meines Wissens nach unmöglich… und angenommen, dass man in einer Klausur sofort schreibt, was einem einfällt! "

Prof. Karsten Weihe
Dozentin/Dozent
Beiträge: 1824
Registriert: 21. Feb 2005 16:33

Re: LastMinute: Invariante in Methoden mit mehreren Schritten

Beitrag von Prof. Karsten Weihe »

rosh08 hat geschrieben:Aus der Praxis kennen wir viele Lösungen zu den Programmierproblemen, die nicht am Stück in einer Schleife umgefasst werden, sondern zB nach der Schleife wird noch evtl. paar weitere Schritte benötigt, um das Endergebnis zurückzuliefern, wie kann man in solchen Fällen EINE Invariante erwähnen, die vor, während und nach der Schleife stimmt und somit für den Korrektheitsbeweis gilt??
Die Invariante ist ja nicht identisch mit dem Korrektheitsbeweis, sondern "nur" ein wesentlicher Bestandteil des Korrektheitsbeweises :!: :idea:

Bei den meisten Algorithmen in der GdI II folgte die Korrektheit der Ergebnisse so unmittelbar aus der Invariante, das der Unterschied vielleicht nicht immer klar wird. In Ihrem Beispiel wird offensichtlich, dass es doch einen Unterschied geben muss.

Die Invariante der for-Schleife in Ihrem Codebeispiel ist, dass die beiden Strings nach der i-ten Iteration bis zum Index i einschließlich identisch sind. Daraus folgt unmittelbar, dass die beiden Strings bis min{s1.length,s2.length} identisch sind, falls die Schleife nicht vorzeitig abbricht. Daraus wiederum folgt unmittelbar, dass entweder beide Strings identisch sind, oder dass einer ein Präfix des anderen ist. Diese drei Fälle werden in den drei unteren if's abgefragt. Gemäß Spezifikation von compare und gemäß der Setzung, dass ein Präfix lexikographisch vorgeordnet sind, werden diese drei Fälle in diesen drei if's offensichtlich korrekt abgehandelt.

Und das ist schon - in betont ausführlicher (und angeratener) Form - die in diesem Fall nicht ganz triviale Brücke von der Invariante zur Korrektheit der Ergebnisse :!: :idea: 8)

BTW: Müsste in der Fortsetzungsbedingung der for-Schleife nicht "&&" statt "||" stehen?

KW

Benutzeravatar
rosh08
Erstie
Erstie
Beiträge: 14
Registriert: 10. Apr 2010 17:50
Wohnort: Frankfurt am Main

Re: LastMinute: Invariante in Methoden mit mehreren Schritten

Beitrag von rosh08 »

Danke für die #LastMinute Erklärung! Das Missverständnis, dass man die weiteren Bedingungen nicht in den Korrektheitsbeweis miteinbeziehen kann, könnte mich teuer zu stehen kommen!
Also ich habe am Ende es All-In-One geschrieben und alle Fälle in der Schleife berücksichtigt… Aber frage mich trotzdem ist es richtig mit einem Loop der mit true weiterläuft, bis es mit einem der ifs gestoppt wird? Und kann man in dem Fall sagen: Nach jeder Iteration i>=0 sind entweder die Substrings s1[0...i] und s2[0...i] identisch oder einer ist dem anderen vorgeordnet ?

Code: Alles auswählen

 int compareS(String s1, String s2) {

        for (int i =0; true; i++){
            if(i == s1.length() && i == s2.length()) return 0;
            if (i == s1.length()) return -1;
            if (i == s2.length()) return 1;
            if (s1.charAt(i) < s2.charAt(i)) return -1;
            if (s1.charAt(i) > s2.charAt(i)) return 1;
        }
    }
PS: zu || war gedacht, dass i das Ende des kürzeren Strings erreicht!

Prof. Karsten Weihe
Dozentin/Dozent
Beiträge: 1824
Registriert: 21. Feb 2005 16:33

Re: LastMinute: Invariante in Methoden mit mehreren Schritten

Beitrag von Prof. Karsten Weihe »

rosh08 hat geschrieben:Das Missverständnis, dass man die weiteren Bedingungen nicht in den Korrektheitsbeweis miteinbeziehen kann, könnte mich teuer zu stehen kommen!
Ich hoffe (und bilde mir ein), dass das genaue Lesen der Aufgabenstellung Sie davor bewahren wird. 8)

rosh08 hat geschrieben: Also ich habe am Ende es All-In-One geschrieben und alle Fälle in der Schleife berücksichtigt… Aber frage mich trotzdem ist es richtig mit einem Loop der mit true weiterläuft, bis es mit einem der ifs gestoppt wird?
Ist was richtig? :roll:

Pronomen sind der Feind des präzisen, unmissverständlichen Ausdrucks (nicht nur in Informatik) :!: :shock:

rosh08 hat geschrieben: Und kann man in dem Fall sagen: Nach jeder Iteration i>=0 sind entweder die Substrings s1[0...i] und s2[0...i] identisch oder einer ist dem anderen vorgeordnet ?
Invariante ist doch offenbar, dass die beiden Substrings bis i einschließlich nach der i-ten Iteration identisch sind.

Korrektheit folgt jetzt einfach so, wieder ausführlich:

1. Nach Induktionsvoraussetzung sind die Substrings bis i-1 einschließlich identisch. Wenn diese beiden Substrings identisch mit den beiden Strings sind (erstes if), dann sind die beiden Strings identisch, und Rückgabe 0 ist korrekt.

2. Im zweiten und dritten if wird abgefragt, ob einer der beiden Strings Präfix des anderen ist, und dann sind Rückgabe .1 bzw. +1 korrekt gemäß der Definition, dass ein Präfix immer vorgeordnet ist.

3. Wird am aktuellen Index i eine Ungleichheit festgestellt, dann entscheidet dieses Zeichen aufgrund der Induktionsvoraussetzung,

Es fehlt nur noch, sich (und den Leser/Korrektor) zu vergewissern: Diese drei Fälle decken alle möglicherweise auftretenden Fälle ab.
rosh08 hat geschrieben: PS: zu || war gedacht, dass i das Ende des kürzeren Strings erreicht!
Ja, aber wird das nicht gerade durch "&&" statt "||" erreicht :?:

KW

Benutzeravatar
rosh08
Erstie
Erstie
Beiträge: 14
Registriert: 10. Apr 2010 17:50
Wohnort: Frankfurt am Main

Re: LastMinute: Invariante in Methoden mit mehreren Schritten

Beitrag von rosh08 »

Ist was richtig?
Die Frage war zu Basic! :oops: Also ob man eine Schleife ohne Abbruchbedingung (im Head) definieren kann? -Die Antwort habe ich selbst: Solange es sicher terminiert, Ja! :wink:
Ja, aber wird das nicht gerade durch "&&" statt "||" erreicht
Doch! :oops:

Antworten

Zurück zu „Archiv“