Stack: Klasseninvariante

[sh33p]

Versuche mir gerade verzweifelt das Verständnis einer Klasseninvariante anzueignen.

Mein bisheriges Verständnis:

Klasseninvariante ist eine Bedingung, die in jedem Zustand eines Objektes einer Klasse K gilt, d.h nach der Initalisierung und vor und nach dem methodenaufruf.

Hierzu ein Beispiel:

public final class Stack {
    private int count; // aktuelle Zahl der Elemente - 1
    
    // Index des obersten Elements
    private int[] a = new int[10]; // Ablageplatz fuer die Elemente
    // a[0]...a[count] sind die gestapelten Elemente
    // a[count] ist das oberste, a[0] das unterste
   // INV: -1 <= count <= 9

    public Stack () { // Konstruktor, erzeugt den leeren Stapel
    count = -1;
  }

    //Leseoperation, keine Zustandsaenderung
     public int top() { // liefert das oberste Element
    // Vorbedingung: Stapel nicht leer
    if (count<=9 && count>=0) {
    return a[count];
    } else
    return -999;
   }

    // Schreiboperationen, zustandsaendernd, ohne Ergebnis
    // veraendert Stapel-Zustand: legt Element ab
     public void push(final int x){
     // Vorbedingung: Stapel nicht voll
     if (count<9) {
     count++;
    a[count] = x;
}
}
    public void pop(){ // veraendert Stapel-Zustand: entfernt oberstes Element
   // Vorbedingung: Stapel nicht leer
   if (count>=0) {
   count--;
   }
 }
 }

Wenn man sich nun die Klasse anschaut, glaube ich,das die Klasseninvariante des Stacks lautet, das der Stack niemals leer sein darf.
Richtig?:bahnhof: Ansonsten bitte korrigieren

 

[IhrBenutzername]

Wenn man sich nun die Klasse anschaut, glaube ich,das die Klasseninvariante des Stacks lautet, das der Stack niemals leer sein darf.
Richtig?:bahnhof: Ansonsten bitte korrigieren

Wie kommst du darauf? Wenn ich einen neuen Stack erstelle ist der doch leer, oder wird irgendwo automatisch was eingefügt?

PS: du solltest entweder deine Variable count umbenennen oder ihr die tatsächliche Anzahl von Elementen im Stack zuweisen, dann wär deine falsche Schlußfolgerung wahrscheinlich gar nicht erst zustande gekommen.

 

[ThreadPool]

Klasseninvariante ist eine Bedingung

Es muss nicht nur genau eine Bedingung sein, eine Klasseninvariante kann durchaus durch mehrere Bedingungen beschrieben werden.

 

[sh33p]

Wie lauten denn dann die Bedingungen der Klasseninvariante des Stacks?
Nur wenn count sich im bereich -1 (ich weiß, war dumm mit -1) und 9 bewegt, ist der Stack in einem legalen Zustand.

 

[ThreadPool]

Wie lauten denn dann die Bedingungen der Klasseninvariante des Stacks?

Kommt drauf an wie es implementiert ist. In deinem Code sollte deine Invariante reichen, da du mit -1 beginnst.

Eine andere Möglichkeit wäre z.B. folgende Implementierung mit einer etwas anderen Klasseninvariante.

final class StackInvariantException extends RuntimeException {
}

final class Stack {
	// Klasseninvariante
	// capacity >= 1
	// capacity >= pos >= 0
	// capacity = data.length

	//
	// fields
	//
	private int _capacity, _pos;
	private Object[] _data;

	//
	// constructors
	//
	public Stack(int capacity) {
		_pos = 0;
		_capacity = Math.max(capacity, 1);
		_data = new Object[_capacity];
	}

	//
	// methods
	//
	public boolean isEmpty() {
		return _pos <= 0;
	}

	public boolean isFull() {
		return _pos >= _capacity;
	}

	public Object top() throws StackInvariantException {
		if (isEmpty())
			throw new StackInvariantException();
		return _data[_pos-1];
	}

	public void push(Object o) throws StackInvariantException {
		if (isFull()) 
			throw new StackInvariantException();
		_data[_pos++] = o;
	}

	public void pop() throws StackInvariantException {
		if (isEmpty())
			throw new StackInvariantException();
		_pos--;
	}
}