Eiffel Contracts doubts

Question

I am working on a planning software being coded in Eiffel language, I've created the following code but I am not quite sure of which kind of post conditions and/or pre conditions should be specified for this class' routines.

If you can provide syntax hints for this it would be great because I am not a master in Eiffel language, and its keywords are still a bit tricky & hard to understand for me at my current level of knowledge.

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

I am not an expert in Eiffel, my experience mostly comes from C# CodeContracts, but here it goes.

I will provide just an example syntax for your set_hour feature. Hopefully, you can generalize this to your whole example:

 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.

Answer 2

Here is what I would use:

For the constructor:

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

In other words, the preconditions indicates what is requirement for the arguments to be valid in the context of the class. You may be tempted to ask why put those preconditions if those are already in the invariants. The answer is: both are not there for the same reason. See an invariant as the state that a class must (always) be to be valid. The only one that have to be sure that this invariant is valid is the class itself or it's descendant (but not the client of a class). In other word, it is the role of the feature make to be sure that the invariant is valid, not of the callers of the feature make. That take us to the reason of the precondition I put to make. Because yes, it is the role of make to be sure that the invariants are respected, but if make want to respect the invariants, it have to restrict the client about what value it can receive as arguments. So, in others words, the precondition 'Hour_Valid: one_hour < 24' assure that the feature `make' can be sure that it can respect the invariant 'range_hour: hour < 24'.

Now, for the postcondition. You can find strange to put a postcondition like 'Hour_Assing: hour = one_hour' when the first line of the routine is 'hour := one_hour'. The point is, if I inherit of the class TIME and I change the implementation (for exemple, I use a timestamps like the number of second since the the beginning of the day), the respect of the postcondition will not be as trivial, but the postcondition will still applies to the new make routine. You have to see those (precondition and postcondition) as documentations. It is like saying to the callers of the feature make that if the argument one_hour is valid, I can guaranty you that hour will be equal to one_hour and that, whatever the implementation might be.

Now, I would put equivalent precondition and postcondition to every setters. For example:

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

For the invariants, I think that you put good ones in your code already. So no more explanations are require here I think. To finish, it is very important to see every contracts (preconditions, postconditions and invariants) as documentation. Those must be optional and if the compiler remove them, the resulting program must be equivalent to the one with the contracts. See it like code documentation that can help you debug.