Video zum Artikel

Podcast zum Artikel

Hinweis: Dieses Video und dieser Podcast wurden mithilfe von KI erstellt auf Grundlage der ursprünglichen Inhalten sowie den technischen Erkenntnissen des Autors des Blogartikels.

Sie ist wieder da: Die Spezifikation

Mit KI-gestützten Entwicklungsmethoden rückt die Spezifikation erneut ins Zentrum der Softwareentwicklung. Doch was muss eine Spezifikation leisten, damit sie weder zu viel noch zu wenig vorgibt? Der Artikel zeigt anhand eines Praxisbeispiels, wo User Stories und BDD an Grenzen stoßen und wie formale Methoden Anforderungen mathematisch präzise beschreiben können.

Dank KI-gestützter Entwicklungsmethoden rückt die Spezifikation erneut in den Fokus der Aufmerksamkeit. Es ist also an der Zeit, dass wir uns grundlegende Gedanken über Spezifikationen machen:

• Was können Spezifikationen leisten?
• Weshalb sind Spezifikationen sinnvoll?
• Wie ist das Verhältnis von Spezifikation und Implementierung?
• Kann dieses Verhältnis automatisiert und deterministisch bestimmt werden?
• Was ist die geeignete Form für Spezifikationen?
• Sind Spezifikationen bloße Aufzählungen von Fallbeispielen?
• Ist natürliche Sprache ausreichend?
• Was gewinnt man mit formalisierten Spezifikationen?

In diesem Artikel versuchen wir, diese Fragen anhand eines durchgehenden Praxisbeispiels zu beantworten. Insbesondere die letzten drei Fragen weisen dabei über Ansätze wie Test-driven Development (TDD), Behaviour-driven Development (BDD) und agile Anforderungsdokumentation hinaus – hin zu den sogenannten „Formalen Methoden“. Mit diesen lassen sich Spezifikationen mit mathematischer Präzision allgemeingültig formulieren. Es kann sogar automatisiert geprüft werden, ob eine Implementierung ihre Spezifikation erfüllt.

Software ist kein Selbstzweck

Diesen konkreten Zweck handeln Menschen – Auftraggeber oder allgemeiner: Stakeholder – aus, indem sie sich Gedanken machen, Alternativen betrachten, Schlüsse ziehen, Widersprüche auflösen usw. Aus dem Zweck ergeben sich Anforderungen. Ein Programmierer setzt diese Anforderungen um, indem er Software schreibt, die der Computer ausführen soll. Ein Nutzer bedient die Kombination aus Computer und Software wiederum auf Grundlage seines eigenen Verständnisses. Vom Kopf des Auftraggebers über den des Softwareentwicklers bis zum Kopf des Nutzers ist es also ein weiter Weg, auf dem viel schiefgehen kann. Eine Möglichkeit, diesen Prozess zu vereinfachen, besteht darin, diese Vorstellungen und Anforderungen zu dokumentieren.

Was eine Spezifikation leisten muss

Die Dokumentation der Anforderungen einer Software wird als Spezifikation bezeichnet. Sie steht zwischen dem vagen Gedanken im Kopf des Auftraggebers, der sogenannten Intention, und etwaigen Implementierungen. Um diesen Spagat zu bewältigen, muss ein Spezifikationsdokument einerseits möglichst leicht zu verstehen sein, sodass ein Auftraggeber mit wenig Aufwand bestimmen kann, ob die Spezifikation seiner Intention entspricht. Andererseits muss es möglichst präzise formuliert sein, damit falsche von richtigen Implementierungen eindeutig unterschieden werden können.

Im Endeffekt schränken Spezifikationen die Menge der möglichen, gültigen Implementierungen ein. Eine adäquate Spezifikation für einen gegebenen Zweck verbietet einerseits alle Implementierungen, die dem Zweck widersprechen, und erlaubt andererseits alle Implementierungen, die den Zweck erfüllen.

Eine zu laxe oder uneindeutige Spezifikation lässt auch Implementierungen zu, die dem Zweck widersprechen. Das nenne ich Unterspezifikation. Eine zu strenge Spezifikation hingegen verbietet Implementierungen, die eigentlich noch mit dem ursprünglichen Zweck vereinbar wären und unter Umständen sogar effizienter, robuster oder ergonomischer wären. Das nenne ich Überspezifikation. Ein und dieselbe Spezifikation kann sowohl unter­ als auch überspezifisch sein, also sowohl zweckwidrige Implementierungen zulassen als auch an sich gültige Implementierungen ausschließen.

User Stories als Spezifikation

Auch im agilen Softwareprozess stehen am Anfang die Anforderungen, die oft ausschließlich in Form knapper Beschreibungen einzelner Software-Features – sogenannter User Stories – sowie stichprobenartiger Beispielabläufe dokumentiert werden. Wikipedia definiert User Stories wie folgt: „User Stories werden im Rahmen der agilen Softwareentwicklung […] zusammen mit Akzeptanztests zur Spezifikation von Anforderungen eingesetzt.“

Die wichtigste Eigenschaft guter User Stories ist, dass sie ausschließlich in der Sprache der Fachlichkeit formuliert sind. Das erleichtert die Kommunikation mit nicht-technischen Stakeholdern. Gleichzeitig bleibt den Entwickler:innen damit genügend Freiraum, die beschriebenen Anforderungen mit der sinnvollsten technischen Implementierung zu erfüllen. Auf die Sprache der Fachlichkeit beschränkt man sich notwendigerweise, um durch Implementierungsdetails nicht zu überspezifizieren. Allerdings ist die Verwendung der Sprache der Fachlichkeit nicht hinreichend, um Überspezifikation gänzlich zu vermeiden.

Wenn Features zu viel vorgeben

Eine Spezifikation, die Implementierungen beschreibt, sollte grundsätzlich die Alarmglocken schrillen lassen. Implementierungen beschreiben immer, wie etwas umgesetzt wird. Eine Spezifikation hingegen hat die Aufgabe, zu beschreiben, was umgesetzt werden soll. Durch den Verzicht auf technische Details vermeiden User Stories die Beschreibung von Implementierungen. Viele User Stories beschreiben dennoch Implementierungen – Abläufe, Prozesse, Veränderungen von Zuständen – in der Sprache der Fachlichkeit. Das liegt vorrangig daran, dass mit User Stories meistens Features beschrieben werden. Selbst wenn ein Feature rein in der Sprache der Fachlichkeit formuliert ist, ist es oft schon die Umsetzung eines eigentlich allgemeineren Ziels. Ein Beispiel:

„Um das zu veranschaulichen, nehmen wir das klassische Beispiel eines Geldautomaten. Eine der Story Cards könnte so aussehen: Als Kunde möchte ich an einem Geldautomaten Bargeld abheben, damit ich nicht am Bankschalter Schlange stehen muss.“ (Introducing BDD, Dan North) [1]

Der Geldautomat wird hier als Alternative zum Bankschalter mitsamt Bankangestelltem und Warteschlange erwähnt. Die Begründung für das Feature bezieht sich auf einen Nachteil des bisherigen Systems: lange Wartezeiten. Natürlich möchte kein Bankkunde in der Schlange warten, aber das ließe sich auch bewerkstelligen, indem er einfach zu Hause bliebe. Was in dieser Feature-Beschreibung jedoch implizit bleibt, ist die Tatsache, dass hier ein Kunde Bargeld im Geldbeutel haben möchte. Nur deshalb nimmt er den Gang zur Bank auf sich. Wer Anforderungen über Features spezifiziert, schließt damit oftmals alternative Umsetzungen desselben Ziels aus. In Deutschland kann man heute auch an Bargeld kommen, indem man sich bei einem Supermarkteinkauf, der mit Kreditkarte bezahlt wird, zusätzlich ein paar Geldscheine auszahlen lässt. Eine solche Umsetzung der Anforderung „Kunde will Bargeld“ wäre mit dem oben beschriebenen Feature allerdings ausgeschlossen.

User Stories sind nicht notwendigerweise überspezifiziert. Gute User Stories beschreiben zusätzlich zum Feature eine sogenannte Capability, also eine Fähigkeit, die durch das Feature bereitgestellt werden soll. Diese Capabilities entsprechen in der Regel den Anforderungen auf einem zweckdienlicheren Abstraktionslevel.

Wenn zentrale Begriffe unspezifiziert bleiben

User Stories spezifizieren Features. Dazu müssen Begriffe verwendet oder implizit vorausgesetzt werden. Die obige Geldautomaten-User-Story ist nur verständlich, wenn man die Begriffe „Bankkonto“, „Guthaben“, „Gebühr“, „Geldschein“, „Abbuchung“, „Stornierung“ usw. kennt. All diese Begriffe bleiben in der agilen Spezifikation implizit oder besser: unspezifiziert. Dabei sind es gerade diese Begriffe, die in fast allen User Stories vorkommen oder vorausgesetzt werden. Sauber definierte Begriffe ließen sich dagegen in vielen User Stories wiederverwenden. Das agile Verfahren lässt dieses Potenzial jedoch oft ungenutzt. Ein kleiner Lichtblick ist die Ubiquitous Language beim Domain-driven Design. Sie kann eine gute Ausgangsbasis für die im weiteren Verlauf des Artikels gezeigte Formalisierung sein.

Akzeptanztests

User Stories sind nicht die einzigen Werkzeuge zur Dokumentation von Anforderungen in agilen Softwareprojekten: „Da User Stories den Schwerpunkt vom Schreiben auf das Sprechen verlagern, werden wichtige Entscheidungen nicht in Dokumenten festgehalten, die wahrscheinlich nicht gelesen werden. Stattdessen werden wichtige Aspekte der Stories in automatisierten Akzeptanztests festgehalten und regelmäßig ausgeführt.“ (User Stories Applied, Mike Cohn)

Vielleicht decken automatisierte Akzeptanztests alle Mängel auf, die wir an den User Stories dingfest gemacht haben. Sie zwingen einige Details der User Stories schon deshalb zu größerer Präzision, weil sie als Software ausführbar sein müssen.

Um den Geldautomaten näher zu spezifizieren, können wir ein BDD-Szenario im sogenannten Gherkin-Format aufschreiben:

GIVEN Ein Bankkonto mit 100 EUR Guthaben
WHEN Jemand 30 EUR fordert
AND Die PIN korrekt eingibt
THEN Der Geldautomat gibt einen 20-Euro-Schein und einen 10-Euro-Schein aus
AND Das Bankkonto hat 70 EUR Guthaben

Dieses Szenario konkretisiert das vage formulierte Feature „Geldabheben“. Allerdings ist das Feature nach wie vor gravierend unterspezifiziert, denn Szenarien werden immer nur beispielhaft konkretisiert. Das ist kein Unfall. Beispiele stehen im Mittelpunkt des Behaviour-driven-Development.

„Beispiele stehen im Mittelpunkt von BDD. BDD-Praktiker:innen nutzen in Gesprächen mit Anwender:innen und Stakeholdern konkrete Beispiele, um ihr Verständnis für Funktionen und User Stories jeder Größenordnung zu vertiefen, aber auch, um Unsicherheiten aufzudecken und zu klären.“ (BDD in Action, John Ferguson Smart)

Beispiele eignen sich gut, um die Wirkmechanismen allgemeiner Regeln zu veranschaulichen. Ohne die Bestimmung dieser allgemeinen Regeln geht es jedoch nicht. Das Wort „Bei-spiel“ sagte es schon selbst. Eine endliche Menge von Beispielen allein wird nie das Verhalten in einem unendlichen Raum von Möglichkeiten abdecken können.

Die konkreten Szenarien im BDD sollen stellvertretend für eine ganze Klasse von Anwendungsfällen stehen. Im obigen Geldabhebungs-Szenario soll stellvertretend beschrieben sein, was passieren soll, wenn sowohl das Konto für den geforderten Betrag ausreichend gedeckt ist als auch die PIN korrekt eingegeben wurde. Die Idee dahinter ist, dass nicht-technische Stakeholder mit konkreten Szenarien besser umgehen können als mit abstrakten Beschreibungen des Systemverhaltens. Gleichzeitig wird damit trotzdem die Abstraktionsleistung der nicht-technischen Stakeholder noch herausgefordert, da sie ja auch daran interessiert sind, was passiert, wenn der Kontostand 101 EUR, 102 EUR usw. beträgt. Das Geldautomatenbeispiel funktioniert nur deshalb gut, weil alle bereits wissen, wie Geldautomaten und Bankkonten funktionieren.

Beim Schema „Specification by Example“ wird immer an den gesunden Menschenverstand appelliert, der aus den Beispielen die allgemeinen Klassen korrekt ableiten soll. An seine Grenzen stößt das Beispielhafte jedoch, wenn man neue Software schreibt, also Software, für die es noch keine etablierten Klassen oder Modellstrukturen gibt. Dann mag einem die Abstraktionsleistung vom Szenario zur Klasse selbst beim hundertsten konkreten Beispiel nicht gelingen. Auch ein LLM kann dann nur raten.

Die Alternative: formale Spezifikation mit Mathematik

Ein Praxisbeispiel zeigt, wie ein anderer Ansatz aussehen kann. Wir stellen hier die Features in den Hintergrund und konzentrieren uns auf die Begriffe, die wir mathematisch vollständig beschreiben.

Dieses Beispiel basiert auf einer wahren Geschichte, nämlich einem Projekt, an dem ich einige Jahre lang arbeitete. Die Szenerie ist eine Fabrik, in der viele verschiedene Maschinen nicht nur Produkte fertigen, sondern auch Sensordaten (Temperaturen, Lichtschrankendaten, Tankfüllstände, Log-Meldungen usw.) produzieren. Der Auftrag meines Teams war es, mit Hilfe von Machine-Learning-Algorithmen diese Sensordaten zur automatischen Anomalieerkennung heranzuziehen. Das bedeutet: Unsere Software soll Alarm schlagen, sobald die Sensordaten auf eine Unregelmäßigkeit im Betriebsablauf hindeuten. Denn größere Schäden in der Fabrik, deren Behebung viel Geld kostet, schleichen sich erst langsam über die Zeit ein. Mit Hilfe der Anomalieerkennung können diese Probleme frühzeitig erkannt und somit kostengünstiger behoben werden. Unsere Software sollte dabei nicht auf genau eine einzige Fabrik maßgeschneidert sein, sondern allgemein in allen möglichen Fabriken zum Einsatz kommen können.

Für die Machine-Learning-Komponente hatten wir zwei verschiedene Algorithmen identifiziert, die für die Aufgabe infrage kamen. Beide konnten noch mit sogenannten Hyperparametern vom Anwender feinjustiert werden. Wie üblich, mussten die Modelle anschließend auf Beispieldaten aus der Fabrik „trainiert“ werden. Eine Analyse der Fachlichkeit ergab außerdem, dass die Machine-Learning-Komponente, die ja die eigentliche Anomalierkennung durchführt, besser funktioniert, wenn Fachexpert:innen vorher sogenannte „Feature-Vektoren“ definieren. Statt der Machine-Learning-Komponente sämtliche Sensordaten roh zu übergeben, bildet ein Vorverarbeitungsschritt bereits einen Teil des Fachwissens über ihre Zusammenhänge ab. Ein Beispiel ist ein Tank, in den Wasser hineinfließt, das an einer anderen Stelle wieder abfließt. Ein- und Abfluss werden mit Sensoren überwacht. Zusätzlich gibt es einen Sensor, der die Füllhöhe des Tanks misst. Nun hängen die Größen, die diese drei Sensoren messen, natürlich zusammen. Ein Experte, der seine Fabrik kennt, weiß das auch und kann sogar eine mathematische Gleichung aufstellen, die den Zusammenhang im Idealfall beschreibt. Eine Idee der Anomalieerkennungssoftware war nun, dass die Fachexpert:innen ihr Fachwissen im Vorverarbeitungsschritt einbringen konnten, indem sie symbolische Berechnungen mit den Sensordaten anstellten. Das Beispiel mit dem Tank erfordert Addition, Multiplikation, Skalierung usw. Wir könnten mit dem BDD-Ansatz beginnen, indem wir für jede dieser Operationen ein Feature definieren und es mit Hilfe eines Szenarios beschreiben.

Die allgemeinen Probleme des szenariobasierten Ansatzes wurden bereits besprochen. Hier kommt noch hinzu, dass sich unsere Fachexpert:innen laufend neue Operationen wünschen, zum Beispiel: „Eine Glättung wäre hilfreich.“ Wir müssen also ständig neue Features implementieren und den Weg vom Problem zur Lösung immer wieder neu durchschreiten. In diesem Projekt nehmen wir erst einmal Abstand von Szenarien und schauen auf die Begriffe. Der zentrale Begriff in dieser Domäne, der in fast jedem Featurewunsch auftaucht, ist die „Zeitreihe“. Wir versuchen also, diesen Begriff genauer zu bestimmen.

Natürliche Sprache oder Mathematik?

Wir könnten die Frage nach dem Wesen von Zeitreihen auch ausschließlich in natürlicher Sprache beantworten. Das wäre jedoch eine vertane Chance. Schließlich gibt es mit der Mathematik bereits eine Sprache, mit der seit Jahrhunderten Zusammenhänge präzise beschrieben und analysiert werden. Mit Systemen wie Lean, Agda, Idris, Isabelle/HOL, SMT-LIB2 usw. hält die Mathematik Einzug in die Welt der Computer. In diesem Abschnitt geben wir anhand der Sprache Agda [2] einen kleinen Einblick in diese Welt.

Ein guter Ausgangspunkt für die Analyse einer Fachlichkeit sind konkrete Repräsentationen, die uns von umgebenden Systemen ohnehin aufgezwungen werden. In unserem Beispiel gibt es ja bereits Sensoren, die Daten liefern. Diese Daten bestehen schlicht aus einer langen Liste von Paaren aus Zeitstempel und Sensorwert. Solche Daten werden von den Fachexpert:innen bereits als „Zeitreihen“ bezeichnet. In Agda können wir das mit einem Typsynonym modellieren, wie man es aus Programmiersprachen wie Haskell kennt. Eine Sensorzeitreihe ist eine Liste aus Zeit-Wert-Paaren:

SensorZeitreihe = List (Zeit × Double)

Das Zeichen × kann man als „und“ lesen. Dass diese Repräsentation nicht mit der Bedeutung dieser Daten übereinstimmt, wird deutlich, wenn wir uns ein paar Beispiele für solche Zeitreihen anschauen. Seien t1, t2, t3 Zeitpunkte (Werte vom Typ Zeit) von klein nach groß:

zeitreihe-1 = [ (t1 , 3) , (t2 , 8) , (t3 , 4) ]
zeitreihe-2 = [ (t2 , 8) , (t1 , 3) , (t3 , 4) ]

Bei der Definition von „SensorZeitreihe“ haben wir wahrscheinlich an solche Werte wie in zeitreihe-1 gedacht. Alle Zeit-Wert-Paare, die in der Liste stehen, sind der Zeit nach geordnet. Aber was ist mit zeitreihe-2? Dort kommen dieselben Paare vor, aber das Paar für t2 steht vor dem Paar für t1. Eine Möglichkeit, mit dieser Situation umzugehen, wäre zu bestimmen, dass zeitreihe-2 gar keine echte Zeitreihe beschreibt, sondern ein illegaler Wert ist. Eine andere Möglichkeit wäre, zu sagen, dass die Reihenfolge der Zeitpunkte in der Liste egal ist und die beiden Zeitreihen zeitreihe-1 und zeitreihe-2 dieselbe Zeitreihe darstellen.

An diesem kleinen Beispiel erkennen wir, dass die konkrete Repräsentation und die Bedeutung der Werte dieser Repräsentation nicht dasselbe sind. Datenrepräsentationen wie SensorZeitreihe oder JSON-Objekte, Werte in einer Datenbank oder XML-Serialisierungen sind Teil der Implementierung. Die Bedeutung hingegen ist Teil der Begriffsbestimmungen und damit Teil der Spezifikation.

In den meisten Softwareprojekten wird die Bedeutungsebene nie explizit gemacht und selbst wenn, dann oft nur in natürlicher Sprache. Das ist zwar besser als nichts, aber in natürlicher Sprache lassen sich Unklarheiten leider auch durch vage Formulierungen kaschieren. Erst durch präzise Beschreibungen werden solche Unklarheiten zutage gefördert. Mit der Mathematik steht uns eine über Jahrhunderte erprobte Sprache zur Verfügung, mit der sich alle möglichen Sachverhalte präzise beschreiben und analysieren lassen.

Unser erster Versuch einer präzisen Modellierung des Begriffs der Zeitreihe beginnt mit einer Datenstruktur, die aus der klassischen Programmierung bekannt ist: Map (manchmal auch Dictionary genannt) von Zeit nach Double. Sowohl zeitreihe-1 als auch zeitreihe-2 würden derselben Map Zeit Double entsprechen, also dieselbe Bedeutung haben. Allerdings gibt es nicht nur Double-wertige Zeitreihen, sondern auch An-Aus-Schalter oder Zeitreihen mit Strings. Wir abstrahieren deshalb direkt über den Typ der Werte der Zeitreihe und arbeiten zunächst mit Map Zeit a für beliebige Typen a.

Nun bleibt noch zu klären, was Zeit genau ist. Manche Sensoren liefern Werte im Abstand von einigen Sekunden, andere im Abstand von wenigen Millisekunden. Soll Zeit also der Typ aller Ganzzahlen Int sein, mit der Bedeutung von Millisekunden? Oder sollten wir vorausschauend besser Mikrosekunden oder gar Nanosekunden wählen? Schließlich soll unsere Software auch zukünftige Anforderungen erfüllen können, und in der Zukunft wird es eventuell Sensoren geben, die noch viel feiner auflösen.

Jeder Versuch, die Zeit diskret zu spezifizieren, erfordert Entscheidungen, die sich später als falsch herausstellen könnten. Wir könnten komplexe Rundungsregeln in unsere Spezifikation aufnehmen, aber das verstößt gegen ein wichtiges Prinzip der formalen Spezifikation: So einfach wie möglich! Eine Spezifikation muss so beschaffen sein, dass alle Stakeholder sie innerhalb kürzester Zeit verstehen können. Schließlich muss der Auftraggeber beispielsweise prüfen können, ob die Spezifikation seiner Intention entspricht, und Softwareentwickler:innen müssen in akzeptabler Zeit korrekte Implementierungen programmieren können.

Die richtige Alternative zur diskreten Zeit mit komplexen Rundungsregeln ist deshalb ganz einfach: keine Diskretisierung. Zeit, das sind beliebig präzise reelle Zahlen. Wir definieren bei dieser Gelegenheit auch gleich ein Synonym für Dauer:

Zeit = ℝ
Dauer = ℝ

Diese Entscheidung mag auf den ersten Blick hanebüchen erscheinen. Schließlich sind reelle Zahlen im Allgemeinen im Computer gar nicht darstellbar. Das ist zwar richtig, aber irrelevant. Eine Spezifikation beschreibt nicht das, was in der Software und im Computer wirklich passiert, sondern sie beschreibt das Verständnis der Menschen, die mit der Software arbeiten – sei es als Entwickler:in, Auftraggeber:in oder als Nutzer:in. Über Rundungen müssen wir uns auf dieser Ebene keine Gedanken machen.

Von unserer ursprünglichen Idee, Zeitreihen als Map Int Double zu modellieren, ist jetzt nur noch der Map-Teil übrig. Auch dieser ist nicht optimal. Denn eine weitere Anforderung in unserem Projekt besagte, dass auch konstante Zeitreihen darstellbar sein müssen, also solche, die immer einen bestimmten Wert haben. Diese Zeitreihen lassen sich mit Map nicht gut darstellen. Im Grunde beschreibt eine Map a b eine sogenannte partielle Funktion von a nach b, d. h., für jedes a kann es ein b geben oder es gibt keins. Um konstante Funktionen adäquat darstellen zu können, benötigen wir jedoch das allgemeinere Konzept der totalen Funktionen. Schlussendlich modellieren wir den Begriff der Zeitreihe also so:

Zeit = ℝ
Zeitreihe a = Zeit -> a

Auch ein Zeitreihenkonstruktor für konstante Zeitreihen ist dann schnell definiert:

konstant : a -> Zeitreihe a
konstant x = λ t -> x

konstant x ist dabei ein Lambdaausdruck, der den übergebenen Zeitpunkt t ignoriert und stets x zurückgibt. Das λ-Zeichen kennzeichnet dabei eine Funktion; der Pfeil (->) trennt Argument und Ergebnis.

Mit solchen Zeitreihen können wir problemlos rechnen. Wir können eine Double-wertige Zeitreihe skalieren und auf der y-Achse verschieben:

skaliere : Double -> Zeitreihe Double -> Zeitreihe Double
skaliere n zr = λ t -> (zr t) * n

verschiebe : Double -> Zeitreihe Double -> Zeitreihe Double
verschiebe n zr = λ t -> (zr t) + n

Dabei ist zr die obige Zeitreihe-Funktion (von Zeit nach Double) und (zr t) ist der Double-Wert, den die Zeitreihe zum Zeitpunkt t hat.

Auch die Addition und Multiplikation auf Double-wertigen Zeitreihen definieren wir punktweise:

plus : Zeitreihe Double -> Zeitreihe Double -> Zeitreihe Double
plus zr1 zr2 z = (zr1 z) + (zr2 z)

mal : Zeitreihe Double -> Zeitreihe Double -> Zeitreihe Double
mal zr1 zr2 z = (zr1 z) * (zr2 z)

skaliere und verschiebe sind sich sehr ähnlich und auch plus und mal unterscheiden sich lediglich in dem kleinen Operator, den wir auf den einzelnen Datenpunkten anwenden. Tatsächlich können wir diese Muster abstrahieren und einen punktweise- und einen punktweise2-Kombinator definieren, also Funktionen höherer Ordnung, die andere Funktionen als Argumente entgegennehmen. Dabei müssen wir uns nicht einmal auf Double-wertige Zeitreihen beschränken:

punktweise : (a -> b) -> Zeitreihe a -> Zeitreihe b
punktweise f zr = λ t -> f (zr t)

punktweise2 : (a -> b -> c) -> Zeitreihe a -> Zeitreihe b -> Zeitreihe c
punktweise2 f zr₁ zr₂ = λ t -> f (zr₁ t) (zr₂ t)

f bezeichnet hier die Funktion, die punktweise beziehungsweise punktweise2 als Argument übergeben wird. Die Funktion punktweise liefert eine neue Zeitreihe, indem sie eine einstellige Funktion f auf jeden Wert der Zeitreihe anwendet, während punktweise2 eine zweistellige Funktion f entgegennimmt und zwei Zeitreihen punktweise zu einer neuen kombiniert.

Damit können wir beispielsweise auch einen booleschen Oder-Kombinator definieren:

oder : Zeitreihe Bool -> Zeitreihe Bool -> Zeitreihe Bool
oder = punktweise2 ||

Alle Operationen, die unter das Stichwort „Vorverarbeitungsschritt“ fallen, sind solche Zeitreihentransformationen, also Funktionen, die Zeitreihen als Eingabe annehmen und eine Zeitreihe als Ausgabe liefern. Und nicht nur das. Auch die Machine-Learning-Komponente für die eigentliche Anomalieerkennung, für die die Daten hier vorverarbeitet werden, ist eine Zeitreihentransformation. Wir spendieren diesem Begriff ein eigenes Wort in unserer formalen Spezifikation:

Zeitreihentransformation a b = Zeitreihe a -> Zeitreihe b

Die Machine-Learning-Komponente hat dann folgende Signatur:

erkenneAnomalie : Modell -> Zeitreihentransformation (List Double) Bool

Diese Funktion nimmt die Beschreibung eines Modells mitsamt trainierten Parametern und Hyperparametern entgegen und gibt eine Zeitreihentransformation zurück, die eine Zeitreihe über eine Liste von Double-Werten – den sogenannten Feature-Vektor – in eine Zeitreihe von Bools – Anomalie ja oder nein? – übersetzt.

Eine solche Zeitreihentransformation muss nicht zwingend nach der Vorverarbeitung erfolgen. Sie könnte auch zwischendurch zur Anwendung kommen. Könnte das sinnvoll sein? Na klar. Schließlich haben wir nicht nur einen Machine-Learning-Algorithmus, sondern, wie eingangs beschrieben, zwei verschiedene Algorithmen mit jeweils einigen Hyperparametern. Außerdem können die Modelle auf unterschiedlichen Daten trainiert werden. Es könnte also sinnvoll sein, zwei oder mehr dieser Modelle gleichzeitig laufen zu lassen und als Anomalieerkennung am Ende immer dann anzuschlagen, wenn mindestens eines der Modelle eine Anomalie meldet.

oder' : Zeitreihentransformation a Bool → Zeitreihentransformation a Bool → Zeitreihentransformation a Bool
oder' zrt1 zrt2 = λ zr → oder (zrt1 zr) (zrt2 zr)

meineKonfiguration : Zeitreihentransformation (List Double) Bool
meineKonfiguration = oder' (erkenneAnomalie modell1) (erkenneAnomalie modell2)

Statt eines zweistufigen Vorgehens mit einer Vorverarbeitungs­ und einer Machine-Learning-Komponente sind nun auch Konfigurationen darstellbar, die ganz anders funktionieren. Einen entsprechenden Featurewunsch gab es vorher nicht. Erst als wir diese Möglichkeit, die sich aus der Einsicht in die Begriffe der Fachlichkeit ergab, dem Auftraggeber vorstellten, wurde daraus ein Feature.

Im Nachhinein erscheint die Einsicht, dass die Machine-Learning-Komponente auch nur eine Zeitreihentransformation unter vielen ist, banal. Ohne den Fokus auf die Zeitreihe als zentralen Begriff der Fachlichkeit hätten wir diese Einsicht allerdings wahrscheinlich verpasst.

Die Brücke von der Spezifikation zur Implementierung

Ein kurzer Blick auf eine Implementierung der Zeitreihen veranschaulicht das Verhältnis von Spezifikation und Umsetzung. Die formalisierte Spezifikation ist zwar Code, doch das ist nicht gleichbedeutend mit einer Implementierung. Eine einfache Repräsentation von Zeitreihen könnte beispielsweise aus einer Menge aufeinanderfolgender konstanter Segmente bestehen. Ein Segment besteht aus einem Double-Wert und einer Zeitdauer, die angibt, wie lange dieser Wert gilt. Damit die Repräsentation eine totale Funktion beschreibt, wird zusätzlich ein Double-Wert benötigt, der nach dem letzten Element für den Rest der Zeitleiste gilt. Um in der Implementierung nicht mit reellen Zahlen rechnen zu müssen, verwenden wir für Zeit und Zeitdauer in der Repräsentation einfach den Double-Typ.

Duration : Set
Duration = Double

duration2dauer : Duration → Dauer
duration2dauer = double2ℝ

Seg : Set
Seg = Duration × Double

Repr : Set
Repr = List Seg × Double

Die Beschreibung der Bedeutung von Seg und Repr können wir direkt als Funktion darstellen. Das ist dann die sogenannte Bedeutungsfunktion oder, hochtrabender ausgedrückt, die Denotation.

d' : (t : Zeit) -> (List (Duration × Double)) -> Double -> (t' : Zeit) -> (t ≤ t') -> Double
d' t [] v t' t<t' = v
d' t ((dur , v') ∷ xs) v t' t<t' with t' <? (t + (duration2dauer dur)) ... | yes p = v' ... | no ¬p = d' (t + (duration2dauer dur)) xs v t' (≮⇒≥ ¬p) bedeutung : Repr -> Zeitreihe Double
bedeutung (xs , dflt) t = d' 0 xs dflt t _≤_.z≤n

Die Denotation bildet die Brücke zwischen Implementierung und Spezifikation. Einerseits dokumentiert sie formal die oben nur in natürlicher Sprache formulierte Bedeutung der konkreten Repräsentationen, andererseits erlaubt sie uns, in einer Sprache wie Agda auch formale Beweise der Korrektheit von Operationen zu führen. Um dies zu illustrieren, definieren wir zunächst einen kleinen Operator, der die konstante Zeitreihe konstruiert:

always : Double -> Repr
always x = [] , x

always soll eine Implementierung von konstant sein. Auch das können wir formal ausdrücken, und zwar als Typsignatur:

always-is-konstant : ∀ x -> bedeutung (always x) ≗ konstant x

Das umgedrehte A wird als „für alle“ gelesen und der Pfeil ist zwar der ganz normale Funktionspfeil, kann aber hier als „gilt“ gelesen werden. Das Zeichen ≗ ist ein besonderes Gleichheitszeichen für Funktionen. Es verweist auf die sogenannte extensionale Gleichheit. Sie sieht zwei Funktionen f und g als gleich an, wenn für alle Eingabewerte x gilt: f x ≡ g x. Insgesamt steht dort: Für alle x gilt, dass die Bedeutung von always x gleich konstant x ist. Diese Typsignatur ist zunächst einmal eine Behauptung. Sie wird erst dann zu einem wahren Satz, wenn wir auch einen Beweis für die Behauptung liefern. Das kann im Allgemeinen recht knifflig werden. Hier ist es zum Glück ganz einfach. Der Beweis besteht lediglich aus dem Ausdruck λ t -> refl. In Agda steht refl („Reflexivität“) für den trivialen Gleichheitsbeweis, der immer dann funktioniert, wenn beide Seiten der Gleichung nach Auswertung exakt denselben Ausdruck ergeben.

always-is-konstant x = λ t -> refl

Ausblick

Wie formale Beweise genau funktionieren, kann in diesem kurzen Artikel leider nicht erklärt werden. Es gibt jedoch eine Vielzahl von Fachbüchern sowie standardisierte Schulungsformate wie das iSAQB-Advanced-Modul FM [3]. Dort werden auch andere formale Methoden wie Model Checker, SMT-Solver oder das leichtgewichtigere Property-based Testing gelehrt. All diese Methoden basieren immer auf eindeutigen und möglichst einfachen, formalisierten Spezifikationen.

Nicht alle Anforderungen lassen sich in der oben vorgestellten Art mathematisieren. Die Anforderung, dass beispielsweise eine Warnung prominent angezeigt werden soll, wenn eine bestimmte Bedingung eintritt, lässt sich in zwei Teile unterteilen: einerseits die Bestimmung der Bedingungen, die zur Warnung führen, und andererseits die prominente Anzeige auf einem Bildschirm. Ersteres eignet sich zur Mathematisierung, Letzteres eher nicht. Formale Spezifikationen sind also kein Allheilmittel, aber ein Heilmittel ohne „All“ kann ja auch schon Schmerzen lindern.

Links & Literatur

[1] https://dannorth.net/blog/introducing-bdd/
[2] https://github.com/agda/agda
[3] https://www.isaqb.org/certifications/cpsa-certifications/cpsa-advanced-level/fm/