Zusammenfassung

Diese Einreichung beschreibt die Programmierung nach Vertrag für Python. Eiffel’s Design By Contract(tm) ist vielleicht die bekannteste Anwendung von Programmierverträgen [2].

Programmierverträge erweitern die Sprache um Invariante Ausdrücke für Klassen und Module sowie Prä- und Postkonditionsausdrücke für Funktionen und Methoden.

Diese Ausdrücke (Verträge) ähneln Assertions: Sie müssen wahr sein, andernfalls wird das Programm gestoppt, und die Laufzeitprüfung der Verträge ist typischerweise nur im Debugging-Modus aktiviert. Verträge sind auf einer höheren Ebene als einfache Assertions und sind üblicherweise in der Dokumentation enthalten.

Motivation

Python hat bereits Assertions, warum also zusätzliche Dinge in die Sprache aufnehmen, um so etwas wie Verträge zu unterstützen? Die beiden besten Gründe sind 1) eine bessere, genauere Dokumentation und 2) einfacheres Testen.

Komplexe Module und Klassen scheinen nie ganz richtig dokumentiert zu sein. Die bereitgestellte Dokumentation mag ausreichen, um einen Programmierer davon zu überzeugen, ein bestimmtes Modul oder eine Klasse einem anderen vorzuziehen, aber der Programmierer muss fast immer den Quellcode lesen, wenn die eigentliche Fehlersuche beginnt.

Verträge erweitern das ausgezeichnete Beispiel des doctest-Moduls [4]. Die Dokumentation ist für Programmierer lesbar und enthält dennoch ausführbare Tests.

Das Testen von Code mit Verträgen ist ebenfalls einfacher. Umfassende Verträge sind gleichwertig mit Unit-Tests [8]. Tests überprüfen den gesamten Bereich der Präkonditionen und schlagen fehl, wenn die Postkonditionen ausgelöst werden. Theoretisch kann eine korrekt spezifizierte Funktion vollständig zufällig getestet werden.

Warum also dies in die Sprache aufnehmen? Warum nicht mehrere verschiedene Implementierungen haben oder Programmierern erlauben, ihre eigenen Assertions zu implementieren? Die Antwort liegt im Verhalten von Verträgen unter Vererbung.

Angenommen, Alice und Bob verwenden verschiedene Assertion-Pakete. Wenn Alice eine Klassenbibliothek erstellt, die durch Assertions geschützt ist, kann Bob keine Klassen von Alices Bibliothek ableiten und ordnungsgemäße Überprüfungen von Postkonditionen und Invarianten erwarten. Wenn beide das gleiche Assertion-Paket verwenden, kann Bob Alices Methoden überschreiben und dennoch gegen Alices Vertragsassertionen testen. Der natürliche Ort, um dieses Assertion-System zu finden, ist in der Laufzeitbibliothek der Sprache.

Spezifikation

Der Docstring eines beliebigen Moduls oder einer Klasse kann invariante Verträge enthalten, die mit einer Zeile gekennzeichnet sind, die mit dem Schlüsselwort inv gefolgt von einem Doppelpunkt (:) beginnt. Leerzeichen am Anfang der Zeile und um den Doppelpunkt herum werden ignoriert. Der Doppelpunkt wird entweder sofort von einem einzelnen Ausdruck in derselben Zeile gefolgt oder von einer Reihe von Ausdrücken in folgenden Zeilen, die über das Schlüsselwort inv eingerückt sind. Hierbei gelten die normalen Python-Regeln für implizite und explizite Zeilenfortsetzungen. Eine beliebige Anzahl von invarianten Verträgen kann in einem Docstring enthalten sein.

Einige Beispiele

# state enumeration
START, CONNECTING, CONNECTED, CLOSING, CLOSED = range(5)

class conn:

    """A network connection

    inv: self.state in [START, CLOSED,       # closed states
                        CONNECTING, CLOSING, # transition states
                        CONNECTED]

    inv: 0 <= self.seqno < 256
    """

class circbuf:

    """A circular buffer.

    inv:
        # there can be from 0 to max items on the buffer
        0 <= self.len <= len(self.buf)

        # g is a valid index into buf
        0 <= self.g < len(self.buf)

        # p is also a valid index into buf
        0 <= self.p < len(self.buf)

        # there are len items between get and put
        (self.p - self.g) % len(self.buf) == \
              self.len % len(self.buf)
    """

Modulinvarianten müssen nach dem Laden des Moduls und beim Eintritt und Austritt aus jeder öffentlichen Funktion innerhalb des Moduls wahr sein.

Klasseninvarianten müssen nach Rückgabe der __init__-Funktion, beim Eintritt in die __del__-Funktion und beim Eintritt und Austritt aus jeder anderen öffentlichen Methode der Klasse wahr sein. Klasseninvarianten müssen die Variable self verwenden, um auf Instanzvariablen zuzugreifen.

Eine Methode oder Funktion ist öffentlich, wenn ihr Name nicht mit einem Unterstrich (_) beginnt, es sei denn, sie beginnt und endet mit zwei Unterstrichen (__).

Der Docstring einer Funktion oder Methode kann Präkonditionen enthalten, die mit dem Schlüsselwort pre gemäß den oben genannten Regeln dokumentiert sind. Postkonditionen werden mit dem Schlüsselwort post dokumentiert, optional gefolgt von einer Liste von Variablen. Die Variablen befinden sich im selben Geltungsbereich wie der Körper der Funktion oder Methode. Diese Liste deklariert die Variablen, die die Funktion/Methode ändern darf.

Ein Beispiel

class circbuf:

    def __init__(self, leng):
        """Construct an empty circular buffer.

        pre: leng > 0
        post[self]:
            self.is_empty()
            len(self.buf) == leng
        """

Ein Doppelpunkt (::) kann anstelle eines einfachen Doppelpunkts (:) verwendet werden, um Docstrings zu unterstützen, die mit reStructuredText geschrieben wurden [7]. Zum Beispiel beschreiben die folgenden beiden Docstrings denselben Vertrag.

"""pre: leng > 0"""
"""pre:: leng > 0"""

Ausdrücke in Prä- und Postkonditionen werden im Modul-Namespace definiert – sie haben Zugriff auf fast alle Variablen, auf die die Funktion zugreifen kann, mit Ausnahme von Closure-Variablen.

Die Vertrag-Ausdrücke in Postkonditionen haben Zugriff auf zwei zusätzliche Variablen: __old__, die mit flachen Kopien der Werte gefüllt wird, die in der Variablenliste nach dem Schlüsselwort post deklariert sind, und __return__, die an den Rückgabewert der Funktion oder Methode gebunden ist.

Ein Beispiel

class circbuf:

    def get(self):
        """Pull an entry from a non-empty circular buffer.

        pre: not self.is_empty()
        post[self.g, self.len]:
            __return__ == self.buf[__old__.self.g]
            self.len == __old__.self.len - 1
        """

Alle Vertrag-Ausdrücke haben Zugriff auf einige zusätzliche Hilfsfunktionen. Um die Wahrheitsprüfung von Sequenzen zu erleichtern, werden zwei Funktionen forall und exists definiert als

def forall(a, fn = bool):
    """Return True only if all elements in a are true.

    >>> forall([])
    1
    >>> even = lambda x: x % 2 == 0
    >>> forall([2, 4, 6, 8], even)
    1
    >>> forall('this is a test'.split(), lambda x: len(x) == 4)
    0
    """

def exists(a, fn = bool):
    """Returns True if there is at least one true value in a.

    >>> exists([])
    0
    >>> exists('this is a test'.split(), lambda x: len(x) == 4)
    1
    """

Ein Beispiel

def sort(a):
    """Sort a list.

    pre: isinstance(a, type(list))
    post[a]:
        # array size is unchanged
        len(a) == len(__old__.a)

        # array is ordered
        forall([a[i] >= a[i-1] for i in range(1, len(a))])

        # all the old elements are still in the array
        forall(__old__.a, lambda e: __old__.a.count(e) == a.count(e))
    """

Um die Auswertung von Bedingungen zu erleichtern, ist die Funktion implies definiert. Mit zwei Argumenten ähnelt dies dem logischen Implizierungsoperator (=>). Mit drei Argumenten ähnelt dies dem bedingten Ausdruck von C (x?a:b). Dies ist definiert als

implies(False, a) => True
implies(True, a) => a
implies(False, a, b) => b
implies(True, a, b) => a

Beim Eintritt in eine Funktion werden die Präkonditionen der Funktion überprüft. Eine Assertion-Fehler-Ausnahme wird ausgelöst, wenn eine Präkondition falsch ist. Wenn die Funktion öffentlich ist, werden auch die Invarianten der Klasse oder des Moduls überprüft. Kopien der in der Post-Kondition deklarierten Variablen werden gespeichert, die Funktion wird aufgerufen und wenn die Funktion ohne Auslösung einer Ausnahme beendet wird, werden die Postkonditionen überprüft.

AssertionError
    ContractViolationError
        PreconditionViolationError
        PostconditionViolationError
        InvariantViolationError
        InvalidPreconditionError

try:
    some_func()
except contract.PreconditionViolationError:
    # failed pre-condition, ok
    pass

class SimpleMailClient:

    def send(self, msg, dest):
        """Sends a message to a destination:

        pre: self.is_open() # we must have an open connection
        """

    def recv(self):
        """Gets the next unread mail message.

        Returns None if no message is available.

        pre: self.is_open() # we must have an open connection
        post: __return__ is None or isinstance(__return__, Message)
        """

 class ComplexMailClient(SimpleMailClient):
    def send(self, msg, dest):
        """Sends a message to a destination.

        The message is sent immediately if currently connected.
        Otherwise, the message is queued locally until a
        connection is made.

        pre: True # weakens the pre-condition from SimpleMailClient
        """

    def recv(self):
        """Gets the next unread mail message.

        Waits until a message is available.

        pre: True # can always be called
        post: isinstance(__return__, Message)
        """

Begründung

Abgesehen von den folgenden Unterschieden spiegelt die Programmierung nach Vertrag für Python die Eiffel DBC-Spezifikation wider [3].

Das Einbetten von Verträgen in Docstrings ist dem doctest-Modul nachempfunden. Es entfällt die Notwendigkeit zusätzlicher Syntax, stellt sicher, dass Programme mit Verträgen abwärtskompatibel sind, und es ist keine weitere Arbeit erforderlich, um die Verträge in die Dokumentation aufzunehmen.

Die Schlüsselwörter pre, post und inv wurden anstelle der Eiffel-inspirierten Schlüsselwörter REQUIRE, ENSURE und INVARIANT gewählt, da sie kürzer sind, besser zur mathematischen Notation passen, und aus einem subtileren Grund: das Wort „require“ impliziert Verantwortung des Aufrufers, während „ensure“ Garantien des Anbieters impliziert. Dennoch können Präkonditionen bei Verwendung von Mehrfachvererbung ohne Verschulden des Aufrufers fehlschlagen, und Postkonditionen können bei Verwendung von Mehrfach-Threads ohne Verschulden der Funktion fehlschlagen.

Schleifeninvarianten wie in Eiffel werden nicht unterstützt. Sie sind schwierig zu implementieren und ohnehin kein Teil der Dokumentation.

Die Variablennamen __old__ und __return__ wurden gewählt, um Konflikte mit dem Schlüsselwort return zu vermeiden und die Konsistenz mit den Python-Namenskonventionen zu wahren: Sie sind öffentlich und werden von der Python-Implementierung bereitgestellt.

Das Deklarieren von Variablen nach einem post-Schlüsselwort beschreibt genau, was die Funktion oder Methode ändern darf. Dies macht die NoChange-Syntax in Eiffel überflüssig und erleichtert die Implementierung von __old__ erheblich. Es passt auch besser zu Z-Schemata [9], die in zwei Teile unterteilt sind: Deklaration dessen, was sich ändert, gefolgt von Einschränkung der Änderungen.

Flache Kopien von Variablen für den Wert von __old__ verhindern, dass eine Implementierung von Vertrags-Programmierung ein System zu sehr verlangsamt. Wenn eine Funktion Werte ändert, die von einer flachen Kopie nicht erfasst würden, kann sie die Änderungen wie folgt deklarieren:

post[self, self.obj, self.obj.p]

Die Funktionen forall, exists und implies wurden hinzugefügt, nachdem einige Zeit damit verbracht wurde, bestehende Funktionen mit Verträgen zu dokumentieren. Diese erfassen die Mehrheit gängiger Spezifikationsidiome. Es mag den Anschein haben, dass die Definition von implies als Funktion nicht funktioniert (die Argumente werden ausgewertet, ob sie benötigt werden oder nicht, im Gegensatz zu anderen booleschen Operatoren), aber es funktioniert für Verträge, da kein Nebeneffekt für irgendeinen Ausdruck in einem Vertrag auftreten sollte.

Referenzimplementierung

Eine Referenzimplementierung ist verfügbar [1]. Sie ersetzt bestehende Funktionen durch neue Funktionen, die Vertragsprüfungen durchführen, indem sie direkt den Namespace der Klasse oder des Moduls ändert.

Andere Implementierungen existieren, die entweder __getattr__ [5] hacken oder __metaclass__ [6] verwenden.

Referenzen

Urheberrecht

Dieses Dokument wurde gemeinfrei erklärt.