Ferenc Dajka
Ferenc Dajka

Reputation: 1051

Detachable element in ensure, Eiffel

How can I ensure that an element is in my HASH_TABLE, if it is detachable?

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

Upvotes: 1

Views: 237

Answers (1)

Louis M
Louis M

Reputation: 586

Have you try that:

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

Upvotes: 1

Related Questions