module Boleite::Random::Contracts

Defined in:

boleite/random.cr

Constant Summary

CLASS_DATA = ClassData(Boleite::Random).new
CONTRACTED_METHODS = ["seed()", "initialize(seed)", "get_int()", "get_int(min, max)", "get_zero_to_one()", "rand(max : Int)"] of _
CONTRACTS = {:next_def => nil, def get_int(min, max) : UInt32 num = generate (num % (max - min)) + min end => [{:ensures, "return_value >= min", do return_value >= min end}, {:ensures, "return_value < max", do return_value < max end}]} of _ => _
IGNORED_METHODS = ["finalize", "contract_pre_get_int", "contract_post_get_int", "contract_requires_get_int", "contract_ensures_get_int", "generate"] of _
INVARIANTS = [] of _

Class Method Summary

Macro Summary

Class Method Detail

def self.on_assert_fail(condition, type) #

[View source]
def self.on_contract_fail(contract, condition, type, method) #

[View source]

Macro Detail

macro add_contract(stage, str, &test) #

[View source]
macro add_invariant(str, &test) #

[View source]
macro ignore_method(method) #

[View source]