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

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

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

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.annotations.Operation
import org.jetbrains.kotlinx.lincheck.strategy.stress.*
import org.jetbrains.kotlinx.lincheck.verifier.*
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 {
    val s = LinkedList<Int>()

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