After watching https://www.youtube.com/watch?v=zi0rHwfiX1Q I tried to port the example from C (implementation) and Erlang (testing) to Python and Hypothesis. Given this implementation (the rem function emulates %'s C behavior):
import math
def rem(x, y):
res = x % y
return int(math.copysign(res,x))
class Queue:
def __init__(self, capacity: int):
self.capacity = capacity + 1
self.data = [None] * self.capacity
self.inp = 0
self.outp = 0
def put(self, n: int):
self.data[self.inp] = n
self.inp = (self.inp + 1) % self.capacity
def get(self):
ans = self.data[self.outp]
self.outp = (self.outp + 1) % self.capacity
return ans
def size(self):
return rem((self.inp - self.outp), self.capacity)
and this test code
import unittest
from hypothesis.stateful import rule, precondition, RuleBasedStateMachine
from hypothesis.strategies import integers
from myqueue import Queue
class QueueMachine(RuleBasedStateMachine):
cap = 1
def __init__(self):
super().__init__()
self.queue = Queue(self.cap)
self.model = []
@rule(value=integers())
@precondition(lambda self: len(self.model) < self.cap)
def put(self, value):
self.queue.put(value)
self.model.append(value)
@rule()
def size(self):
expected = len(self.model)
actual = self.queue.size()
assert actual == expected
@rule()
@precondition(lambda self: self.model)
def get(self):
actual = self.queue.get()
expected = self.model[0]
self.model = self.model[1:]
assert actual == expected
TestQueue = QueueMachine.TestCase
if __name__ == "__main__":
unittest.main()
The actual question is how to use Hypothesis to also parametrize over QueueMachine.cap instead of setting it manually in the test class.
You can set self.queue in an initialize method rather than __init__, using a suitable integers strategy for the capacity.