contracts and property based testing

contracts.py

from dpcontracts import require, ensure, invariant

@invariant("procs can never be empty", lambda self: len(self.procs) > 0)
@invariant("procs must consist only of positive integers",
         lambda self: all(isinstance(x, int) and x > 0 for x in self.procs))
@invariant("space must be positive integer", lambda self: self.space > 0)
class Meltdown:
    def __init__(self, space, procs):
        self.space = space
        self.procs = procs

    @ensure("result must be greater than 0",
            lambda args, result: result > 0)
    def meltdown_eta(self):
        if len(self.procs) == 1:
            return self.space * self.procs[0]
        smallest = min(p for p in self.procs)
        return self.find_eta(smallest, smallest * self.space * len(self.procs))

    @ensure("result must be between low and high",
            lambda args, result: args.low <= result <= args.high)
    def find_eta(self, low, high):
        guess = ((high - low) // 2) + low
        guess_meltdown = self.size_at_time(guess)
        guess_last_ok = self.size_at_time(guess - 1)
        if (guess_last_ok < self.space) and not (guess_meltdown < self.space):
            return guess
        if guess_meltdown < self.space:
            return self.find_eta(guess, high)
        return self.find_eta(low, guess)

    @require("time must be an integer", lambda args: isinstance(args.time, int))
    @require("time must be greater than 0", lambda args: args.time > 0)
    # @ensure("result must not be greater than 0",
    #         lambda args, result: result > 0)
    @ensure("result must not be negative",
            lambda args, result: result >= 0)
    @ensure("result must be an integer",
            lambda args, result: isinstance(result, int))
    def size_at_time(self, time):
        return sum(time // proc for proc in self.procs)

test.py

import random

from hypothesis import given, reject
from hypothesis.extra.dpcontracts import fulfill
from hypothesis.strategies import integers, lists

from contracts import Meltdown


def test_example_one():
    sut = Meltdown(4, [3, 7])
    actual = sut.meltdown_eta()
    assert actual == 9


def test_example_two():
    sut = Meltdown(4, [1])
    actual = sut.meltdown_eta()
    assert actual == 4


def test_example_three():
    sut = Meltdown(16, [2, 4, 3, 6, 384983498])
    actual = sut.meltdown_eta()
    assert actual == 14


@given(integers(min_value=14))
def test_huge_proc(huge):
    sut = Meltdown(16, [2, 4, 3, 6, huge])
    actual = sut.meltdown_eta()
    assert actual == 14


@given(integers(min_value=1), integers(min_value=1))
def test_single_proc(size, proc):
    sut = Meltdown(size, [proc])
    assert size * proc == fulfill(sut.meltdown_eta)()


@given(
    integers(min_value=1, max_value=100),
    lists(integers(min_value=1, max_value=100), min_size=1, max_size=10)
)
def test_shuffled_procs(size, procs):
    shuffled = random.sample(procs, len(procs))
    a = Meltdown(size, procs)
    b = Meltdown(size, shuffled)
    assert fulfill(a.meltdown_eta)() == fulfill(b.meltdown_eta)()


@given(
    lists(integers(min_value=1, max_value=1), min_size=1),
    integers(min_value=1)
)
def test_many_procs_of_one(procs, time):
    m = Meltdown(1, procs)
    assert time * len(procs) == fulfill(m.size_at_time)(time)


@given(integers(min_value=1))
def test_one_proc_size(time):
    m = Meltdown(1, [time])
    assert 1 == fulfill(m.size_at_time)(time)