Последовательная спецификация

Чтобы убедиться, что алгоритм обеспечивает правильное последовательное поведение, вы можете определить его последовательную спецификацию, написав простую последовательную реализацию структуры данных для тестирования.

Для предоставления последовательной спецификации алгоритма для проверки:

1. Реализуйте последовательную версию всех методов тестирования.

2. Передайте класс с последовательной реализацией в параметр sequentialSpecification():

   StressOptions().sequentialSpecification(SequentialQueue::class)
   

Например, здесь представлен тест для проверки правильности j.u.c.ConcurrentLinkedQueue из стандартной библиотеки Java.

import org.jetbrains.kotlinx.lincheck.*
import org.jetbrains.kotlinx.lincheck.annotations.*
import org.jetbrains.kotlinx.lincheck.strategy.stress.*
import org.junit.*
import java.util.*
import java.util.concurrent.*

class ConcurrentLinkedQueueTest {
    private val s = ConcurrentLinkedQueue<Int>()

    @Operation
    fun add(value: Int) = s.add(value)

    @Operation
    fun poll(): Int? = s.poll()
   
    @Test
    fun stressTest() = StressOptions()
        .sequentialSpecification(SequentialQueue::class.java)
        .check(this::class)
}

class SequentialQueue {
    private val s = LinkedList<Int>()

    fun add(x: Int) = s.add(x)
    fun poll(): Int? = s.poll()
}