The curious case of the lost contract

[Rosivaldo Fernandes Alves]

Hi all.

Please consider the classes below. SPEC1 specifies (and "implements")
the feature foo. SPEC2 inherits SPEC1 and redefines foo in order to
strengthen its contract (it keeps the implementation, but don't mind:
the contract is what counts).

Then IMPL1 inherits SPEC1 and redefines foo's implementation. Finally,
IMPL2 inherits both SPEC2 and IMPL1, undefining {SPEC2}.foo and keeping
{IMPL1}.foo implementation.

Now, within {APPLICATION}.make, the call to obj2.foo (which calls
{IMPL2}.foo) fails to check the contract inherited from {SPEC2}.foo.

This seems weird. Undefining should discard the implementation, never
the contract of the undefined feature. Should it be counted as a bug?

Best regards,

Rosivaldo.


class
APPLICATION

create
make

feature {NONE}

make
local
obj2: IMPL2
do
create obj2
obj2.foo -- Should raise a post-condition violation
(this_will_be_overlooked: Current /= Current), but it does not.
end

end


deferred class
SPEC1

feature

foo
do
ensure
whatever: is_equal (Current)
end

end


deferred class
SPEC2

inherit
SPEC1
redefine
foo
end

feature

foo
do
Precursor {SPEC1}
ensure then
this_will_be_overlooked: Current /= Current
end

end


class
IMPL1

inherit
SPEC1
redefine
foo
end

feature

foo
do
print ("Do something.%N")
end

end


class
IMPL2

inherit
SPEC2
undefine
foo
end
IMPL1

end

[Alexander Kogtenkov]

Hi Rosivaldo,

 

Some further investigation may be needed, but after a quick look it seems to be a bug. Thank you for the report.

 

Best regards,

Alexander Kogtenkov

 

 

Rosivaldo Fernandes Alves <rosiva...@gmail.com>:

[Rosivaldo Fernandes Alves]

Hi Alexander.

Thank *you* for your attention.

Best regards,

Rosivaldo.

Em 19/01/2021 15:21, 'Alexander Kogtenkov' via Eiffel Users escreveu:
> Hi Rosivaldo,
> Some further investigation may be needed, but after a quick look it
> seems to be a bug. Thank you for the report.
> Best regards,
> Alexander Kogtenkov
>

> (...)