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:

  1. Es gibt einen Typen (Sorte) für den Zustand, welcher im Rahmenalgorithmus als Akkumulator fungiert.
  2. Es gibt eine Schrittfunktion, die einen alten Akkumulator in den nächsten Akkumulator überführt.
  3. Es gibt eine Extraktorfunktion, die aus dem Zustandsobjekt den y-Wert für die aktuelle Iteration rausholt.
  4. 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.