Schleifeninvariante: Richtig gemacht ?

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

Re: Schleifeninvariante: Richtig gemacht ?

Beitrag von Prof. Karsten Weihe »

Hallo hat geschrieben:Hallo, hier komme ich nochmal mit einen Code aus dem Internet, der hier für jeden Knoten ein duplikaten als node.left einfügt.
Also Spezifikation von doubleTree(Node): Die Methode doubleTree(Node) erwartet, dass node die Wurzel eines korrekten binären Baumes ist, und modifiziert diesen Baum wie folgt:

1. Falls der Baum nicht leer ist (also falls node != null), modifiziert doubleTree(node) diesen Baum, indem für jeden Knoten x ein neuer Knoten zwischen x und x.left eingefügt wird, auf den x.left dann verweist. Mit anderen Worten: Der Knoten, der vorher x.left war, ist nun x.left.left (bzw. es gilt x.left.left == null hinterher, falls vorher x.left == null war). Bei dem vorher im Baum enthaltenen Knoten x ändert sich ansonsten nichts. Für den neuen Knoten x.left gilt x.left.data == x.data und x.left.right == null.

2. Ist der Baum hingegen leer (also node == null), dann wird der Baum nicht modifiziert.

Bemerkung: Sie sehen an diesem Beispiel gut, warum die Spezifikationen in den Klausuraufgaben immer so umfangreich sind. :idea:

Hallo hat geschrieben: Ind. Behauptung: Für Bäume mit der Höhe h liefert der Algorithmus korrekte Beispiele.
Was soll das heißen: "liefert ... korrekte Beispiele"? Warum schreiben Sie nicht einfach das, was Sache ist, nämlich dass der Algorithmus das gemäß Spezifikation korrekte Ergebnis liefert?

Hallo hat geschrieben: Ind. Anfang: Für leere Bäume der Höhe h= -1, liefert der Algorithmus das korrekte Ergebnis, denn für einen leeren Baum mit node==null, würde sein node.left auch == null sein und immer noch ein leerer Baum werden.
Also, ich kann nachvollziehen, was Sie wohl damit meinen, dass node.left == null bei node == null gelte. Aber ich kann nicht mehr so ganz nachvollziehen, dass jemand im zweiten oder höheren Fachsemester eine solche Formulierung ernsthaft vorschlägt, denn Sie sollten ja wissen, dass der Zugriff auf node.left im Falle node == null nicht definiert ist (und daher zum Wurf einer Exception führt).

Ich denke, hier rächt sich jetzt, dass Sie keine Spezifikation formuliert haben, denn bei Abfassung der Spezifikation wäre Ihnen sicherlich aufgefallen, dass der Fall node == null gesondert zu spezifizieren ist -> vergleiche meinen Vorschlag für die Spezifikation oben.

Hallo hat geschrieben: Ind. Schritt: Nach jedem Rekursiven durchlauf wird an den Knoten mit der Höhe h ein neuer Knoten als linkes Kind angehängt mit gleichem Inhalt wie dessen Vaterknoten, der Knoten mit der Höhe h.
Nach dem rekursiven Durchlauf :?:

Benötigen Sie die Induktionsvoraussetzung denn gar nicht für Ihren Induktionsbeweis :?:

Wie würde ich da herangehen: Nach Induktionsvoraussetzung modifizieren die beiden rekursiven Aufrufe korrekt die beiden Teilbäume mit Wurzel node.left und node.right. Die letzten drei Zeilen hängen dann gemäß Spezifikation auch bei node einen neuen linken Nachfolger ein.

Hallo hat geschrieben: Gesamtkorrektheit : Dank der Variante, das mit jedem Rekursionsschritt eine Stufe tiefer im Baum abgestiegen wird, erreicht man die Abbruchbedingung (node==null) und der Algorithmus liefert einen gespiegelten Teilbaum zurück.
Wäre bei der Korrektur sicherlich zu akzeptieren. Klarer und auch konformer mit der Formulierung des Induktionsbeweises wäre die Variante meines Erachtens über die Induktionsvariable definiert: Die beiden Teilbäume mit Wurzel node.left und node.right haben eine strikt kleinere Höhe als der (Teil-)baum mit Wurzel node.

KW

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

Re: Schleifeninvariante: Richtig gemacht ?

Beitrag von Prof. Karsten Weihe »

uffie hat geschrieben:
Aus dieser Induktionshypothese folgt dann sofort, dass der mit Put ausgegebene Wert gleich \(\sum_{j=1}^{n_0}\) ist.[...]
\(\sum_{j=1}^{n_0}j\) oder? :mrgreen:
Offensichtlich haben Sie meinen Post so gut verstanden, dass Sie ihn korrigieren konnten. :oops: 8) :)

KW

Hallo
Endlosschleifenbastler
Endlosschleifenbastler
Beiträge: 162
Registriert: 22. Apr 2015 19:03

Re: Schleifeninvariante: Richtig gemacht ?

Beitrag von Hallo »

Hallo, hier nochmal mit einen neuen Code.

( Ich werde hier meine Übungen so lange posten bis ich die Korrektheit des Algorithmus im Schlaf kann :x :roll: :evil: )

Code: Alles auswählen

*/ 
public boolean sameTree(BinaryTree other) { 
 return( sameTree(root, other.root) ); 
}
/** 
 Recursive helper -- recurs down two trees in parallel, 
 checking to see if they are identical. 
*/ 
boolean sameTree(Node a, Node b) { 
  // 1. both empty -> true 
  if (a==null && b==null) return(true);

  // 2. both non-empty -> compare them 
  else if (a!=null && b!=null) { 
    return( 
      a.data == b.data && 
      sameTree(a.left, b.left) && 
      sameTree(a.right, b.right) 
    ); 
  } 
  // 3. one empty, one not -> false 
  else return(false); 
} 

Spezifikation: Untersucht zwei verschiedene Bäume auf Identität der Struktur.
1. Sind beide Bäume leere Bäume, dann haben sie auch identische Struktur.
2. Sind beide nicht leere Bäume geht der Algorithmus Knoten für Knoten durch (a.left, b.left) (a.right,b.right) und prüft ob beide entweder != null oder beide == null sind.

Ind. Behauptung: Für zwei Bäume der Höhe h liefert der Algorithmus das korrekte Ergebnis.

Ind. Anfang: Für zwei leere Bäume der Höhe h = -1, sind beide Bäume auch von der Struktur her identisch.

Ind. Schritt: Nach Induktionsvoraussetzung werden die beiden Teilbäume (a.left && b.left und a.right && b.right) der zwei Bäume (a und b) durch die zwei Rekursiven Aufrufe geprüft und der Algorithmus liefert für Bäume der Höhe h den Korrekten Ergebnis.

Gesamtkorrektheit: Dank der Variante, dass der Algorithmus immer ein Stufe tiefer im Baum hinabsteigt terminiert er auch bei Abbruchbedingung, dass einer von den beiden Teilbäume die er durchsucht ungleich sind (a.left == null && b.left!=null oder a.right == null && b.right!=null oder umgekehrt) oder das beide gleich null sind, also entweder der Linke oder der Rechte Teilbaum beide gleich null sind (a.left == && b.left == null oder a.right == && b.right == null)

Vielen Dank.

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

Re: Schleifeninvariante: Richtig gemacht ?

Beitrag von Prof. Karsten Weihe »

Hallo hat geschrieben: ( Ich werde hier meine Übungen so lange posten bis ich die Korrektheit des Algorithmus im Schlaf kann :x :roll: :evil: )
Die richtige Einstellung :!: :idea: :twisted:

Hallo hat geschrieben: Spezifikation: Untersucht zwei verschiedene Bäume auf Identität der Struktur.
1. Sind beide Bäume leere Bäume, dann haben sie auch identische Struktur.
2. Sind beide nicht leere Bäume geht der Algorithmus Knoten für Knoten durch (a.left, b.left) (a.right,b.right) und prüft ob beide entweder != null oder beide == null sind.
Und wenn einer der Bäume leer und der andere nicht leer ist :?: :roll:

Generell: Die Spezifikation beschreibt nicht, was der Algorithmus tut. sondern sie beschreibt Input und Output. Also so etwas wie:

Gegeben sind zwei Bäume, das Ergebnis ist true genau dann, wenn die beiden Bäume identische Struktur haben, das heißt: Es gibt eine (1:1)-Korrespondenz (=Bijektion) zwischen den Knotenmengen der beiden Bäume, so dass für einen Knoten x in dem einen Baum und dem korrespondierenden Knoten y im anderen Baum gilt: x.left == null gdw y.left == null und x.right == null gdw y.right == null.

Hallo hat geschrieben: Ind. Behauptung: Für zwei Bäume der Höhe h liefert der Algorithmus das korrekte Ergebnis.
Und wenn beide Bäume unterschiedliche Höhe haben, darf der Algorithmus dann ein inkorrektes Ergebnis liefern :?: :roll:

Hallo hat geschrieben: Ind. Anfang: Für zwei leere Bäume der Höhe h = -1, sind beide Bäume auch von der Struktur her identisch.
Ok.

Hallo hat geschrieben: Ind. Schritt: Nach Induktionsvoraussetzung werden die beiden Teilbäume (a.left && b.left und a.right && b.right) der zwei Bäume (a und b) durch die zwei Rekursiven Aufrufe geprüft und der Algorithmus liefert für Bäume der Höhe h den Korrekten Ergebnis.
Was soll uns das sagen, die Bäume werden geprüft? Nicht zum ersten Mal - warum schreiben Sie nicht einfach das, was Sache ist: Nach Induktionsvoraussetzung sind die Ergebnisse für besagte Teilbäume korrekt.

Wenn ich ehrlich sein soll: Mich beschleicht das Gefühl, dass Ihr Problem nicht speziell mit Korrektheitsbeweisen zu tun hat, sondern allgemeiner mit präzisem sprachlichem Ausdruck.

KW

Hallo
Endlosschleifenbastler
Endlosschleifenbastler
Beiträge: 162
Registriert: 22. Apr 2015 19:03

Re: Schleifeninvariante: Richtig gemacht ?

Beitrag von Hallo »

Wenn ich ehrlich sein soll: Mich beschleicht das Gefühl, dass Ihr Problem nicht speziell mit Korrektheitsbeweisen zu tun hat, sondern allgemeiner mit präzisem sprachlichem Ausdruck.
Da haben Sie recht und da stimme ich auch ihnen zu. Aber zu Beispiel bei meinem Ind. Schritt da kann man doch nachvollziehen dass ich mit 'geprüft', geprüft auf identische Struktur meine. Haben sie eigentlich noch Kommentare zu der Gesamtheit oder ist dazu nicht mehr zu sagen ?

Und wegen der Ind. Behauptung,
Und wenn beide Bäume unterschiedliche Höhe haben, darf der Algorithmus dann ein inkorrektes Ergebnis liefern :?: :roll:
das habe ich auch gerade erst jetzt bemerkt, ich glaube ich hätte für die zwei Bäume verschiedene Höhenvariablen nehmen sollen, also ,,für zwei Bäume der Höhe h und b" zum Beispiel..oder ?


Ich kann aber leider nicht Nachvollziehen warum Sie meine Ind. Schritt Formulierung nicht korrekt finden. Ich meine, ich muss doch erklären was jetzt bei den nächsten Teilbäume passiert ? Und da einfach zu schreiben :
Nach Induktionsvoraussetzung sind die Ergebnisse für besagte Teilbäume korrekt.
Ich befürchte wenn ich so eine Formulierung in der Klausur schreibe werde ich nicht die volle Punktzahl kriegen und die Korrektur wird meinen Sie könnte meine Formulierung nicht nachvollziehen.

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

Re: Schleifeninvariante: Richtig gemacht ?

Beitrag von Prof. Karsten Weihe »

Hallo hat geschrieben: Da haben Sie recht und da stimme ich auch ihnen zu. Aber zu Beispiel bei meinem Ind. Schritt da kann man doch nachvollziehen dass ich mit 'geprüft', geprüft auf identische Struktur meine.
Na ja, da ich weiß, worauf das Ganze hinausläuft, kann ich das natürlich nachvollziehen, aber ich bin dezidiert der Meinung, dass das nicht der Maßstab sein kann. Bei Ihrem Arzt oder Rechtsanwalt erwarten Sie doch auch, dass er sich korrekt und treffend formelhaft ausdrückt, so dass zumindest Fachkollegen ihn verstehen, auch wenn sie nicht vorher wissen, was er eigentlich meinen sollte. Und als Informatiker programmieren Sie vielleicht später Steuerungssoftware für AKWs o.ä., und dann wäre es für das Fortbestehen des Kontinents schon vorteilhaft, wenn Sie die treffenden Formulierungen bei der Kommunikation mit den Energieingenieuren verwenden... :shock:
Hallo hat geschrieben: Haben sie eigentlich noch Kommentare zu der Gesamtheit oder ist dazu nicht mehr zu sagen ?
Was konkret vermissen Sie?
Hallo hat geschrieben: Und wegen der Ind. Behauptung,
Und wenn beide Bäume unterschiedliche Höhe haben, darf der Algorithmus dann ein inkorrektes Ergebnis liefern :?: :roll:
das habe ich auch gerade erst jetzt bemerkt, ich glaube ich hätte für die zwei Bäume verschiedene Höhenvariablen nehmen sollen, also ,,für zwei Bäume der Höhe h und b" zum Beispiel..oder ?
Entscheidend ist, dass Sie eine Induktionsvariable definieren, die eine korrekte vollständige Induktion erlaubt. Ich denke, ich würde das Maximum oder das Minimum beider Höhen als Induktionsvariable nehmen. Ob man dann noch Kürzel für die Höhen beider Bäume braucht, weiß ich nicht, das wird man bei der Ausformierung merken.
Hallo hat geschrieben: Ich kann ber leider nicht Nachvollziehen warum Sie meine Ind. Schritt Formulierung nicht korrekt finden. Ich meine, ich muss doch erklären was jetzt bei den nächsten Teilbäume passiert ?
Nein :!:

Das ist doch gerade der Gag bei der vollständigen Induktion, dass Sie blindlings die Induktionsvoraussetzung anwenden können. Schauen Sie doch einmal in Ihre Mathe-Skripte, da gibt es doch bestimmt Beweise für Summenformeln. Wird da beim Schritt n -> n+1 noch einmal etwas dazu gesagt, wie die Korrektheit für n zustande kommt? Ich vermute nein.
Hallo hat geschrieben: Und da einfach zu schreiben :
Nach Induktionsvoraussetzung sind die Ergebnisse für besagte Teilbäume korrekt.
Ich befürchte wenn ich so eine Formulierung in der Klausur schreibe werde ich nicht die volle Punktzahl kriegen und die Korrektur wird meinen Sie könnte meine Formulierung nicht nachvollziehen.
Das wäre der Satz, den ich in die Musterlösung schreiben würde, wenn ich diese Aufgabe stellen würde. Und daran hat sich die Korrektur zu orientieren. Und zwar nicht, weil das KWs persönliche Vorliebe wäre, sondern weil das 1:1 zum Prinzip der vollständigen Induktion gehört: Wenn ein Teilbaum die Bedingung erfüllt, dass die Induktionsvoraussetzung anwendbar ist, dann kann man sie ohne weitere Begründung anwenden.

KW

Hallo
Endlosschleifenbastler
Endlosschleifenbastler
Beiträge: 162
Registriert: 22. Apr 2015 19:03

Re: Schleifeninvariante: Richtig gemacht ?

Beitrag von Hallo »

Vielen Dank für ihre Antwort.

Hier nochmal einen anderen Programm, der überprüft ob ein binärer Baum symmetrisch ist oder nicht, also dass er sich an der Wurzel des Baumes spiegelt.

Code: Alles auswählen


		public boolean isSymmetric(TreeNode root){
		
		return (isSymmetric(root1, root2));}


		public boolean isSymmetricRec(TreeNode root1, TreeNode root2)
    {
	        if (root1 == null && root2 == null)
	        {
	           	 return true;
	        }
	        else if (root1 == null || root2 == null)
	        {
          		return false;
        }
	        
	        if (root1.value == root2.value)
	        {
	            if (isSymmetricRec(root1.left, root2.right))
	            
	                return isSymmetricRec(root1.right, root2.left);
	            }
	        }
	        return false;
	    }

Also, Spezifikation: Gegeben ist ein Baum. Das Ergebnis ist genau dann true wenn der Baum sich an seiner Wurzel spiegelt, also wenn es sich um einen symmetrischen Baum handelt. Es muss sich ergeben, dass root.value == root.value ist, und dass dann root.left.value == root.right.value ist.


Ind. Behauptung: Für einen Baum der Höhe h, liefert der Algorithmus das Korrekte Ergebnis.

Ind. Anfang: Für einen leeren Baum der Höhe h=-1 mit root==null, gilt auch dass der Baum symmetrisch ist.

Ind. Schritt. Nach Induktionsvoraussetzung sind die Ergebnisse für besagte Teilbäume korrekt.

Gesamtkorrektheit: Dank der Variante, dass der Algorithmus bei jede Rekursion eine Stufe tiefer im Baum hinabsteigt, erreicht er die Abbruchbedingung, dass (root1 == null && root2 == null) und liefert korrekte Ergebnisse.


Vielen Dank.
:oops:

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

Re: Schleifeninvariante: Richtig gemacht ?

Beitrag von Prof. Karsten Weihe »

Hallo hat geschrieben: Hier nochmal einen anderen Programm, der überprüft
Was ist eigentlich generell mit Ihrem Deutsch?

Hallo hat geschrieben: Also, Spezifikation: Gegeben ist ein Baum. Das Ergebnis ist genau dann true wenn der Baum sich an seiner Wurzel spiegelt, also wenn es sich um einen symmetrischen Baum handelt. Es muss sich ergeben, dass root.value == root.value ist, und dass dann root.left.value == root.right.value ist.
Diese Spezifikation sagt nichts aus über die Werte irgendeines Knotens außer root.left und root.right :!:

Sie müssten schon so etwas sagen wie: Es gibt eine 1:1-Korrespondenz (=Bijektion) der Knotenmenge auf sich selbst, so dass gilt:

1. Wenn x mit y korrespondiert, dann auch y mit x (d.h. die Korrespondenz ist symmetrisch).

2. root korrespondiert zu sich selbst.

3. Wenn x und y korrespondieren, dann ist x.left != null genau dann, wenn y.right != null, und in diesem Fall korrespondieren x.left und y.right.

4. Wenn x und y korrespondieren, dann ist x.value == y.value.

Don't panic: Wie Sie aus dem Klausurblatt mit Lücken herauslesen können, müssen Sie keine Spezifikationen selbst schreiben. Dieses Problem habe nur ich als Aufgabensteller. :wink:

Hallo hat geschrieben: Ind. Behauptung: Für einen Baum der Höhe h, liefert der Algorithmus das Korrekte Ergebnis.
Ok

Hallo hat geschrieben: Ind. Anfang: Für einen leeren Baum der Höhe h=-1 mit root==null, gilt auch dass der Baum symmetrisch ist.
Würde vermutlich bei der Korrektur akzeptiert. Aber es gibt zwei Möglichkeiten zur Verbesserung der Klarheit:

1. " Baum der Höhe h=-1 mit root==null" klingt so, als wären h=-1 und root==null zwei unabhängige Bedingungen, die zugleich gelten. Treffender wäre eine Formulierung wie "Baum der Höhe h=-1 (also root==null)", die klarmacht, dass h=-1 und root==null dasselbe aussagen.

2. Ich würde die aus der Mathematik wohlbekannte formelhafte Formulierung verwenden: Die vier Bedingungen in der Spezifikation sind bei einem leeren Baum trivialerweise erfüllt.

Hallo hat geschrieben: Ind. Schritt. Nach Induktionsvoraussetzung sind die Ergebnisse für besagte Teilbäume korrekt.
Na ja, von welchen "besagten" Teilbäumen sprechen Sie hier? Sie haben einen Satz von mir wörtlich kopiert, ohne zu berücksichtigen, dass die exakte Formulierung kontextspezifisch ist. :roll:

Hallo hat geschrieben: Gesamtkorrektheit: Dank der Variante, dass der Algorithmus bei jede Rekursion eine Stufe tiefer im Baum hinabsteigt, erreicht er die Abbruchbedingung, dass (root1 == null && root2 == null) und liefert korrekte Ergebnisse.
Wäre sicher zu akzeptieren.

KW

Hallo
Endlosschleifenbastler
Endlosschleifenbastler
Beiträge: 162
Registriert: 22. Apr 2015 19:03

Re: Schleifeninvariante: Richtig gemacht ?

Beitrag von Hallo »

Was ist eigentlich generell mit Ihrem Deutsch?
Professor Weihe, es gibt auch Studenten, die nicht aus Deutschland kommen (Ich wohne hier in Deutschland seit 1,5 Jahren.) und sich sehr bemühen verständliches/gutes Deutsch zu sprechen/schreiben. Ich bemühe mich grammatikalisch und sprachlich gut auszudrücken, manchmal gelingt das mir auch nicht.

Danke für die Korrektur der Aufgabe.

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

Re: Schleifeninvariante: Richtig gemacht ?

Beitrag von Prof. Karsten Weihe »

Wollen Sie die Klausuraufgaben lieber auf Englisch beantworten? Kann jeder bei mir gerne wählen. Die Aufgabenstellungen sind allerdings für alle deutsch.

KW

Hallo
Endlosschleifenbastler
Endlosschleifenbastler
Beiträge: 162
Registriert: 22. Apr 2015 19:03

Re: Schleifeninvariante: Richtig gemacht ?

Beitrag von Hallo »

Nein ich beantworte Sie lieber auf Deutsch weil ich jetzt die ganze Zeit auf Deutsch lerne und alle Übungen auf Deutsch löse. Ein paar Grammatikfehler sind doch nicht so schlimm.

Viele Grüße.

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

Re: Schleifeninvariante: Richtig gemacht ?

Beitrag von Prof. Karsten Weihe »

Hallo hat geschrieben:Nein ich beantworte Sie lieber auf Deutsch weil ich jetzt die ganze Zeit auf Deutsch lerne und alle Übungen auf Deutsch löse. Ein paar Grammatikfehler sind doch nicht so schlimm.[/[/
Wir tun bei der Korrektur ja unser Bestes, zu verstehen, was Sie meinen. :-)

KW

Hallo
Endlosschleifenbastler
Endlosschleifenbastler
Beiträge: 162
Registriert: 22. Apr 2015 19:03

Re: Schleifeninvariante: Richtig gemacht ?

Beitrag von Hallo »

public static Node reverseLinkedList(Node currentNode)
{
// For first node, previousNode will be null
Node previousNode=null;
Node nextNode;
while(currentNode!=null)
{
nextNode=currentNode.next;
// reversing the link
currentNode.next=previousNode;
// moving currentNode and previousNode by 1 node
previousNode=currentNode;
currentNode=nextNode;
}
return previousNode;
}
Hallo, hier nochmal ein anderes Programm, der eine Linked List umgekehrt als Ergebnis hat.

Ind. Behauptung: Für eine LinkedList n der Länge l als Input, liefert der Algorithmus eine korrekte umgekehrte LinkedList als output.

Ind. Anfang: Für eine leere Liste mit currentNode = null, terminiert der Algorithmus und liefert null (previousNode).

Ind. Schritt. Nach Induktionsvoraussetzung ist das Ergebnis für eine LinkedList der Länge l (der Input) korrekt, also es wird eine umgekehrte (reversed) LinkedList von der Eingabe geliefert (output).

Gesamtkorrektheit: Dank der Variante, dass der Pointer bei jeder Iteration auf den nächsten Listenelement zugreift, erreicht man die Abbruchbedingung (currentNode==null) und der Algorithmus Terminiert.

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

Re: Schleifeninvariante: Richtig gemacht ?

Beitrag von Prof. Karsten Weihe »

Hallo hat geschrieben: Ind. Behauptung: Für eine LinkedList n der Länge l als Input, liefert der Algorithmus eine korrekte umgekehrte LinkedList als output.
Wäre sicher zu akzeptieren.
Hallo hat geschrieben: Ind. Anfang: Für eine leere Liste mit currentNode = null, terminiert der Algorithmus und liefert null (previousNode).
Ebenso.
Hallo hat geschrieben: Ind. Schritt. Nach Induktionsvoraussetzung ist das Ergebnis für eine LinkedList der Länge l (der Input) korrekt, also es wird eine umgekehrte (reversed) LinkedList von der Eingabe geliefert (output).
Hier müssten Sie aber schon noch kurz schreiben, was die Zeilen machen, die Sie mit "reversing the link" überschrieben haben.
Hallo hat geschrieben: Gesamtkorrektheit: Dank der Variante, dass der Pointer bei jeder Iteration auf den nächsten Listenelement zugreift, erreicht man die Abbruchbedingung (currentNode==null) und der Algorithmus Terminiert.
Wäre wohl zu akzeptieren, auch wenn der dass-Satz etwas schwierig zu interpretieren ist.

KW

Sonne34
Windoof-User
Windoof-User
Beiträge: 26
Registriert: 3. Mai 2015 18:10

Re: Schleifeninvariante: Richtig gemacht ?

Beitrag von Sonne34 »

Da hier bei den Korrektheitsbeweisen auch immer auf die Spezifikation eingegangen wird, frage ich mich ob dies zur vollständigen Bearbeitung des Beweises notwendig ist? Oder ist im Falle einer solchen Aufgabe davon auszugehen, dass diese Spezifikation in der Aufgabenstellung steht?
Ich habe es doch richtig verstanden, dass wenn man Variante und Invariante beweisen soll, das mittels Induktion macht oder?

Freundliche Grüße

Antworten

Zurück zu „Archiv“