
Das Funktionsteam bei Xebia ist immer bestrebt, neue Techniken und Methoden zu testen, um die Sicherheit unseres Codes zu verbessern. Einer unserer neuesten Wege ist das
Zeitliche Spezifikationen
Beginnen wir mit Unit-Tests. Bei dieser Form des Testens prüfen wir, ob das Ergebnis der Anwendung einer Funktion auf einen einzelnen Wert den erwarteten Wert liefert oder das erwartete Verhalten zeigt. Am konkreten Beispiel der Addition würde ein Unit-Test prüfen, ob 3 + 2 == 5. Eine gute Testmethodik stellt sicher, dass auch Eck- und Randfälle in solchen Tests abgedeckt werden.
Eigenschaftsbasiertes Testen verallgemeinert Unit-Tests, um auf Eigenschaften zu prüfen, die nichts anderes als allgemeine Aussagen über das Verhalten unserer Funktionen sind. Anstelle eines konkreten Eingabewerts werden diese willkürlich generiert, so dass ein einziger eigenschaftsbasierter Test zu mehreren Unit-Tests wird. Im Falle der Addition ist x + 0 == x eine solche Eigenschaft, die für jede Eingabe gelten sollte.
Betrachten wir nun die Zeit in unserer Testmethodik, wobei wir einen Zähler als konkretes Beispiel verwenden. Jedes Counter enthält einfach einen Wert, der inkrementiert und geprüft werden kann.
data class Counter(private var value: Int) {
fun increment() { value++ }
val current get() = value
}
Wir können eine Eigenschaft schreiben, die sicherstellt, dass eine einzelne Operation wie erwartet funktioniert. Im folgenden Beispiel wird Kotest verwendet, aber die Einzelheiten sind hier nicht relevant.
"counter increments" {
checkAll<Int> { initialValue ->
val counter = Counter(counter)
counter.increment()
counter.current shouldBe (initialValue + 1)
}
}
Vom zeitlichen Standpunkt aus gesehen ähnelt dies einem Unit-Test: Wir prüfen nur, was passiert, wenn ein einzelner Benutzer eine einzelne Operation ausführt. Aber es gibt noch andere Fragen, die wir über diesen Code stellen könnten:
- Wie sollte es sich verhalten, wenn mehrere
incrementaufgerufen werden? - Wie soll es sich verhalten, wenn mehrere Benutzer gleichzeitig auf
Counterarbeiten?
An dieser Stelle kommen die zeitlichen Spezifikationen ins Spiel. Mit ihnen können wir Eigenschaften ausdrücken wie:
- Der Wert von
currentsollte immer größer sein als der voninitialValue; - Nachdem
incrementaufgerufen wurde, solltecurrentgrößer sein als zuvor.
Die wichtigsten Ergänzungen sind die Operationen, die sich auf die Zeit beziehen: always, after. Diese machen unsere Tests robuster, indem sie von einer einstufigen Denkweise zu einer ganzheitlicheren Sicht auf den gesamten Lebenszyklus des Zählers übergehen.
Unsere Sprache, mit der wir diese zeitlichen Spezifikationen ausdrücken, heißt Lineare Temporale Logik. Sie wurde in der Vergangenheit erfolgreich in einer Vielzahl von Situationen eingesetzt, vom Testen von Web-Interaktionen bis hin zur Modellierung von nebenläufigen Protokollen.
Testabläufe
Zum Zeitpunkt der Erstellung dieses Beitrags unterstützt Karat - der Name, den wir unseren verschiedenen Bemühungen im Bereich der temporalen Modellierung und Spezifikation gegeben haben - das Schreiben von Spezifikationen und deren Überprüfung mit Kotest und ScalaCheck. Um diesen Beitrag jedoch kurz zu halten, werden wir Turbine verwenden, eine kleine Bibliothek zum Testen von Kotlin Flow s.
Kurz gesagt, eine Flow ist eine Berechnung, die mehrere Werte sequentiell liefert. Ihre Stärke liegt in der engen Integration von Flows mit dem übrigen Coroutine-Mechanismus von Kotlin. Viele Bibliotheken stellen ihre Daten als Flows zur Verfügung, von Spring Boot-Controllern bis hin zu Kafka-Themen. In diesem Beitrag werden wir nur drei Möglichkeiten verwenden, um Flows zu erstellen und zu manipulieren:
- Verwenden Sie
Iterableals Quelle mitasFlow, - Explizites Emittieren der Elemente mit dem
flowBuilder und der Aufruf vonemitinnerhalb des Geltungsbereichs. - Transformieren Sie ein anderes
FlowmitmapundflatMap, in ähnlicher Weise, wie wir es mit Listen tun.
Der Hauptbestandteil von Turbine ist ein test
cashapp.github.io/turbine/docs/0.x/turbine/app.cash.turbine/test.html
Erweiterungsfunktion. Diese Funktion nimmt einen Block als Parameter entgegen, in dem wir die Werte deklarieren, die wir von 1 ist, das zweite 2, und der Rest von Flow ist uns dann egal.
"simple test" {
(1 .. 10).asFlow().test {
awaitItem() shouldBe 1
awaitItem() shouldBe 2
cancelAndIgnoreRemainingEvents()
}
}
Lassen Sie uns zeitliche Spezifikationen in den Mix bringen! Dazu erstellen wir eine Formel mit einfachen Prädikaten, die mit zeitlichen Operationen gespickt sind. Unser erstes Beispiel prüft, ob die Werte immer positiv sind. Die shouldBeSuccess ist hier erforderlich, weil Flowentweder einen tatsächlichen Wert oder eine Ausnahme zurückgeben kann, die in Karat mit Hilfe der in Kotlin eingebauten Result modelliert wird.
val alwaysPositive: TurbineFormula<Int> = always(
predicate { it.shouldBeSuccess().shouldBePositive() }
)
Wenn wir über Flow sprechen, wird jedes sequenzielle Element als neuer Schritt im zeitlichen Sinne betrachtet. Indem wir hier test durch testFormula und das Verweisen auf die entsprechende zeitliche Spezifikation.
"positive flow" {
(1 .. 10).asFlow().testFormula { alwaysPositive }
}
Das entsprechende Problem wird ausgelöst, wenn die Flow die Eigenschaft nicht erfüllt. Hier haben wir den Fehler, der ausgelöst wird, wenn die Bewegung den Wert -1 enthält:
StateAssertionError on Item(-1)
- java.lang.AssertionError: -1 should be > 0
Temporale Operationen sind ziemlich mächtig. Während zum Beispiel ein Zähler, der mit einem negativen Wert beginnt, nicht immer positiv ist, sollte die folgende Eigenschaft, die besagt, dass der Zähler irgendwann positiv wird, gelten. In der Tat wird eventually häufig verwendet, um das Verhalten von nebenläufigen Systemen zu deklarieren: "Wenn eine HTTP-Anfrage dieser Form eintrifft, dann werden wir irgendwann eine Nachricht in dieser Kafka-Warteschlange sehen."
val atSomePointPositive: TurbineFormula<Int> = eventually(
predicate { it.shouldBeSuccess().shouldBePositive() }
)
Eine weitere Eigenschaft, die wir für unseren Zähler deklariert haben, ist, dass das Lesen von value immer zunehmen sollte (tatsächlich kann er auch gleich bleiben, wenn wir zwischen den Lesevorgängen nicht increment aufrufen). Um diese Spezifikation zu schreiben, müssen wir einen weiteren wichtigen Operator in Karat einführen, predicate einen Wert als Argument, der den Wert zum aktuellen Zeitpunkt darstellt. Wenn wir einen temporalen Operator verwenden, kann sich dieser aktuelle Zeitpunkt ändern, so dass wir alle Informationen explizit abrufen müssen.
In unserem Fall handelt es sich um eine Zusammenarbeit zwischen drei Betreibern:
- Wir verwenden
always, um mit jedem Element zu arbeiten, so dass sich der aktuelle Wert innerhalb des Körpers vonalwaysüber all diese Elemente erstreckt. - In jedem dieser Momente finden Sie unter
rememberdas aktuelle Element. - Dann bewegen wir uns in der Zeit vorwärts, indem wir
afterwardsverwenden, das etwas definiert, das in jedem zukünftigen Wert passieren soll (aber nicht im aktuellen). - Wenn wir also
predicateinnerhalb vonafterwardsausführen, sind wir bereits in Zeit zu diesem zukünftigen Zustand gereist. Daher die Notwendigkeit, sich den vorherigen Wert zu merken. Wenn wir all dies zusammennehmen, sieht unsere Spezifikation wie folgt aus.
val alwaysIncreasing: TurbineFormula<Int> = formula<Result<Int>, _, _> {
always(
remember { old ->
afterwards(
predicate { new ->
val oldValue = old.shouldBeSuccess()
val newValue = new.shouldBeSuccess()
newValue shouldBeGreaterThanOrEqual oldValue
}
)
}
)
}
Derzeit lehnt sich unsere Spezifikationssprache recht eng an LTL an, was leider dazu führt, dass viele Verschachtelungen auftreten. Wir arbeiten hart daran, eine DSL zu implementieren, mit der die oben genannte Eigenschaft linearer ausgedrückt werden kann.
val alwaysIncreasing = trace {
val oldValue = current.shouldBeSuccess()
oneOrMoreSteps()
val newValue = current.shouldBeSuccess()
newValue shouldBeGreaterThanOrEqual oldValue
}
Sie können unsere Fortschritte verfolgen (oder selbst etwas beitragen!), indem Sie das Karat Open-Source-Repository verfolgen.
Fazit
Wir sind sehr gespannt auf die Möglichkeiten, die die temporale Spezifikation für deklarative und robuste Tests bietet. Wir werden das Testen komplexerer Arbeitsabläufe in zukünftigen Ausgaben besprechen, einschließlich der Integration mit Ktor-Servern und TestContainern. Testen ist nur eine der Techniken, die Sie mit temporalen Spezifikationen bereichern können. Auch die Modellierung mit Tools wie Alloy 6 verbessert das Vertrauen in das zu entwickelnde System erheblich.
Verfasst von
Alejandro Serrano Mena
Contact



