estudio does not check `require` when it should?

Question

Eiffel Studio seems to pass through my requirements even if I have them enabled on project settings. And as far as I remember I was able some time to put a break point into the requirements...

I don't understand what I'am missing here, as you can see in my example, the requirement passes through as I have the same condition on the code and it goes into (attached {POWER_DEVICE} a_csv.device as l_dev).

Answer 1

A general rule for inherited assertions is the following:

• preconditions can be only relaxed;
• postconditions can be only strengthened.

In the particular example the effective precondition is

    True
or else
    valid_csv (a_csv) and then attached {POWER_DEVICE} a_csv.device

This is reflected by the keywords require at the beginning and require else in the middle of the combined precondition in the flat form of the feature. The expression True is inherited. This is the precondition of the feature in the parent.

A possible solution is to move valid_csv (a_csv) to the parent feature, and redefine valid_csv in the descendant. If valid_csv is common for all calls, but the second test varies across descendants, it might be better to introduce a new feature is_known and have 2 precondition subclauses in the parent:

is_valid_csv: is_valid_csv (a_csv)
is_known_csv: is_known_csv (a_csv)

The implementation of is_known_csv in the class POWER_CSV_PROCESSOR would be

is_known_csv (a_csv: ...)
    do
        Result := attached {POWER_DEVICE} a_csv.device
    end

and the precondition of feature process in POWER_CSV_PROCESSOR would be empty.

The caller would then do something like

if processor.is_known_csv (csv) then
    processor.process (csv)
end