Design by Contract

Dieses Notebook vermittelt fortgeschrittene Techniken zur semantischen Absicherung von Python-Code. Während Typ-Checker die strukturelle Korrektheit prüfen und Unit-Tests einzelne Pfade abdecken, schließen die hier behandelten Paradigmen die Lücke zu mathematisch bewiesener Korrektheit und systematischer Fehlersuche.

Wir haben das im Testing-Kapitel angerissen, allerdings muss sich Design by Contract nicht nur im Testing abspielen, sondern kann auch zur Laufzeit eingesetzt werden (etwa in Bereichen, die nicht performancekritisch, sondern sicherheitskritisch sind).

Einordnung im Testing-Spektrum¶

Property-Based Testing (hypothesis): Generiert stochastisch/probabilistisch eine Vielzahl von Testfällen entlang definierter Invarianten.
Design by Contract (DbC): Verankert diese Invarianten als formale Spezifikation direkt im Code (Vorbedingungen, Nachbedingungen, Invarianten).
Symbolische Ausführung (CrossHair): Nutzt SMT-Solver, um den Code entlang der Verträge analytisch auf Gegenbeispiele zu prüfen (beweist Korrektheit oder findet minimale Edge Cases).
Fuzzing: Durchbricht strukturierte Annahmen und sucht mittels unstrukturierter, mutierter Eingabeströme nach harten Laufzeit- und Speicherfehlern.

# Vorbereitung der Umgebung
!uv venv --quiet
!uv sync --quiet
!uv pip --quiet install icontract deal crosshair-tool z3-solver hypothesis

Design by Contract mit `icontract`¶

Das Paradigma Design by Contract (DbC) versteht die Interaktion zwischen zwei Softwarekomponenten als Vertrag. icontract realisiert dies über Dekoratoren zur Laufzeit.

Die Kern-Dekoratoren und ihre Regeln¶

@icontract.require (Vorbedingung / Precondition): Verpflichtung für den Aufrufer. Muss vor Ausführung der Funktion True ergeben. Verletzt der Aufrufer die Bedingung, wird ein icontract.ViolationError geworfen.
@icontract.ensure (Nachbedingung / Postcondition): Verpflichtung für die Funktion. Muss nach der Ausführung True ergeben. Der Parametername result ist hierbei reserviert und repräsentiert den Rückgabewert der Funktion.
@icontract.invariant (Klassen-Invariante): Wird auf Klassenebene definiert. Garantiert, dass der Zustand des Objekts vor und nach jedem Methodenaufruf integer bleibt.
@icontract.snapshot: Erlaubt es, den Zustand einer Variablen vor der Ausführung einzufrieren, um ihn in der Nachbedingung (@icontract.ensure) mit dem neuen Zustand zu vergleichen.

%%writefile first_contract.py
import icontract
import math

# 1. Alternative: Klassischer Ansatz mit Lambda
@icontract.require(lambda probs: len(probs) > 0, "Verteilung darf nicht leer sein.")
@icontract.require(lambda probs: math.isclose(sum(probs), 1.0, abs_tol=1e-5), "Wahrscheinlichkeiten müssen sich zu 1 summieren.")
@icontract.ensure(lambda result: result >= 0.0, "Die Shannon-Entropie ist immer nicht-negativ.")
def calculate_entropy_icontract(probs: list[float]) -> float:
    return -sum(p * math.log2(p) for p in probs if p > 0) + 0.0

# 2. Alternative: Ohne Lambda mittels regulärer Funktionen (Funktionsreferenz)
def pre_is_normalized(probs: list[float]) -> bool:
    return math.isclose(sum(probs), 1.0, abs_tol=1e-5)

def post_non_negative(result: float) -> bool:
    return result >= 0.0

@icontract.require(pre_is_normalized)
@icontract.ensure(post_non_negative)
def calculate_entropy_no_lambda(probs: list[float]) -> float:
    return -sum(p * math.log2(p) for p in probs if p > 0) + 0.0

# Testlauf (Happy Path)
print("Valid: ", calculate_entropy_icontract([0.25, 0.25, 0.25, 0.25]))

# Testlauf (Vertragsverletzung provozieren)
try:
    calculate_entropy_icontract([0.5, 0.6])  # Summiert sich zu 1.1
except icontract.ViolationError as e:
    print("\nAbgefangen (erwartete Vertragsverletzung):\n", e)

Writing first_contract.py

Die Rolle von `lambda` und Alternativen¶

Warum lambda? Verträge dürfen nicht zur Definitionszeit des Moduls ausgewertet werden, sondern erst zur Laufzeit beim konkreten Funktionsaufruf. Die Lambda-Syntax verzögert diese Ausführung. Zudem nutzt icontract das Modul inspect, um die Argumentnamen der Lambda-Funktion zu parsen. Dadurch kann icontract die Argumente des Originalaufrufs per Dependency Injection exakt in den Vertrag einspeisen. Wenn der Vertrag fehlschlägt, liest icontract den AST (Abstract Syntax Tree) der Lambda-Funktion aus, um im Fehlerprotokoll genau anzuzeigen, welche Variablenwerte zum Fehlschlag führten.

Geht es auch ohne lambda? Ja. Jedes aufrufbare Objekt (Callable) kann übergeben werden, sofern seine Signatur mit den Parametern der Funktion (oder result) übereinstimmt.

Sicherheit ohne `private`/`protected`¶

Klassen-Invarianten in Python sind bei direkter Attributmanipulation (obj.x = -1) wirkungslos. Sie erzwingen Integrität nur bei Nutzung der durch Verträge geschützten Methoden-API. Externe Manipulation ist ein Architekturfehler, kein Kontraktfehler.

!uv run first_contract.py

Valid:  2.0

Abgefangen (erwartete Vertragsverletzung):
 File /home/voelkel/sciebo/hhu/eipy-26/eipy-skript/part-tools/first_contract.py, line 6 in <module>:
Wahrscheinlichkeiten müssen sich zu 1 summieren.: math.isclose(sum(probs), 1.0, abs_tol=1e-5):
math.isclose(sum(probs), 1.0, abs_tol=1e-5) was False
probs was [0.5, 0.6]
sum(probs) was 1.1

Erweitere Verifikation mit `deal`¶

deal ist eine alternative DbC-Bibliothek.

Praxisbeispiel: Refaktorisierte Wirtschaftssimulation¶

Wir implementieren eine Marktlogik. Die Verträge garantieren auf Klassenebene (@deal.inv), dass Kontostände und Bestände niemals negativ sein können, und auf Methodenebene, dass Preise und Mengen strikt positiv sind.

%%writefile art_of_the_deal.py
import deal
from dataclasses import dataclass, field
from enum import Enum, auto

class GameException(Exception): """Basisklasse"""
class NotEnoughMoneyException(GameException): pass
class NotEnoughStockException(GameException): pass

class ProductType(Enum):
    FOOD = auto()
    
    def __str__(self):
        return self.name.title()

# Klassen-Invarianten absichern: Zustand darf niemals illegal werden
@deal.inv(lambda inv: inv.money >= 0.0)
@deal.inv(lambda inv: all(qty >= 0 for qty in getattr(inv, 'stock', {}).values()))
@dataclass
class Inventory:
    money: float
    stock: dict[ProductType, int] = field(default_factory=dict)

    @deal.pre(lambda self, product, quantity, unit_price: quantity != 0)
    @deal.pre(lambda self, product, quantity, unit_price: unit_price > 0.0)
    @deal.raises(NotEnoughMoneyException, NotEnoughStockException)
    def execute_trade(self, product: ProductType, quantity: int, unit_price: float) -> None:
        cost = quantity * unit_price

        if quantity > 0 and self.money < cost:
            raise NotEnoughMoneyException(f"Benötige {cost:.2f}€, habe {self.money:.2f}€")
        elif quantity < 0 and self.stock.get(product, 0) < abs(quantity):
            raise NotEnoughStockException("Nicht genügend Lagerbestand zum Verkauf.")

        self.money -= cost
        self.stock[product] = self.stock.get(product, 0) + quantity

@deal.inv(lambda m: getattr(m, 'current_price', 1.0) >= 1.0)
@dataclass
class Market:
    product: ProductType
    current_price: float
    volatility: float

    @deal.pre(lambda self, direction: direction in (1, -1))
    def adjust_price(self, direction: int) -> None:
        change = direction * self.volatility
        self.current_price = max(1.0, round(self.current_price + change, 2))

# Demonstration der Funktionsfähigkeit
inv = Inventory(money=50.0, stock={ProductType.FOOD: 2})
market = Market(product=ProductType.FOOD, current_price=10.0, volatility=0.5)

# Gültiger Kauf
inv.execute_trade(ProductType.FOOD, 2, market.current_price)
print("Zustand nach Kauf:", inv)

# Provozieren einer Invarianten-Verletzung durch direkte Manipulation
try:
    inv.money = -10.0
except deal.InvContractError as e:
    print("\nAbgefangen via deal (Invarianten-Verletzung):", e)

Writing art_of_the_deal.py

!uv run art_of_the_deal.py

Zustand nach Kauf: InventoryInvarianted(money=30.0, stock={<ProductType.FOOD: 1>: 4})

Abgefangen via deal (Invarianten-Verletzung): expected inv.money >= 0.0

Domain Exceptions vs. Contract Violations¶

Ein kritischer Punkt beim Entwurf von Verträgen ist die Abgrenzung zwischen Fachlogik-Ausnahmen (Domain Exceptions) und Vertragsverletzungen (Contract Violations). Schauen wir uns dazu noch einmal die Methode execute_trade aus dem obigen deal-Beispiel an:

Contract Violation (@deal.pre): Wenn ein Aufrufer quantity=0 oder unit_price=-5.0 übergibt, bricht er die Vorbedingung. Dies ist kein regulärer Laufzeitfehler, sondern ein Programmierfehler (Bug) im aufrufenden Code. Das Programm sollte hier hart abstürzen (Fail-Fast), da die internen Annahmen der Methode verletzt wurden.
Domain Exception (raise NotEnoughMoneyException): Wenn der Aufrufer valide Argumente übergibt (z. B. quantity=10, unit_price=5.0), das Inventar aber nur 20€ Guthaben aufweist, sind die Kontrakte formell erfüllt. Der Zustand des Systems verhindert jedoch die Ausführung. Dies ist ein erwartbarer fachlicher Zustand, der über klassische Kontrollstrukturen (if/raise) behandelt und vom Gesamtsystem abgefangen werden muss.

Architektur-Regel: Verträge prüfen die Gültigkeit der Systemzustände und Parameterstrukturen. Sie ersetzen niemals die normale Business-Logik für die Behandlung von fachlichen Ausnahmesituationen.

Architektur-Frage: Kann man `deal` und `icontract` mischen?¶

Nein, das ist ein Anti-Pattern. Beide Bibliotheken arbeiten primär über Funktions-Wrapper und Modifikationen zur Laufzeit. Ein paralleler Einsatz führt zu:

Redundanz & Performance-Verlust: Doppeltes Wrapping verlangsamt Funktionsaufrufe linear.
Unvorhersehbarem Verhalten: Die Reihenfolge, in der Dekoratoren ausgewertet werden (von unten nach oben), kann dazu führen, dass Invarianten einer Bibliothek Preconditions der anderen Bibliothek blockieren.
Werkzeug-Inkompatibilität: Statische Verifizierer wie CrossHair sind darauf optimiert, die Kontrakte einer bekannten Bibliothek zu parsen. Das Mischen bricht die symbolische Analyse.

Integration von Property-Based und Concolic Testing¶

DbC entfaltet seine maximale Stärke, wenn die Verträge automatisiert auf Inkorrektheiten geprüft werden. Das Wort ‘Concolic’ ist ein Portemanteau (ein Kofferwort) aus ‘Concrete’ und ‘Symbolic’.

Zusammenspiel der Werkzeuge¶

Hypothesis: Generiert Werte deterministisch-zufällig (Fuzzing-artig auf Type-Ebene) und versucht, Verträge zu brechen. Findet es einen Fehler, schrumpft es die Eingabe auf das minimale Gegenbeispiel (Shrinking).
CrossHair: Arbeitet analytisch. Es führt den Code nicht nur stochastisch aus, sondern analysiert den Kontrollfluss symbolisch. Es übersetzt den Python-Bytecode in mathematische Gleichungen und übergibt diese an den SMT-Solver Z3. CrossHair sucht gezielt nach mathematischen Pfaden, die den Vertrag brechen.

Kombination von DbC mit Hypothesis & CrossHair¶

Sowohl deal als auch icontract integrieren sich in dieses Ökosystem:

deal test: Ein CLI-Befehl (deal test mein_modul.py), der automatisch Hypothesis unter der Haube startet. Er nutzt die @deal.pre-Bedingungen, um den Suchraum für Argumente einzuschränken.
icontract-hypothesis: Erlaubt es, aus icontract-Spezifikationen automatisch Hypothesis-Strategien zu generieren.
CrossHair als Hypothesis-Backend: Hypothesis erlaubt es, CrossHair direkt als analytisches Backend einzubinden. Dadurch wird die stochastische Generierung durch geführte symbolische Pfadsuche ersetzt.

%%writefile deal_hypothesis.py
from hypothesis import given, settings, strategies as st
import deal

# Spezifikation einer mathematischen Invariante via deal
@deal.pre(lambda x, y: x > 0 and y > 0)
@deal.ensure(lambda x, y, result: result > x and result > y)
def add_positive_integers(x: int, y: int) -> int:
    return x + y

# Hypothesis nutzt den Vertrag implizit oder explizit zur Verifikation
@given(x=st.integers(), y=st.integers())
def test_with_hypothesis(x, y):
    # Wir filtern Eingaben, die die Vorbedingung nicht erfüllen
    if x > 0 and y > 0:
        assert add_positive_integers(x, y) == x + y

test_with_hypothesis()

Writing deal_hypothesis.py

!uv run deal_hypothesis.py

CrossHair via CLI ausführen¶

Um ein Skript formal via CrossHair zu prüfen, nutzt man die Shell. CrossHair liest sowohl deal- als auch icontract-Dekoratoren:

crosshair check mein_skript.py

Findet CrossHair eine Kombination von Inputs, die die Preconditions erfüllen, aber die Postcondition verletzen, gibt es den exakten Wert aus.

Man kann Contracts auch als kostspieliege Testing-Geschichte verstehen, und in Produktivumgebungen darauf verzichten. Das -O Flag bedeutet: ignoriere Assertions und deaktiviere DbC zur Laufzeit:

uv run python -O mein_skript.py

SMT-Solver und Formale Verifikation im Detail¶

Zeitleiste der formalen Verifikation im Python-Kontext¶

Phase 1 (Typisierung - Pre-2015): Python gilt als rein dynamisch. Fehler werden erst zur Laufzeit bemerkt.
Phase 2 (Statisches Linting & Typ-Annotationen - PEP 484): Einführung von mypy. Überprüfung der strukturellen Korrektheit (Typen), jedoch ohne semantische Validierung (Logik).
Phase 3 (Laufzeit-Verträge): Bibliotheken wie icontract erlauben logische Prüfungen zur Laufzeit. Fehler werden deterministisch beim Eintritt abgefangen.
Phase 4 (Concolic Testing / Symbolische Ausführung): Werkzeuge wie CrossHair docken an Laufzeit-Verträge an und übersetzen sie mittels SMT-Solvern in mathematische Beweise.
Phase 5 (Full Static Verification): Werkzeuge wie Nagini verifizieren Python-Code vollständig statisch zur Compile-Zeit ohne Code-Ausführung.

Z3Py: Der Theorem Prover von Microsoft¶

CrossHair arbeitet intern mit Z3. Wir können Z3Py direkt nutzen, um komplexe logische Bedingungen oder Spielregeln zu validieren, ohne Algorithmen zu implementieren. Der Solver findet die mathematische Lösung (oder beweist, dass keine existiert).

%%writefile z3_example.py
from z3 import Int, Solver, sat, unsat

# Problemstellung: Bestimme den optimalen Clearing-Preis in einer Wirtschaftssimulation

preis = Int('preis')
nachfrage = Int('nachfrage')
angebot = Int('angebot')

solver = Solver()

# Constraints:
solver.add(preis >= 10, preis <= 40) # 1. Der Preis muss zwischen 10 und 50 Euro liegen.
solver.add(nachfrage == 100 - 2 * preis) # 2. Die Nachfrage-Gleichung lautet: nachfrage == 100 - 2 * preis
solver.add(angebot == 10 + preis) # 3. Das Angebot lautet: angebot == 10 + preis
solver.add(angebot == nachfrage)  # Marktgleichgewicht, suche diesen Gleichgewichtspreis

if solver.check() == sat:
    model = solver.model()
    print(f"Mathematisch bewiesener Gleichgewichtspreis: {model[preis]} €")
    print(f"Menge: {model[angebot]} Einheiten")
else:
    print("Kein stabiles Marktgleichgewicht unter diesen Bedingungen möglich.")

Writing z3_example.py

!uv run z3_example.py

Mathematisch bewiesener Gleichgewichtspreis: 30 €
Menge: 40 Einheiten

Exkurs: SMT-Solver vs. Interaktive Theorembeweiser¶

Wenn wir von “Formaler Verifikation” sprechen, müssen wir konzeptionell zwischen zwei grundlegend verschiedenen Werkzeugklassen unterscheiden:

SMT-Solver (wie Z3): Dies sind automatisierte “Push-Button”-Lösungen. Wir übersetzen unseren Python-Code in ein Gleichungssystem, drücken auf Start, und der Solver liefert vollautomatisiert eine Antwort (sat oder unsat). Sie sind exzellent darin, konkrete Randfälle in logischen Kontrollflüssen (z. B. Integer-Arithmetik, Array-Zugriffe oder Bitvektoren) zu finden.
Interaktive Theorembeweiser (ITP) (wie Lean 4, Coq oder Isabelle): Hierbei handelt es sich eher um mathematische Programmiersprachen. Wenn die Beweisführung komplexe Induktion oder abstrakte Algebra erfordert, scheitern vollautomatisierte SMT-Solver (der Zustandsraum explodiert). In Lean 4 schreibt der Entwickler/Mathematiker den mathematischen Beweis Schritt für Schritt selbst. Der Compiler verifiziert lediglich, ob die logischen Schlüsse und Transformationen formal valide sind.

Werkzeuge wie CrossHair nutzen mit Z3 absichtlich einen SMT-Solver, da Softwareentwickler im Alltag pragmatisch Bugs und Edge-Cases finden wollen, ohne begleitend ein Mathematikstudium in abstrakter Beweisführung absolvieren zu müssen.

Nagini¶

Nagini ist ein statischer Verifizierer für typisiertes Python, basierend auf dem Viper-Verifikations-Infrastrukturprojekt (was wiederum auch auf den Z3 SMT Solver setzt).

Unterschied zu CrossHair: CrossHair führt den Code partiell aus (concolic). Nagini führt den Code niemals aus. Es liest Typ-Annotationen und Verträge, die als spezifische Python-Kommentare oder Funktionsaufrufe hinterlegt sind, und übersetzt das gesamte Programm in ein mathematisches Zwischenformat.

Typischer Einsatzzweck:

Verifikation von Nebenläufigkeit (Beweis der Abwesenheit von Deadlocks / Race Conditions).
Kryptographische Protokolle, bei denen Speicher- und Logikfehler fatale Sicherheitslücken bedeuten.

Exemplarischer Nagini-Codeblock (Syntax-Prinzip):

from nagini.contracts import *

def cast_vote(voter_id: int, state: list[int]) -> None:
    # Nagini-Kontrakte werden statisch analysiert
    Requires(voter_id >= 0 and Acc(state)) 
    Ensures(len(state) > Old(len(state)))
    
    state.append(voter_id)

Acc steht für Accessibility Predicate. Es weist formal nach, dass die Funktion die Berechtigung besitzt, auf den Speicherbereich der Referenz state zuzugreifen und ihn zu mutieren. Das ist in der formalen Verifikation notwendig, um Speicherzugriffsfehler, Aliasing-Konflikte oder Data Races in nebenläufigen Systemen auszuschließen.

Fuzzing¶

Fuzzing bildet das destruktive Gegenstück zur formalen Verifikation.

Prinzipien und Ziele des Fuzzings¶

Während DbC und SMT-Solver innerhalb des definierten logischen Weltmodells operieren, bricht Fuzzing gezielt aus diesem aus. Ein Fuzzer generiert keine validen Typen, sondern mutiert Eingabedatenströme auf Byte-Ebene (oft vollkommen unstrukturiert).

Hauptziel: Das Provokation von unkontrollierten Zuständen wie:

Dangling Pointers / Buffer Overflows (insb. in Python-C-Extensions wie numpy, cryptography oder llama-cpp-python).
Unendliche Schleifen und Out-of-Memory-Zustände im Interpreter.

Die Bibel des Fuzzings¶

Das Standardwerk für diese Methodik ist “The Fuzzing Book” (fuzzingbook.org) von Andreas Zeller et al. Es beschreibt fundamental, wie Coverage-guided Fuzzing funktioniert: Der Fuzzer misst via Instrumentierung, welche Codezeilen eine Eingabe ausführt. Erhöht eine Mutation die Codeabdeckung (Coverage), wird sie als Basis für weitere Mutationen herangezogen.

Wann nutzt man Fuzzing, wann DbC?¶

DbC + Symbolische Ausführung: Zur Absicherung der inneren Fachlogik, mathematischer Algorithmen und Zustandsübergänge.
Fuzzing: Zur Absicherung der Systemgrenzen – Parser, Netzwerkschnittstellen, Datei-Importer. Überall dort, wo unvalidierte Rohdaten verarbeitet werden.

Fuzzing in der Praxis: Coverage-Guided Fuzzing mit Atheris¶

Um die im Standardwerk “The Fuzzing Book” beschriebenen theoretischen Konzepte des Coverage-Guided Fuzzing produktiv in Python zu nutzen, kann man Atheris einsetzen (ein von Google entwickeltes Open-Source-Framework).

Atheris nutzt die LLVM-Infrastruktur (via libFuzzer) und instrumentiert den Python-Bytecode zur Laufzeit. Dadurch ``sieht’’ der Fuzzer, welche Pfade und Bedingungen (z. B. if-Anweisungen) durch eine Byte-Mutation im Input ausgelöst wurden, und optimiert den Datenstrom gezielt, um tiefer im Programmablauf voranzukommen.

%%writefile atheris_fuzz.py
import atheris
import sys

# Das zu testende Ziel (Target)
def test_target(data):
    if len(data) >= 3:
        # Ein Fuzzer sucht nach harten Interpreter-Abstürzen oder Memory-Leaks
        if data[0] == 0xFF and data[1] == 0x00 and data[2] == 0xAA:
            raise RuntimeError("Versteckter Edge-Case getriggert!")

# Initialisierung und Start des Fuzzers
atheris.instrument_all()  # Instrumentiert alle importierten Module
atheris.Setup(sys.argv, test_target)
atheris.Fuzz()

Writing atheris_fuzz.py

!uv run python atheris_fuzz.py

INFO: Instrumenting functions: [2898/2898] 100%
INFO: Using built-in libfuzzer
WARNING: Failed to find function "__sanitizer_acquire_crash_state".
WARNING: Failed to find function "__sanitizer_print_stack_trace".
WARNING: Failed to find function "__sanitizer_set_death_callback".
INFO: Running with entropic power schedule (0xFF, 100).
INFO: Seed: 3600305800
INFO: -max_len is not provided; libFuzzer will not generate inputs larger than 4096 bytes
INFO: A corpus is not provided, starting from an empty corpus
#2	INITED cov: 2 ft: 2 corp: 1/1b exec/s: 0 rss: 52Mb
#7	NEW    cov: 4 ft: 4 corp: 2/4b lim: 4 exec/s: 0 rss: 52Mb L: 3/3 MS: 5 ChangeByte-ChangeBit-ShuffleBytes-ChangeBit-CMP- DE: "\001\000"-
#69	NEW    cov: 7 ft: 7 corp: 3/7b lim: 4 exec/s: 0 rss: 52Mb L: 3/3 MS: 2 ShuffleBytes-ChangeByte-
#75	NEW    cov: 8 ft: 8 corp: 4/10b lim: 4 exec/s: 0 rss: 52Mb L: 3/3 MS: 1 ChangeByte-

 === Uncaught Python exception: ===
RuntimeError: Versteckter Edge-Case getriggert!
Traceback (most recent call last):
  File "/home/voelkel/sciebo/hhu/eipy-26/eipy-skript/part-tools/atheris_fuzz.py", line 9, in test_target
    raise RuntimeError("Versteckter Edge-Case getriggert!")
RuntimeError: Versteckter Edge-Case getriggert!

Exception ignored in: <function _removeHandlerRef at 0x7fb543460400>
Traceback (most recent call last):
  File "/home/voelkel/.local/share/uv/python/cpython-3.13.2-linux-x86_64-gnu/lib/python3.13/logging/__init__.py", line 890, in _removeHandlerRef
TypeError: 'NoneType' object is not callable
==176749== ERROR: libFuzzer: fuzz target exited
SUMMARY: libFuzzer: fuzz target exited
MS: 3 PersAutoDict-ShuffleBytes-CMP- DE: "\001\000"-"\252\000\000\000\000\000\000\000"-; base unit: 64f78a863c7ffca9967660a5c354380f485a12b4
0xff,0x0,0xaa,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x1,0x0,0xbf,
\377\000\252\000\000\000\000\000\000\000\001\000\277
artifact_prefix='./'; Test unit written to ./crash-772218a87a893f1b4a5852b8f6a9dec99135b5a6
Base64: /wCqAAAAAAAAAAEAvw==

Abgrenzung Design by Contract von Datenvalidierung¶

Mit Pydantic lassen sich Daten zur Laufzeit validieren, und dabei auch Verträge wie money >= 0 prüfen. Volles ``Design by Contract’’ ist aber mehr, da nicht nur bei Daten eine Validierung durchgeführt wird, gewissermaßen statisch, sondern eben auch Pre- und Postconditions für Methoden, sodass die Semantik von Transformationen geprüft werden kann. Diese Grenzen verwischen teilweise, wenn man sehr stark auf Representational State Transfer (ReST) als Design Pattern setzt, etwa wenn man mit FastAPI oder FastUI arbeitet, um Schnittstellen direkt mit Pydantic zu beschreiben.

DbC ersetzt keine Eingangsvalidierung. Pydantic sichert die Systemgrenze gegen invalide Rohdaten und konvertiert Daten in Python-Datenstrukturen; DbC sichert die interne Integrität bei Zustandsübergängen.

!rm -f art_of_the_deal.py deal_hypothesis.py first_contract.py z3_example.py atheris_fuzz.py crash-*

zsh:1: no matches found: crash-*