Donnerstag, 9. September 2010

Java meets Design by Contract

Design by Contract ist ein Konzept von Dr. Bertrand Meyer mit dem Hintergrund das Programmieren durch Vertrag zu definieren. In der von Dr. Bertrand Meyer entwickelten Programmiersprache Eiffel ist Design by Contract im Sprachschatz verankert. Dort werden Moduln mit konkreten Verträgen implementiert, die Vorbedingungen, Nachbedingungen und Invarianten einhalten. Bedingungen und Invarianten sind Zusicherungen für die Software-Zuverlässigkeit zur Implementierung robuster Programme, die der zugrunde liegenden Programmspezifikation entsprechen.

Am Methodenbeispiel erkennt man, dass Vorbedingungen vom Aufrufer einer Methode eingehalten werden müssen. Die Nachbedingungen hingegen beinhalten die Zusicherungen, die die aufgerufene Methode einhält. Die Vor- und Nachbedingungen bilden den Vertrag, der von einer Methode eingehalten wird. Sofern der Aufrufer einer Methode die Vorbedingungen erfüllt, ist die Methode verpflichtet die Nachbedingungen und damit den vorgegebenen Vertrag zu erfüllen.

In der Programmiersprache Java werden Assertions zur Prüfung der Korrektheit eines Programms verwendet. Mit einer Assertion prüft man Zusicherungen in einem Programm, um den korrekten Programmablauf zu garantieren. Mit Zusicherungen sollen Programmierfehler, die zur Programmlaufzeit auftreten können, entdeckt werden. Im Falle eines Fehlers, wirft das Java-Laufzeitsystem einen AssertionError.

AssertionErrors sind grundsätzlich nicht abzufangen. Das nicht Abfangen des Fehlers ist unproblematisch. Assertions decken Fehler in der Implementierungs- und Testphase auf. Nur in Ausnahmen dienen Assertions zum Laufzeitdebugging im eingeschränkten Produktionsbetrieb. Die Regel ist allerdings, dass Assertions in Produktion deaktiviert werden. Assertions sind durch ein Argument der Java Virtual Machine aktivierbar bzw. deaktivierbar. Das ist einer der Gründe, weswegen Assertions nicht vollständig die Anforderungen von Design by Contract erfüllen.

Seit Java 1.4 unterstützt Java Assertions, die durch das Schlüsselwort assert ausgedrückt werden. Mit dem Schlüsselwort assert prüft man eine Bedingung auf den boolschen Wert true. Ist die Bedingung nicht erfüllt, wird der AssertionError geworfen.

Beim Gebrauch von Assertions gelten folgende Grundsatzregeln:
  1. Argumente von öffentlichen Methoden nicht mit Assertions prüfen
  2. Kommandozeilenargumente nicht mit Assertions prüfen
  3. Assertions dürfen keine Seiteneffekte hervorrufen
  4. Argumente von privaten Methoden dürfen durch Assertions validiert werden
  5. Assertions sollen für die Prüfung von Bedingungen verwendet werden, die
    man normalerweise nicht erwarten würde
 Assertion-Schlüsselwort:

assert booleanExpression;
assert booleanExpression : errorMessage;

Einfache Stack-Implementierung mit Zusicherungen:

package ccd.jee.dbc;

import java.lang.reflect.Array;

public final class Stack<T> {

    private static final int DEFAULT_CAPACITY = 5;
  
    private int counter;
    private boolean touched;
    private final T[] stack;
    private final int capacity;

    public Stack() {
      
        this(Integer.class, DEFAULT_CAPACITY);
    }
  
    public Stack(Class<?> clazz) {
      
        this(clazz, DEFAULT_CAPACITY);
    }
     
    public Stack(Class<?> clazz, int capacity) {

        this.capacity = capacity;
        stack = (T[]) Array.newInstance(clazz, capacity);
    }
  
    public T pop() {

        popPreCondition();

        T entry = stack[--counter];
        touched = true;

        popInvariant();

        return entry;
    }

    public void push(T element) {

        pushPreCondition();

        int oldCounter = counter;

        pushInvariant();

        stack[counter++] = element;
        touched = true;

        pushPostCondition(element, oldCounter);
    }

    public int getCapacity() {
      
        return capacity;
    }

    private void popPreCondition() {

        assert isNotEmpty() : "stack is empty";
      
        if(isEmpty()) {
          
            throw new IllegalStateException("stack is empty");
        }
    }

    private boolean isEmpty() {
      
        return !isNotEmpty();
    }

    private boolean isNotEmpty() {

        return touched && counter > 0 ? true : false;
    }

    private void popInvariant() {

        assert invariant() : invariantErrorMessage();
    }

    private boolean invariant() {

        return (counter >= 0 && isNotFull());
    }

    private String invariantErrorMessage() {

        return "invariant error occured: count >= 0 && count < capacity";
    }

    private void pushPreCondition() {

        assert isNotFull() : "stack is full";
      
        if(isFull()) {
          
            throw new IllegalStateException("stack is full");
        }
    }

    private boolean isFull() {
      
        return !isNotFull();
    }

    private boolean isNotFull() {

        return counter < capacity;
    }
  
    private void pushInvariant() {

        assert invariant() : invariantErrorMessage();
    }

    private void pushPostCondition(T element, int oldCount) {

        assert counterCondition(element, oldCount) : "counter error occured";
    }

    private boolean counterCondition(T element, int oldCounter) {

        return ((counter == oldCounter + 1) && (stack[counter - 1] == element));
    }
}

Unit-Test der Stack-Implementierung:

package ccd.jee.dbc;

import org.junit.Before;
import org.junit.Test;

public class TestStack {
  
    private Stack<Integer> stack;

    @Before
    public void setUp() {

        stack = new Stack<Integer>();
    }

    @Test
    public void testPushElement() {

        stack.push(1);
    }

    @Test
    public void testPushPopElement() {

        stack.push(1);
        stack.pop();
    }

    @Test
    public void testPushPopMultipleElements() {

        stack.push(1);
        stack.pop();
        stack.push(1);
        stack.push(2);
        stack.pop();
        stack.pop();
        stack.push(1);
        stack.pop();
    }

    @Test
    public void testPushAndPopElements() {

        for (int i = 0; i < stack.getCapacity(); i++) {
           
            stack.push(i);
        }

        for (int i = 0; i < stack.getCapacity(); i++) {
           
            stack.pop();
        }
    }

    @Test(expected=Throwable.class)
    public void testStackWithoutElementsAndPop() {

        stack.pop();
    }

    @Test(expected=Throwable.class)
    public void testStackIsFull() {

        for (int i = 0; i < stack.getCapacity() + 1; i++) {
           
            stack.push(i);
        }
    }

    @Test(expected=Throwable.class)
    public void testStackisEmpty() {

        for (int i = 0; i < stack.getCapacity(); i++) {
           
            stack.push(i);
        }

        for (int i = 0; i < stack.getCapacity() + 1; i++) {
           
            stack.pop();
        }
    }
}

Die Stack-Implementierung verdeutlicht, dass Assertions nur bedingt für Zusicherungen konform des Konzeptes von Design by Contract geeignet sind. Die Vorbedingungen sind zu schwach mit einem assert Statement ausgelegt, sodass zusätzlich noch eine Ausnahme geworfen wird. Der Stack ist eine allgemeine Komponente, sodass es ungünstig wäre, dem Verwender des Stacks bei falscher Anwendung eine ArrayIndexOutOfBoundsException zu präsentieren. An dieser Stelle ist eine stackspezifische Ausnahme besser geeignet. Man bedenke, dass die Assertions in Produktion nicht aktiviert sind. Vor- und Nachbedingungen in Produktion zu prüfen ist der wesentliche Vorteil eines vollwertigen Design by Contract Frameworks.

Bei den Testfällen ist unschön, dass Throwable bei den fehlschlagenden Tests angewandt wird. Der Hintergrund ist, dass einmal eine Ausnahme und einmal ein Fehler das Ergebnis des Testfalls ist. Assertions sind ein gutes Mittel um Zusicherungen zu prüfen. Allerdings sind Assertions kein vollwertiger Ersatz für einen Design by Contract Framework.


Der Rechtshinweis des Java Blog für Clean Code Developer ist bei der Verwendung und Weiterentwicklung des Quellcodes des Blogeintrages zu beachten.