Temporal Testing with Karat + Turbine

The functional team at Xebia is always eager to test new techniques and methods to improve our code’s confidence. One of our latest avenues is building upon property-based testing but targeting entire execution traces instead of unitary function calls, using the stateful testing abilities already available in libraries like ScalaCheck. In this post, we introduce Karat, a new library we’ve built to leverage temporal specifications into testing.

Temporal specifications

Let’s begin with unit testing. In that form of testing, we check that the result of applying one function to a single value returns the expected value or shows the expected behavior. Using addition as a concrete example, a unit test would check that 3 + 2 == 5. A good testing methodology ensures that corner and edge cases are covered in such tests.

Property-based testing generalizes unit tests to check for properties, which are nothing else than general statements about the behavior of our functions. Instead of a concrete input value, those are generated arbitrarily, so a single property-based test turns into multiple unit tests. In the case of addition, x + 0 == x is one such property that should hold for every input.

Now let’s consider time in our testing methodology, using a counter as a concrete example. Each Counter simply holds a value that can be incremented and inspected.

data class Counter(private var value: Int) {
  fun increment() { value++ }
  val current get() = value
}

We can write a property that ensures that a single operation works as expected. Kotest is used in the example below, but the specifics are not relevant here.

"counter increments" {
  checkAll<Int> { initialValue ->
    val counter = Counter(counter)
    counter.increment()
    counter.current shouldBe (initialValue + 1)
  }
}

From the perspective of time, this resembles a unit test: we’re just checking what happens when a single user executes a single operation. But there are other questions we could ask over this code:

• How should it behave when several increments are called?
• How should it behave when several users operate on Counter concurrently?

This is where temporal specifications enter the game. By using these, we can express properties such as:

• The value of current should always be greater than the initialValue;
• After increment is called, current should be greater than it was.

The key additions are the operations which talk about time: always, after. Those make our tests more robust by moving from a single-step mindset into a more holistic view of the whole lifecycle of the counter.

Specifically, our language to express these temporal specifications is called Linear Temporal Logic. It has been successfully used in the past in a wide range of situations, from testing web interactions to modeling concurrent protocols.

Testing Flows

At the moment of writing, Karat — the name we’ve given to our different efforts in temporal modeling and specification — supports writing specifications and checking them using Kotest and ScalaCheck. However, to keep this post concise, we’re going to use Turbine, a small library to test Kotlin Flows.

In short, a Flow is a computation that provides multiple values sequentially. Its power comes from the tight integration of Flows with the rest of Kotlin’s coroutine mechanism. Many libraries expose their data as Flows, ranging from Spring Boot controllers to Kafka topics. In this post, we’re going to use only three ways to create and manipulate Flows:

1. Using Iterable as source with asFlow,
2. Explicitly emitting the elements using the flow
   builder, and calling emit within its scope.
3. Transforming another Flow using map and flatMap,
   in a similar way we do with lists.

The key ingredient of Turbine is a test extension function. This function takes a block as a parameter, in which we declare the values we expect to come from the Flow. In the code below, we declare that we expect the first item to be 1, the second to be 2, and then we don’t care about the rest of the Flow.

"simple test" {
  (1 .. 10).asFlow().test {
    awaitItem() shouldBe 1
    awaitItem() shouldBe 2
    cancelAndIgnoreRemainingEvents()
  }
}

Let’s bring temporal specifications into the mix! To do so, we create a formula using basic predicates sprinkled with temporal operations. Our first example checks that the values are always positive. The shouldBeSuccess is required here because Flows may either return an actual value, or an exception, which is modeled in Karat using Kotlin’s built-in Result.

val alwaysPositive: TurbineFormula<Int> = always(
  predicate { it.shouldBeSuccess().shouldBePositive() }
)

When talking about Flow, each sequential item is considered a new step in the temporal sense. By using always here, we effectively check a property that should hold over every item. Using Karat is as simple as replacing test with testFormula, and pointing to the corresponding temporal specification.

"positive flow" {
  (1 .. 10).asFlow().testFormula { alwaysPositive }
}

The corresponding issue is raised if the Flow doesn’t satisfy the property. Here we have the error raised when the flow contains the value -1:

StateAssertionError on Item(-1)
- java.lang.AssertionError: -1 should be > 0

Temporal operations are quite powerful. For example, whereas always being positive won’t hold for a counter starting with a negative value, the following property which specifies that eventually the counter turns positive should. In fact, eventually is often used to declare the behavior of concurrent systems: "If an HTTP request of this form comes, then eventually we’ll see a message in this Kafka queue."

val atSomePointPositive: TurbineFormula<Int> = eventually(
  predicate { it.shouldBeSuccess().shouldBePositive() }
)

Another property we declared for our counter was that reading the value should always increase (in fact, it may also stay the same if we don’t call increment between reads). To write this specification, we must introduce another important operator in Karat, remember. As we’ve seen above, when we use predicate, we get a value as argument, representing the value at the current moment. When we use a temporal operator, this current moment may change, so we need to be explicit in recalling all the information.

In our case, we have a collaboration between three operators:

• We use always to work on every element, so within the body of always
  the current value ranges over all those elements.
• At each of those moments, we remember the current element.
• Then we move forward in time by using afterwards, which defines something
  which should happen in every future value (but not in the current one).
• So when we run predicate inside afterwards, we’ve already traveled in
  time to that future state. Hence the need to remember the previous value.
  Putting all of this together, our specification looks as follows.

val alwaysIncreasing: TurbineFormula<Int> = formula<Result<Int>, _, _> {
  always(
    remember { old ->
      afterwards(
        predicate { new ->
          val oldValue = old.shouldBeSuccess()
          val newValue = new.shouldBeSuccess()
          newValue shouldBeGreaterThanOrEqual oldValue
        }
      )
    }
  )
}

Currently, our specification language follows LTL quite closely, with the unfortunate effect of lots of nesting. We’re working hard on implementing a DSL that would allow the previous property to be expressed more linearly.

val alwaysIncreasing = trace {
  val oldValue = current.shouldBeSuccess()
  oneOrMoreSteps()
  val newValue = current.shouldBeSuccess()
  newValue shouldBeGreaterThanOrEqual oldValue
}

You can keep track of our progress (or contribute yourself!) by following the Karat open-source repository.

Conclusion

We’re very excited about temporal specification’s possibilities for more declarative and robust testing. We’ll discuss testing more complex workflows in future installments, including integrations with Ktor servers and TestContainers. Testing is only one of the techniques you can enrich with temporal specification. Modeling with tools like Alloy 6 also dramatically improves the confidence in the system under development.