Ein Algorithmus soll effizient Lösungen zu gegebenen Problemen
berechnen. In der Praxis besteht das Argument, dass der Algorithmus
auch die richtigen Lösungen berechnet, meist aus einer Menge von
Testfällen, einer kurzen Rechtfertigung in natürlicher Sprache oder
einem Stoßgebet. Selbst eine große Menge von Testfällen – auch wenn diese
bspw. mithilfe von
QuickCheck
erstellt wurden – kann aber keine Aussage über die allgemeine
Korrektheit eines Softwarestücks machen. Um wirklich sicher zu gehen,
müssen wir die Struktur des Codes betrachten, darüber Aussagen
treffen und formal argumentieren, dass diese Aussagen auch
allgemeine Geltung haben. Ein Mittel, um das zu tun, lernen wir in
dieser dreiteiligen Artikelserie kennen: Wir nutzen den SMT-Solver
Z3 als automatisierten
Theorembeweiser. Diese Artikel sollen einen ersten Einblick geben in
die Inhalte unserer neuen
iSAQB-Advanced-Level-Schulung zu
Formalen Methoden. In der
Schulung kommen neben Z3 weitere Verifikationswerkzeuge wie
VeriFast,
Forge und Liquid
Haskell zur Sprache.
Da wir formale Aussagen über Code treffen wollen, könnten wir
versucht sein, die
Aussagenlogik zu
nutzen. In der Aussagenlogik kann man sich mit Variablen, „wahr“ und
„falsch“ und ein paar Verknüpfungen logische Ausdrücke basteln (x
oder (nicht y und z)). Das ist zwar ein nettes Vehikel der
theoretischen Informatik, allerdings kann man damit leider für unsere Zwecke ziemlich
wenig Interessantes aussagen. Die nächste Stufe solcher formalen
Systeme wäre die
Prädikatenlogik, bei
der zusätzlich zu den Werkzeugen der Aussagenlogik Prädikate und
Quantoren existieren. Die Mächtigkeit der Prädikatenlogik ist meistens
ausreichend, um Korrektheitsbedingungen von Software zu beschreiben.
Die Herausforderung, Formeln in der Aussagenlogik auf ihre
Erfüllbarkeit zu prüfen, nennt sich „SAT“ (für Satisfiability) und
ist zwar im Worst-Case sehr rechenaufwendig, aber immerhin
machbar. Dahingegen gibt’s für die Prädikatenlogik keinen allgemeinen
Algorithmus, der Formeln mit Sicherheit auf Erfüllbarkeit überprüfen
kann. Für jeden erdenklichen Prüfalgorithmus wird es immer Formeln
geben, bei denen dieser sich in einer Endlosschleife verfängt.
Die Aussagenlogik ist also zu ausdrucksschwach, lässt sich aber automatisch
ausrechnen. Die Prädikatenlogik ist ausdrucksstark genug, lässt sich
aber nicht mehr automatisch ausrechnen. Gibt es vielleicht noch was
dazwischen? Ja, gibt es und es nennt sich SAT Modulo Theories – SMT.
Sehr frei übersetzt: SAT aber mit noch bisschen mehr Werkzeugen. Mit
SMT-LIB-2 gibt’s einen Standard für die Sprache von SMT. Z3 ist ein
sog. SMT-Solver, also ein Prüfalgorithmus für SMT-Formeln.
SMT-LIB-2 ist eigentlich gedacht als einheitliches Austauschformat
zwischen SMT-Libraries auf der einen Seite und SMT-Solvern auf der
anderen Seite. Zu diesem Zwecke basiert die Syntax von SMT-LIB-2 auf
S-Expressions. Der Standard sagt sogar ganz explizit:
The choice of the S-expression syntax and the design of the concrete
syntax was mostly driven by the goal of simplifying parsing, as
opposed to facilitating human readability.
Diese Argumentation ist Teil der Kraft, die stets einfache Parser will
und dabei einfache Lesbarkeit schafft: Als Scheme-, Racket- oder
Clojure-Programmierende ist uns diese Syntax gerade recht. Man kann in
SMT-LIB-2 direkt ziemlich gut programmieren und das werden wir in
diesem Blogartikel demonstrieren. Als Anschauungsbeispiel wollen wir
Geraden rasterisieren, um sie auf den Bildschirm zu malen.
Ich zieh ’ne Line, ihr zieht Leine
Eine Linie hat einen Start- und einen Endpunkt und verhält sich
dazwischen sehr geradlinig. In der abstrakten Welt der Mathematik gibt
es darüber gar nicht viel mehr zu wissen, doch wenn wir solche Linien
auf einen Computerbildschirm zeichnen wollen, haben wir das Problem,
dass dieser in der Regel aus einem Raster an Pixeln besteht; wir
müssen die Punkte auf der idealen Linie also irgendwie in dieses
starre Pixelkorsett zwängen. Um dieses Rasterisierungsproblem im
folgenden noch etwas einfacher zu machen, bestimmen wir, dass der
Startpunkt immer bei der Koordinate (0, 0) und dass der Endpunkt
(dx, dy) rechts oben davon liegen soll – dass also dx > 0 und dy >= 0 sind. Eine solche Linie entspricht weitgehend einer
Geradenfunktion f mit f(x) = dy/dx * x. Solche Funktionen f
können wir in x-Richtung ganz einfach diskretisieren – der erste
Schritt zur Rasterisierung –, indem wir sie nur für ganzzahlige x
aufrufen. Im allgemeinen werden die Ergebnisse – also die y-Werte –
aufgrund des Bruchs dy/dx dann aber rationale Zahlen und keine
Ganzzahlen sein. Um auch in y-Richtung zu diskretisieren, müssen
wir also geeignet runden.
Der simple Algorithmus als Spezifikation
Wir können solche Linien bzw. Geraden in SMT-LIB-2 direkt modellieren
indem wir eine neue sog. „Sorte“ (als Programmierende würden wir
sagen: Typ) einführen:
(declare-datatypes ()
((Line (mk-line (line-dx Int)
(line-dy Int)))))
Ab jetzt ist Line ein Bezeichner für die neue Sorte, mk-line ist
der Konstruktor mit zwei Argumenten und line-dx und line-dy sind
die zwei Getter.
Nicht jeder Ganzzahlwert für dx ist zulässig. Der eine andere
Punkt (außer (0, 0)) muss auch ein anderer Punkt sein. Diese
Einschränkung beschreiben wir in einer Funktion, die prüft, ob dx
ungleich Null ist. Wir wollen uns hier außerdem weiter einschränken auf
„flache“ Linien (dx >= dy) nach oben rechts (dx >= 0 und dy >=
0) (warum wir uns einschränken und warum das keine echte
Einschränkung ist, wird später klar). Insgesamt sieht die
Validierungsfunktion so aus:
(define-fun line-valid ((l Line))
Bool
(and
(> (line-dx l) 0)
(>= (line-dx l)
(line-dy l))
(>= (line-dy l)
0)))
Für eine solche valide Linie können wir die (rationale) Steigung
durch eine Divison berechnen. Diese Division ist zulässig, weil dx
echt größer Null ist.
(define-fun line-slope ((l Line))
Real
(/ (line-dy l)
(line-dx l)))
Mithilfe des line-slope finden wir den exakten (rationalen) y-Wert
für einen gegebenen x-Wert mit einer einfachen Multiplikation
heraus. Die Rasterisierung in x-Richtung ist damit automatisch
sichergestellt, denn x kann nur ganzzahlige Werte annehmen:
(define-fun line-exact-y ((l Line) (x Int))
Real
(* (line-slope l) x))
Wenn wir jetzt wissen möchten, welcher Pixel zu diesem y-Wert
korrespondiert, dann müssen wir nur noch runden. Die eingebaute
Funktion to_int macht eine Real-Zahl zu einer Int-Zahl, rundet
dabei allerdings immer ab. Um bspw. 0.6 zu 1 aufzurunden, addieren
wir vor dem to_int-Aufruf einfach noch 0.5 drauf.
(define-fun round-to-nearest ((x Real))
Int
(to_int (+ x 0.5)))
(define-fun line-rounded-y ((l Line) (x Int))
Int
(round-to-nearest (line-exact-y l x)))
Um in der Welt der puren Funktionen zu bleiben, zeichnen wir nicht
direkt per Seiteneffekt auf den Bildschirm, sondern berechnen erst
eine Liste mit allen y-Werten von links nach rechts. Hier soll’s ja
nicht um Effekte gehen, sondern um Algorithmen. Das Berechnen einer
solchen Liste macht der übliche rekursive Algorithmus. Den kann man auch
in SMT-LIB-2 hinschreiben:
(define-fun-rec draw-simple-acc ((l Line) (x Int) (todo Int))
(List Int)
(ite (<= todo 0)
;; done
nil
;; recurse
(insert (line-rounded-y l x)
(draw-simple-acc l (+ x 1) (- todo 1)))))
(define-fun draw-simple ((l Line) (todo Int))
(List Int)
(draw-simple-acc l 0 todo))
draw-simple nimmt als Parameter eine Linie (also im wesentlichen eine Geradensteigung) und
ein Ziel auf der x-Achse (todo). Wir rufen dann die Funktion
draw-simple-acc auf mit dem zusätzlichen initialen Akkumulator 0. Dieser
Akkumulator beschreibt die gerade betrachtete x-Koordinate, für welche
wir die passende y-Koordinate entlang der Linie berechnen
wollen. nil ist die leere Liste und mit insert bauen wir aus einer
alten Liste und einem Listenelement eine neue Liste zusammen (oft
heißt das Ding cons oder in Clojure conj).
Wir können den Algorithmus ausprobieren, indem wir ans Ende der Datei
noch einen (check-sat)-Aufruf machen. Danach können wir uns
Ergebnisse mithilfe von (simplify ...) ausdrucken. Dieser Code:
(check-sat)
(simplify (draw-acc (mk-state-1 (mk-line 7 5) 0) 4))
liefert dieses Ergebnis:
sat
(insert 0 (insert 1 (insert 1 (insert 2 nil))))
Wir sehen, dass bei diesen „flachen“ Geraden manchmal ein Schritt nach
oben gemacht wird, manchmal verbleibt die rasterisierte Linie aber
auch für ein paar Schritte auf derselben Höhe.
Die Funktion draw-simple-acc macht eine Menge Dinge gleichzeitig:
Abbruchbedingung prüfen, Business-Logik aufrufen, den einen Teil der
Business-Daten in die Liste einfügen und den anderen Teil der
Business-Daten an den nächsten rekursiven Aufruf weiterleiten. Im
folgenden werden wir die Business-Logik dieses Algorithmus nach und
nach optimieren, während der buchhalterische Rest des Algorithmus gleich
bleibt. Deshalb faktorisieren wir draw-simple-acc schon jetzt in
zwei Teile. Der eine Teil ist schon fertig – wir nennen diesen
Teil den Rahmenalgorithmus. Der andere Teil ändert sich mit jeder
Optimierung – wir nennen diesen Teil die Businesslogik. Die
Businesslogik besteht immer aus vier Elementen:
- Es gibt einen Typen (Sorte) für den Zustand, welcher im
Rahmenalgorithmus als Akkumulator fungiert.
- Es gibt eine Schrittfunktion, die einen alten Akkumulator in den
nächsten Akkumulator überführt.
- Es gibt eine Extraktorfunktion, die aus dem Zustandsobjekt den
y-Wert für die aktuelle Iteration rausholt.
- Um mit der Rechnerei starten zu können, brauchen wir eine Funktion,
die uns ein initiales Zustandsobjekt baut.
In Code sieht das dann so aus: Der Zustand enthält eine Linie und das
x, was vorher der Akkumulator war.
(declare-datatypes ()
((State-1 (mk-state-1 (state-1-line Line)
(state-1-x Int)))))
Ähnlich zum Linienobjekt sind nur manche Zustandsobjekte valide. Wir definieren entsprechend wieder eine Validierungsfunktion:
(define-fun state-1-valid ((st State-1))
Bool
(and
(line-valid (state-1-line st))
(>= (state-1-x st) 0)))
Wir definieren außerdem die Extraktorfunktion:
(define-fun state-1-exact-y ((st State-1))
Real
(line-y (state-1-line st)
(state-1-x st)))
(define-fun state-1-y ((st State-1))
Int
(round-to-nearest
(state-1-exact-y st)))
Die Schrittfunktion zählt einfach nur das x hoch. Das Linienobjekt
wird nicht verändert:
(define-fun step-1 ((st State-1))
State-1
(mk-state-1
(state-1-line st)
(+ 1 (state-1-x st))))
Die Funktion, die das initiale Zustandsobjekt baut, ist mit dem
Konstruktor mk-state-1 bereits gegeben. Wir können diese Teile
jetzt in den Rahmenalgorithmus einsetzen. Das sieht dann so aus:
(define-fun-rec draw-1-acc ((st State-1) (todo Int))
(List Int)
(ite (<= todo 0)
;; done
nil
;; recurse
(insert (state-1-y st)
(draw-1-acc (step-1 st) (- todo 1)))))
(define-fun draw-1 ((l Line) (todo Int))
(List Int)
(draw-1-acc (mk-state-1 l 0) todo))
Als funktional Programmierende würden wir den Rahmenalgorithmus
natürlich gern als Funktion höherer Ordnung hinschreiben. Das geht in
SMT-LIB-2 leider nicht.
Addition statt Multiplikation
Dieser Algorithmus ist einfach zu verstehen, arbeitet allerdings sehr
verschwenderisch. Er macht mit der Funktion state-1-y in jedem
Schritt eine Multiplikation. Das ist teuer, zumindest teurer als es
sein müsste. Wir wissen ja, dass wir in jeder Iteration nur einen
x-Schritt nach rechts gehen. Zur Optimierung dieses Algorithmus können
wir uns die meiste Arbeit dieser wiederholten Multiplikation sparen,
indem wir in jedem Schritt einfach nur einmal die Steigung auf den
vorher berechneten y-Wert draufaddieren. Das erfordert natürlich, dass
wir uns den y-Wert auch gemerkt haben, also packen wir diesen in ein
neues Zustandsobjekt State-2. Wir definieren den Extraktor
gleich mit:
(declare-datatypes ()
((State-2 (mk-state-2 (state-2-line Line)
(state-2-x Int)
(state-2-exact-y Real)))))
(define-fun state-2-y ((st State-2))
Int
(round-to-nearest
(state-2-exact-y st)))
Die zugehörige Validierungsfunktion muss jetzt auch noch prüfen, ob
der y-Wert im Zustand auch zur angegebenen Linie und dem x-Wert passt.
(define-fun state-2-valid ((st State-2))
Bool
(and
(line-valid (state-2-line st))
(>= (state-2-x st) 0)
(= (state-2-exact-y st)
(line-y (state-2-line st)
(state-2-x st)))))
Die neue Schrittfunktion macht jetzt nur noch eine Addition und keine
ganze Multiplikation mehr:
(define-fun step-2 ((st State-2))
State-2
(mk-state-2
(state-2-line st)
(+ 1 (state-2-x st))
(+ (state-2-exact-y st)
(line-slope
(state-2-line st)))))
Und jetzt fehlt nur noch die Funktion, die für eine gegebene Linie den
initialen Zustand berechnet:
(define-fun init-state-2 ((l Line))
State-2
(mk-state-2 l 0 0.0))
Diese Funktionen können wir wieder in den Rahmenalgorithmus
einsetzen. Wir nennen das Ergebnis draw-2 (und führen es hier nicht
noch mal aus).
Das haben wir jetzt alles so hinprogrammiert, aber ist es auch
richtig? Um diese Frage beantworten zu können, müssen wir uns erst mal
klar machen, was „richtig“ hier überhaupt bedeutet. Ich würde
vorschlagen, der Algorithmus arbeitet richtig, wenn er unter Absehung
technischer Details die gleichen Ergebnisse wie der einfachere
Algorithmus oben produziert. Formalisiert würden wir also gern solche
eine solche Aussage prüfen:
(assert
(forall ((l Line)
(todo Int))
(= (draw-1 l todo)
(draw-2 l todo))))
Das kann man in SMT-LIB-2 so hinschreiben und Z3 rennt sogar los – es
wird aber nie fertig. Mit einem solchen Programm befinden wir uns in
einem Logikfragment, das für Z3 nicht mehr entscheidbar ist. Wir
können aber eine Spezifikation aufschreiben, die funktional äquivalent
und trotzdem entscheidbar ist. Der erste Teil davon ist einfach: Wir
wollen sagen, dass der initiale Zustand, der aus init-state-2
rausfällt ein valider Zustand ist und außerdem das erwartete y
zurückgibt, wenn man den Extraktor darauf anwendet. Wir wollen
natürlich diese Aussage wieder prüfen für alle Linien. Dennoch
müssen wir kein forall verwenden. Mit forall suchen wir nach einer
Garantie der Allgemeingültigkeit unserer Formel. Anstatt aber die
Allgemeingültigkeit zu prüfen, können wir auch das Gegenteil unserer
Formel behaupten und dann fragen, ob diese negierte Formel erfüllbar
ist:
(declare-const l Line)
(assert (line-valid l))
(assert
(not (state-2-valid (init-state-2 l))))
(check-sat)
Wir können dieses SMT-LIB-2-Programm mit Z3 prüfen lassen. Raus kommt:
unsat. Das klingt unbefriedigend, ist aber das Ergebnis, das sagt,
dass unsere Verifikation erfolgreich ist. Die Aussage „Unsere Formel
gilt nicht“ ist nicht erfüllbar, für kein einziges Linienobjekt l,
d.h. unsere Formel gilt für alle l.
Das wichtigere Korrektheitskriterium betrifft step-2. Wir
wollen sagen, dass step-2 sich so verhält wie step-1,
abgesehen von einigen technischen Details. Formalisiert:
(declare-const st State-1)
(assert (state-1-valid st))
(assert
(not
(= (step-2
(into-state-2 st))
(into-state-2
(step-1 st)))))
(check-sat)
Hier steht, dass es egal ist, ob wir für einen gegebenen
State-1 zuerst mit into-state-2 in die
State-2-Welt gehen und dann step-2 aufrufen, oder ob
wir zuerst step-1 aufrufen und dann in die
State-2-Welt eintauchen. Dieses Korrektheitskriterium ist ein
typisches „kommutierendes Diagramm“: Egal welchen Pfad man verfolgt,
man landet immer bei demselben Ergebnis. Dass das gilt, bestätigt uns Z3 mit einem weiteren unsat.
Die Korrespondenz zwischen den Welten von State-1 und
State-2, welche wir als Korrektheitskriterium herangezogen
haben, ist noch recht offensichtlich. Dafür hätten wir vielleicht Z3
gar nicht gebraucht. Wir wollen unseren Algorithmus im nächsten
Artikel aber noch weiter verbessern. Die Art der Korrektheit bleibt
dabei immer dieselbe: Wir sagen, unsere neuen Algorithmen sollen sich
wie der offensichtlich richtige erste Algorithmus verhalten.
Permalink
