Korrektheitsbeweis für lineare Liste

fy06keju
Neuling
Neuling
Beiträge: 7
Registriert: 5. Sep 2016 16:52

Korrektheitsbeweis für lineare Liste

Beitrag von fy06keju » 17. Sep 2016 10:39

Guten Tag, ich habe mal ein Korrektheitsbeweis für eine lineare Liste durchgeführt.
Konkret gesagt handelt es sich um die Aufgabe 3.1.6 remove(rekursiv) vom JavaÜbungsblatt.
Ich bitte um Feedback :!:

hier mein Code:

Code: Alles auswählen

public boolean remove(ListItem<T> list, T element) {
	if(list ==null) return false;
	else {
		if(list.key.equals(element)) {
			if(list.next != null)
			  list.next.back = list.back;
			if(list.back != null)
			  list.back.next = list.next;
			else
			  list = list.next;			
			  return true;
		}
	          return remove(list.next, element); }
Funktion: überprüft ob der zweite Parameter mindestens einmal als Schlüsselwert im ersten Parameter, also in der Liste vorkommt, wenn ja wird ein einzelnes Vorkommen entfernt.

Input:
-eine korrekt gebildete lineare Liste list, welche auf den Kopf einer korrekt gebildeten Liste verweist. Außerdem ist das Attribut key bei keinem ListenElement null.
-ein Element 'element' vom Typ T

Output: true, wenn in der Liste in Vorkommen gleich 'element' gefunden und gelöscht wird,sonst false

Wohldefiniertheit: Überlauf unmöglich, da keine arithmetischen Operationen oder Methoden mit arithmetischen Rückgaben vorkommen
NullPointerException unmöglich aufgrund der Einschränkung des Inputs

Terminierung : liste == null oder list.key.equals(element), dh. es wurde in der Liste ein Element mit dem zu löschenden Wert gefunden.

Variante: actElement = actElement.next

Invariante: falls ein Vorkommen gleich dem zweiten Parameter in der Liste gefunden wird, wird ein einzelnes Vorkommen aus der Liste entfernt.

Induktionsanfang: wenn liste == null, so wurde offensichtlich kein Vorkommen gleich 'element' in der Liste gefunden, sodass korrekterweise false zurückgeliefert wird.

Induktionsschritt: Fallunterscheidung:
wenn die liste != null , wird überprüft, ob der Wert des aktuellen Vorkommens der Liste dem Wert 'element' entspricht, falls ja, werden seine back- und next-verweise, sobald diese existieren, gelöscht. Danach bricht die Rekursion ab und die weiteren ListenElemente werden nicht mehr betrachtet.
Wenn der Wert des aktuellen Elements nicht dem Wert 'element' entspricht, so wird der nächste Element der Liste rekursiv aufgerufen und nach Gleichheit des Wertes überprüft. Falls bis zum Ende der Liste( liste == null) kein Vorkommen gleich 'element' gefunden wurde, gibt die Funktion korrekterweise false zurück.
D.h. es wird auf jeden Fall, sobald ein Vorkommen gleich dem zweiten Parameter 'element' gefunden wird, nur ein einzelnes Vorkommen aus der Liste entfernt.

Korrektheit: Dank der Variante und Abbruchbedingung wird nach endlich vielen Rekursionsschritten das Ende der Liste erreicht und somit terminiert der Algorithmus. Die Invariante bleibt bis zum Ende erhalten, denn wenn bis zum Ende der Liste, also liste null ist, wurde kein Listenelement gleich dem Wert 'element' gefunden und liefert korrekterweise false zurück.

yokop
Windoof-User
Windoof-User
Beiträge: 28
Registriert: 13. Apr 2016 12:49

Re: Korrektheitsbeweis für lineare Liste

Beitrag von yokop » 17. Sep 2016 11:55

Bin auch kein Experte also alle Angaben ohne Gewähr :D
fy06keju hat geschrieben: Funktion: überprüft ob der zweite Parameter mindestens einmal als Schlüsselwert im ersten Parameter, also in der Liste vorkommt, wenn ja wird ein einzelnes Vorkommen entfernt.
Vielleicht etwas unnötig kompliziert formuliert, besser wäre wahrscheinlich sowas wie: Löscht das erste Vorkommen eines Schlüsselwertes element, falls dieser ein Teil der Liste ist. (Einfach die Spezifikation in der Aufgabenstellung)
fy06keju hat geschrieben: Input:
-eine korrekt gebildete lineare Liste list, welche auf den Kopf einer korrekt gebildeten Liste verweist. Außerdem ist das Attribut key bei keinem ListenElement null.
-ein Element 'element' vom Typ T
Der erste Satz macht für mich wenig Sinn. Gemeint ist wohl: Ein Listenelement list != null, welches auf den Kopf einer korrekt gebildeten linearen Liste zeigt. Das mit dem key != null ist okay.
Bei dem zweiten Satz vielleicht noch erwähnen, dass es sich um den zu löschenden Schlüsselwert handelt.
fy06keju hat geschrieben: Output: true, wenn in der Liste in Vorkommen gleich 'element' gefunden und gelöscht wird,sonst false.
Meiner Meinung nach wieder etwas "komisch" formuliert.
true, falls element ein Teil der Liste ist und das erste Vorkommen dieses Wertes gelöscht wurde, sonst false.
Eigene Frage: Sollte man hier hinzufügen, dass auch false für eine leere Liste ausgegeben wird ?
fy06keju hat geschrieben: Invariante: falls ein Vorkommen gleich dem zweiten Parameter in der Liste gefunden wird, wird ein einzelnes Vorkommen aus der Liste entfernt.
Das ist für mich nicht wirklich eine Invariante sondern die Spezifikation der Methode.
Ich hätte geschrieben: Nach einem Rekursionsschritt wurde das Element entweder gelöscht (und die Funktion terminiert) oder noch nicht gefunden.
fy06keju hat geschrieben: Induktionsanfang: wenn liste == null, so wurde offensichtlich kein Vorkommen gleich 'element' in der Liste gefunden, sodass korrekterweise false zurückgeliefert wird.
Hier kann man vorher noch den Induktionsparameter erwähnen. Es bietet sich eine Induktion über die Länge der Liste an.
fy06keju hat geschrieben: Induktionsschritt: Fallunterscheidung:
wenn die liste != null , wird überprüft, ob der Wert des aktuellen Vorkommens der Liste dem Wert 'element' entspricht, falls ja, werden seine back- und next-verweise, sobald diese existieren, gelöscht. Danach bricht die Rekursion ab und die weiteren ListenElemente werden nicht mehr betrachtet.
Wenn der Wert des aktuellen Elements nicht dem Wert 'element' entspricht, so wird der nächste Element der Liste rekursiv aufgerufen und nach Gleichheit des Wertes überprüft. Falls bis zum Ende der Liste( liste == null) kein Vorkommen gleich 'element' gefunden wurde, gibt die Funktion korrekterweise false zurück.
D.h. es wird auf jeden Fall, sobald ein Vorkommen gleich dem zweiten Parameter 'element' gefunden wird, nur ein einzelnes Vorkommen aus der Liste entfernt.
Hier stellt sich die Frage wie genau man das beschreiben muss. Ich finde aber, dass das nicht wirklich ein Induktionsschritt ist, sondern eher eine Nacherzählung wie die Methode gesamt funktioniert.

Sei die Länge der Liste k+1, dann ist nach Induktionsvoraussetzung das zu löschende Element in der Teilliste der Länge k noch nicht gefunden.
Wenn der aktuelle Schlüsselwert nun mit element übereinstimmt, so wird das Listenelement korrekterweise gelöscht und true zurückgegeben.
Im anderen Fall mit !key.equals(element) ist element also auch nicht Teil der Liste der Länge k+1, also bleibt die Invariante erhalten.

fy06keju
Neuling
Neuling
Beiträge: 7
Registriert: 5. Sep 2016 16:52

Re: Korrektheitsbeweis für lineare Liste

Beitrag von fy06keju » 17. Sep 2016 22:15

Vielen Dank für die Verbessung.

Antworten

Zurück zu „Archiv“