module Boleite::StateStack::Contracts

Defined in:

boleite/state_stack.cr

Constant Summary

CLASS_DATA = ClassData(Boleite::StateStack).new

CONTRACTED_METHODS = ["initialize()", "empty?()", "push(state : State)", "pop()", "replace(state : State)", "clear()", "top()"] of _

CONTRACTS = {:next_def => nil, def push(state : State) state.next = @state if prev_state = @state prev_state.disable end @state = state state.enable end => [{:requires, "state.nil? == false", do state.nil? == false end}], def pop old_state = @state.as(State) @state = old_state.next old_state.next = nil old_state.disable if new_state = @state new_state.enable end old_state end => [{:requires, "empty? == false", do empty? == false end}], def replace(state : State) pop push(state) end => [{:requires, "empty? == false", do empty? == false end}, {:requires, "state.nil? == false", do state.nil? == false end}], def top @state.as(State) end => [{:requires, "empty? == false", do empty? == false end}]} of _ => _

IGNORED_METHODS = ["finalize", "contract_pre_push", "contract_post_push", "contract_requires_push", "contract_ensures_push", "contract_pre_pop", "contract_post_pop", "contract_requires_pop", "contract_ensures_pop", "contract_pre_replace", "contract_post_replace", "contract_requires_replace", "contract_ensures_replace", "contract_pre_top", "contract_post_top", "contract_requires_top", "contract_ensures_top"] of _

INVARIANTS = [] of _

Class Method Summary

• .on_assert_fail(condition, type)
• .on_contract_fail(contract, condition, type, method)

Macro Summary

• add_contract(stage, str, &test)
• add_invariant(str, &test)
• ignore_method(method)

Class Method Detail

Macro Detail