在调用例程之后和之前，在哪里评估不变量？

class SWITCH -- Creation procedure is ommitted for brevity.
feature
    toggle1, toggle2: TOGGLE -- Mutually exclusive toggles.
    ...
invariant
    toggle1.is_on = not toggle2.is_on
end

SWITCH

switch.toggle1.turn_on -- Make `switch.toggle1.is_on = True`
switch.toggle2.turn_on -- Make `switch.toggle2.is_on = True`
switch.operate -- Class invariant is violated before this call

class TABLE_CELL feature
    item: DATA
        do
            Result := cache -- Attempt to use cached value.
            if not attached Result then
                    -- Load data from the database (slow).
                Result := database.load_item (...)
                cache := Result
            end
        end
feature {NONE} -- Storage
    cache: detachable DATA
invariant
    consistent_cache: -- Cache contains up-to-date value.
        attached cache as value implies
        value ~ database.load_item (...)
end

data := table_cell.item -- Class invariant is violated before this call.

class HANDLER feature
    process (s: STRUCTURE)
        do
            ... -- Some code that sets `is_valid` to False.
            s.iterate_over_elements (Current)
        end
    process_element (e: ELEMENT)
        do
            ...
        end
    is_valid: BOOLEAN
        do
            ...
        end
invariant
    is_valid
end

STRUCTURE

iterate_over_elements

HADNLER

handler

handler.process_element (...) -- Class invariant is violated before the call.