Где оценивать инварианты после и до вызова рутины? - PullRequest
Новая
       34

Где оценивать инварианты после и до вызова рутины?

1 голос
/ 15 июня 2011

В проектировании по контрактам инвариант класса должен выполняться в двух случаях: после создания объекта и после вызова подпрограммы.Есть ли какие-нибудь примеры или условия, которые я должен выполнить для оценки перед вызовом процедуры?

1 Ответ

4 голосов
/ 15 июня 2011

Инвариант класса может быть нарушен перед вызовом функции.Условия могут быть разными, я представляю только самые очевидные из них:

  1. Псевдоним.Объект ссылается на некоторый другой объект, который участвует в инварианте класса, и этот другой объект изменяется третьей стороной: 

    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

  2. Внешнее состояние.Объект связан с внешними данными, на которые ссылается инвариант класса, и может неожиданно измениться: 

    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.

  3. Обратный вызов.Объект может быть передан другому в недопустимом состоянии: 

    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

    Обратный вызов HADNLER, выполняемый функцией iterate_over_elements класса STRUCTURE, вызывает нарушение инварианта, поскольку handler не в хорошем состоянии: 

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

Можно утверждать, что все случаи из-за программных ошибок и недостатков, но это именно цель инвариантов класса, чтобы пойматьвключая случаи, когда нарушение происходит до вызова функции.

...