在保证，艾菲尔可拆卸元素(Detachable element in ensure, Eiffel)

我怎样才能确保一个元素是我HASH_TABLE，如果是可拆卸的？

Current = HASH_TABLE[ARRAYED_SET[G], G]

add_edge (src: G; dst: G)
do
    if attached Current.at(src) as edges then
        edges.put(dst)
    end
ensure
    in: Current.at (src).has (dst)
end

Answer 1:

你有没有尝试：

add_edge (src: G; dst: G)
do
    if attached Current.at(src) as edges then
        edges.put(dst)
    end
ensure
    in: attached Current.at (src) as edges implies edges.has (dst)
end

文章来源: Detachable element in ensure, Eiffel