SE2 Testat - Design by Contract

designy_by_contract.md

Aufgabe 1

Interface Spezifikation

/**
Invariance:
    assert isEmpty() != isFull()
*/
public interface PrimitiveIntStack {
    /**
    Preconditions:
        assert not isFull()
    
    Postconditions:
        assert not isEmpty()
        assert top() == value
    */
    public void push(int value);

     /**
    Preconditions:
        assert not isEmpty()
    
    Postconditions:
        assert not isFull()
        assert top() == returned value
    */
    public int pop();
    
    /**
    Preconditions:
        assert not isEmpty()
    
    Postconditions:
        throws no IndexOutOfRangeException
    */
    public int top();
    
    /**
    Preconditions:
    assert not isFull()
    
    Postconditions:
    */
    public boolean isEmpty();
    
    /**
    Preconditions:
    assert not isEmpty()
    
    Postconditions:

    */
    public boolean isFull();
}

Welche Regel verletzt dieses Interface? Und wie „schlimm“ ist das?

Das Interface beschreibt nicht, das bei top() eine IndexOutOfRangeException auftreten könnte. Das ist nicht so schlimm, da das sowieso von der Implementation abhängig ist.

Aufgabe 2

/**
Invariance:
    assert size() >= 0
*/
public interface SimpleMap {

    /**
        Preconditions:
            assert value != null
        Postconditions:
            assert size() == 0 then return value == false
            assert return value == true then get(key) != null
    */
    public boolean containsKey(String key);
    
    /**
        Preconditions:
            assert value != null
        Postconditions:
             assert size() == 0 then return value == false
    */
    public boolean containsValue(Object value);
    
    /**
        Preconditions:
            assert containsKey(key)
        Postconditions:
            return value is not null
    */
    public Object get(String key);
    
    /**
        Preconditions:
            key != null
            value != null
        Postconditions:
            old size() == size() - 1
    */
    public void put(String key, Object value) throws KeyOrValueNullException;
    
    /**
        Preconditions:
            size() > 0
        Postconditions:
            old size() == size() + 1
    */

    /**
        Preconditions:
            assert containsKey(key)
        Postconditions:
            old size() == size() + 1
    */
    public void remove(String key);

    /**
        Preconditions:
        Postconditions:
    */
    public int size();
}

Aufgabe 3

Was können Sie damit nicht abdecken? Wie können Sie das Problem lösen? Es ist nicht möglich aus dem Interface den alten Wert herauszuholen. Auch lässt sich nicht prüfen ob eine Exception geworfen wurde.

Können Sie die Stack-Semantik des Stacks mit Contracts vollständig beschreiben? Nein dazu sind immer noch Tests nötig. z.b. das nach bei Stack der mit 5 initialisiert wurde der Stack nach 5x push() erst isFull() ist.