Eiffel Contracts сомнения

Question

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

Если бы вы могли предоставить подсказки синтаксиса для этого, это было бы здорово, потому что я не являюсь мастером в языке Eiffel, и его ключевые слова все еще немного сложны и трудны для понимания для меня на моем нынешнем уровне знаний.

class TIME
feature -- Initialization
 make (one_hour, one_min, one_sec: NATURAL_8)
 -- Setup ‘hour’, ‘minute’, and ‘seconds’ with
 -- ‘one_hour’, ‘one_min’, and ‘one_sec’, as corresponds.
 require
 do
 hour := one_hour
 minute := one_min
 second := one_sec
 ensure
 end
feature -- Setters
 set_hour (one_hour: NATURAL_8)
 -- Updates `hour' w/ value ‘one_hour’.
 require

 do
 hour := one_hour
 ensure

 end
 set_min (one_min: NATURAL_8)
 -- Updates `minute' w/ value ‘one_min’.
 require
 do
 minute := one_min
 ensure
 end
 set_sec (one_sec: NATURAL_8)
 -- Updates `second' w/ value ‘one_sec’.
 require
 do
 second := one_seg
 ensure
 end
feature -- Operation
 tick
 -- Counts a tick for second cycle, following 24 hr format
 -- During the day, “tick” works as follows
 -- For example, the next second after 07:28:59 would be
 -- 07:29:00. While the next second of 23:59:59
 -- is 00:00:00.
 do
 ensure
 end
feature -- Implementation
 hour: NATURAL_8
 minute: NATURAL_8
 second: NATURAL_8
invariant
 range_hour: hour < 24
 range_minute: minute < 60
 range_second: second < 60
end

Answer 1

Вот что я бы использовал:

Для конструктора:

make (one_hour, one_min, one_sec: NATURAL_8)
        -- Setup `hour', `minute', and `seconds' with
        -- `one_hour', `one_min', and `one_sec', as corresponds.
    require
        Hour_Valid: one_hour < 24
        Minute_Valid: one_min < 60
        Second_Valid: one_sec < 60
    do
        hour := one_hour
        minute := one_min
        second := one_sec
    ensure
        Hour_Assing: hour = one_hour
        Minute_Assing: minute = one_min
        Second_Assing: second = one_sec
    end

Другими словами, предварительные условия указывают, что требуется для того, чтобы аргументы были действительны в контексте класса. Вы можете спросить, зачем ставить эти предварительные условия, если они уже есть в инвариантах. Ответ: оба не существуют по одной и той же причине. Под инвариантом следует понимать состояние, в котором класс должен (всегда) быть действительным. Единственный, кто должен быть уверен, что этот инвариант действителен, это сам класс или его потомок (но не клиент класса). Другими словами, это роль функции make чтобы убедиться, что инвариант действителен, а не вызывающих функцию make, Это приводит нас к причине предварительных условий, которые я поставил make, Потому что да, это роль make чтобы быть уверенным, что инварианты соблюдаются, но если make Чтобы уважать инварианты, он должен ограничивать клиента в отношении того, какое значение он может получить в качестве аргументов. Итак, другими словами, предварительное условие "Hour_Valid: one_hour <24" гарантирует, что функция "make" может быть уверена в том, что она может уважать инвариант range_hour: hour < 24'.

Теперь для постусловия. Вы можете найти странным поставить постусловие типа "Hour_Assing: hour = one_hour", когда первая строка подпрограммы - "hour:= one_hour". Дело в том, если я унаследую от класса TIME и я изменяю реализацию (например, я использую временные метки, такие как число секунд с начала дня), соблюдение постусловия не будет столь же тривиальным, но постусловие все равно будет применяться к новому make рутина. Вы должны видеть их (предусловие и постусловие) как документацию. Это все равно, что сказать звонящим по телефону make что если аргумент one_hour действительно, я могу гарантировать, что hour будет равен one_hour и что бы ни была реализация.

Теперь я бы поставил эквивалентные предварительные условия и постусловия для каждого сеттера. Например:

set_hour (one_hour: NATURAL_8)
        -- Updates `hour' with the value ‘one_hour’.
    require
        Hour_Valid: one_hour < 24
    do
        hour := one_hour
    ensure
        Hour_Assign: hour = one_hour
    end

Что касается инвариантов, я думаю, что вы уже добавили хорошие в свой код. Так что больше никаких объяснений здесь не требуется, я думаю. Чтобы закончить, очень важно видеть все контракты (предусловия, постусловия и инварианты) как документацию. Они должны быть необязательными, и если компилятор удаляет их, результирующая программа должна быть эквивалентна той, которая содержит контракты. Посмотрите на документацию кода, которая может помочь вам в отладке.

Answer 2

Я не эксперт в Eiffel, мой опыт в основном исходит из C# CodeContracts, но здесь все и так.

Я приведу только примерный синтаксис для вашей функции set_hour. Надеюсь, вы можете обобщить это на весь пример:

 set_hour (one_hour: NATURAL_8)
 -- Updates `hour' w/ value ‘one_hour’.
 require
  -- generally you can put here any boolean expression featuring arguments/class variables
  hour_in_range: one_hour < 24 -- the part before : is optional, it's called
  -- a name tag, helps with debugging.
 do
  hour := one_hour
 ensure
  hour_is_set: hour = one_hour -- it may seem excessive, but for verification tool such as automated proovers this information is valuable. 
  hour < 24 -- this one duplicates your invariant, you may or may not want to add contracts like this, depending on your needs/style/etc.