detachable generic to generic in eiffel

Question

I have a feature with post-condition as follow:

checkValue (k: K): detachable V
do
...
end
ensure
some_post_condition:
    checkKey (Result)

And here is prototype of "checkKey":

checkKey (v: V): BOOLEAN

Since "Result" is type of "detachable V", and I try to pass that as parameter to "checkKey " which only accept type of "V" but not "detachable V", thus it cannot compile.

Here is what compile error says:

Argument name: v
Argument position: 1
Formal argument type: Generic #1
Actual argument type: detachable Generic #1

How can I convert detachable Generic to Generic?

Answer 1

There are several options:

1. Change the type of checkValue from detachable V to V.
2. Change the type of the argument of checkKey from V to detachable V.

3. Change the postcondition to read

   • if Result should always be attached

     result_attached: attached Result
     some_post_condition: checkKey (Result)
     

   • if Result may be detachable (in which case it is considered valid):

     some_post_condition: attached Result implies checkKey (Result)