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).
Worum es geht. Zusagen über Code so aufschreiben, dass Maschinen sie prüfen können: Vorbedingungen, Nachbedingungen, Invarianten. Und was daraus wird, sobald Werkzeuge sie systematisch angreifen — Property-Based Testing, symbolische Ausführung, Fuzzing.
Was Sie danach können. Verträge mit icontract und deal schreiben; eine Vertragsverletzung von einem Domänenfehler unterscheiden und daraus ableiten, welchen der beiden man abfangen darf; crosshair auf Verträge ansetzen und sein Ergebnis richtig lesen; und einordnen, welche der vier Techniken welche Frage beantwortet.
Die Java-Entsprechung in einem Satz. Am nächsten kommt JML oder eine Kaskade von assert-Zeilen am Methodenanfang — der Unterschied ist, dass der Vertrag hier maschinenlesbar am Code hängt und externe Werkzeuge ihn als Spezifikation benutzen, statt ihn nur zur Laufzeit zu prüfen.
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.
Verträge und Tests beantworten verschiedene Fragen: Ein Test prüft einen Fall, ein Vertrag prüft jeden Aufruf — dafür sagt er nichts darüber, ob die Funktion das Richtige tut. Am stärksten sind beide zusammen: Sobald Vorbedingungen aufgeschrieben sind, kann Property-Based Testing gültige Eingaben erzeugen, und ein Solver wie CrossHair sucht nach Eingaben, die die Nachbedingung verletzen.
# Vorbereitung der Umgebung
!uv venv --quiet
!uv sync --quiet
!uv pip --quiet install icontract deal crosshair-tool z3-solver hypothesisDesign 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 FunktionTrueergeben. Verletzt der Aufrufer die Bedingung, wird einicontract.ViolationErrorgeworfen.@icontract.ensure(Nachbedingung / Postcondition): Verpflichtung für die Funktion. Muss nach der AusführungTrueergeben. Der Parameternameresultist 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.pyValid: 2.0
Abgefangen (erwartete Vertragsverletzung):
File /home/user/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.pyZustand 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 Aufruferquantity=0oderunit_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
CrossHairsind 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 automatischHypothesisunter der Haube startet. Er nutzt die@deal.pre-Bedingungen, um den Suchraum für Argumente einzuschränken.icontract-hypothesis: Erlaubt es, ausicontract-Spezifikationen automatisch Hypothesis-Strategien zu generieren.CrossHair als Hypothesis-Backend:
Hypothesiserlaubt 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.pydeal test: Verträge als Testgenerator¶
Bis hierher haben die Verträge nur geprüft, was das Programm ohnehin tut. deal kann sie auch umgekehrt benutzen: aus den Vorbedingungen Eingaben erzeugen und schauen, ob eine davon die Nachbedingung bricht. Das ist Property-Based Testing, bei dem die Properties schon im Code stehen.
Zwei Voraussetzungen gelten dafür:
Die Funktion muss
@deal.puretragen.deal testprüft ausschließlich reine Funktionen — bei einer Methode, die Zustand ändert, wüsste es nicht, gegen welchen Ausgangszustand es testen soll. Die Klassen aus dem Abschnitt oben fallen damit heraus.Die Parameter brauchen Type Hints, denn daraus leitet
dealab, welche Werte es überhaupt einsetzen darf.
Eine Funktion mit einer absichtlich zu optimistischen Nachbedingung — bei negativem Preis oder Rabatt über 100 wäre das Ergebnis negativ, und die Vorbedingung schließt nur den Rabatt ein, nicht den Preis:
%%writefile dealdemo.py
import deal
@deal.pure
@deal.pre(lambda preis, rabatt: 0 <= rabatt <= 100)
@deal.post(lambda result: result >= 0.0)
def endpreis(preis: float, rabatt: float) -> float:
"""Zieht einen Prozent-Rabatt ab. Die Nachbedingung ist zu optimistisch."""
return preis - preis * rabatt / 100Writing dealdemo.py
# sed filtert Farbcodes und die langen Pfade aus der Ausgabe.
!uv run python -m deal test dealdemo.py 2>&1 \
| sed -e 's/\x1b\[[0-9;]*m//g' -e 's|/[^ "]*/site-packages/|.../|g'running dealdemo.py
running endpreis
endpreis(preis=0.0, rabatt=0.0)
Traceback (most recent call last):
File ".../deal/_cli/_test.py", line 111, in run_cases
case()
~~~~^^
File ".../deal/_testing.py", line 55, in __call__
self._check_result(result)
~~~~~~~~~~~~~~~~~~^^^^^^^^
File ".../deal/_testing.py", line 65, in _check_result
memo = typeguard.CallMemo(
^^^^^^^^^^^^^^^^^^
File ".../typeguard/__init__.py", line 45, in __getattr__
raise AttributeError(f"module {__name__!r} has no attribute {name!r}")
AttributeError: module 'typeguard' has no attribute 'CallMemo'
Diese Ausgabe ist nicht das, was das Beispiel zeigen sollte — und sie bleibt hier trotzdem stehen, weil sie etwas Wichtigeres zeigt.
Zu lesen ist sie so: deal test hat die Funktion gefunden, den ersten Fall endpreis(preis=0.0, rabatt=0.0) erzeugt und ausgeführt. Der Aufruf lief durch, das Ergebnis 0.0 erfüllt die Nachbedingung — und beim anschließenden Typcheck des Rückgabewerts ist deal abgestürzt: Es ruft typeguard.CallMemo auf, eine Funktion, die es in typeguard 4.x nicht mehr gibt. Betroffen ist also genau der Erfolgspfad; ein gefundener Vertragsbruch würde vorher gemeldet.
Für die Lehre ist das ein nützlicher Befund, kein Ärgernis. Design by Contract lebt von einem Werkzeug-Stapel — Laufzeitprüfung, Testgenerierung, symbolische Ausführung — und dieser Stapel ist deutlich dünner besetzt als der um pytest. Wer DbC in einem echten Projekt einsetzt, sollte damit rechnen, dass eine dieser Schichten gerade nicht funktioniert, und wissen, welche davon er wirklich braucht. Die Laufzeitprüfung — der Teil, der im Programm selbst steckt — ist davon nicht betroffen und funktioniert in allen Beispielen oben.
Die Testgenerierung lässt sich außerdem ersetzen. Zwei Wege stehen im Rest dieses Kapitels:
Hypothesis direkt, mit
deal.cases(...)als Brücke — das ist der Abschnitt Abschnitt Kombination von DbC mit Hypothesis & CrossHair unten und läuft hier durch.crosshair check, das dieselbendeal-Dekoratoren liest, aber symbolisch statt mit Zufallswerten arbeitet — siehe den folgenden Abschnitt.
Wo das in diesem Skript wirklich läuft¶
Die Beispiele in diesem Kapitel sind zum Erklären gebaut. Ein deal-Einsatz in einem Modul, das nicht für die Lehre geschrieben wurde, steht an anderer Stelle im Repository: part-practical/gen7engine.py, die Spiellogik der KI-generierten Tic-Tac-Toe-Fassung aus Generierte Wirtschaftssimulation.
Dort sind fünf Methoden mit Verträgen versehen, und die Verträge sind inhaltlich interessant, weil sie Eigenschaften festhalten, die man in Typen nicht ausdrücken kann:
| Methode | Vertrag (verkürzt) | was er behauptet |
|---|---|---|
norm | sorted(result) == sorted(b) | Die Normalisierung permutiert das Brett, sie erfindet und verliert keine Steine |
valid_moves | all(0 <= i <= 8), len(set(res)) == len(res) | gültige Feldindizes, keine Dopplungen |
apply_move | result.count('.') == b.count('.') - 1 | ein Zug belegt genau ein freies Feld |
is_terminal | len(b) == 9 als Vorbedingung | die Repräsentation bleibt ein 9-Zeichen-String |
mm | Minimax-Vorbedingung | dieselbe Brett-Invariante, rekursiv |
Bemerkenswert ist der Zusammenhang zur Entstehung des Codes: Die Verträge wurden nachträglich an KI-generierten Code geschrieben, den niemand Zeile für Zeile gereviewt hat. Genau dafür sind sie ein gutes Werkzeug — sie halten fest, was man erwartet, ohne dass man verstehen muss, wie die Implementierung es erreicht. Was crosshair check daraus macht, steht in jenem Kapitel: kein Gegenbeispiel, aber auch keine Bestätigung.
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.pyFindet 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
icontracterlauben logische Prüfungen zur Laufzeit. Fehler werden deterministisch beim Eintritt abgefangen.Phase 4 (Concolic Testing / Symbolische Ausführung): Werkzeuge wie
CrossHairdocken an Laufzeit-Verträge an und übersetzen sie mittels SMT-Solvern in mathematische Beweise.Phase 5 (Full Static Verification): Werkzeuge wie
Naginiverifizieren 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 40 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.pyMathematisch 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 (
satoderunsat). 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,cryptographyoderllama-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.pyINFO: 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/user/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/user/.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.
Zusammenfassung und Kontrollfragen¶
Ein Test prüft einen Fall, ein Vertrag prüft jeden Aufruf — dafür sagt der Vertrag nichts darüber, ob die Funktion überhaupt das Richtige tut.
Eine Vertragsverletzung ist ein Programmierfehler und gehört nicht in ein
except; ein Domänenfehler wie “zu wenig Geld” ist eine reguläre Exception und wird behandelt.Verträge sind zugleich Spezifikation: Sobald Vorbedingungen aufgeschrieben sind, können Hypothesis und CrossHair daraus Eingaben ableiten, ohne dass man Testfälle nennt.
Ein Fund von CrossHair ist ein harter Befund, ein Nicht-Fund nur eine Zeitangabe — erst
--report_allmacht sichtbar, welcher von beiden Fällen vorliegt.Der Werkzeugstapel um Design by Contract ist deutlich dünner besetzt als der um
pytest; wer ihn einsetzt, sollte wissen, welche Schicht er wirklich braucht — die Laufzeitprüfung im Programm selbst ist die verlässlichste.
Kontrollfragen
Was unterscheidet eine Vorbedingung von der Prüfung einer Nutzereingabe? Was folgt daraus für die Frage, ob man den entstehenden Fehler abfangen darf?
crosshair checkgibt für Ihr Modul nichts aus und endet mit Exit-Code 0. Dürfen Sie daraus schließen, dass die Verträge gelten? Welche Option zeigt, was tatsächlich passiert ist?Ein Vertrag und ein Unit Test beschreiben dieselbe Eigenschaft einer Funktion. Welchen Vorteil hat jeder von beiden gegenüber dem anderen?
!rm -f art_of_the_deal.py dealdemo.py deal_hypothesis.py first_contract.py z3_example.py atheris_fuzz.py crash-*zsh:1: no matches found: crash-*