确保中的可拆卸元素，埃菲尔答案

【问题标题】：Detachable element in ensure, Eiffel确保中的可拆卸元素，埃菲尔
【发布时间】：2014-01-05 15:12:47
【问题描述】：

如果一个元素是可拆卸的，我如何确保它在我的 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

【问题讨论】：

标签： hashtable detach eiffel

【解决方案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

【讨论】：

更改后置条件以使用 'implies' 而不是 'and then'：in: attach at(src) as edges 暗示 edges.has(dst)
我确实认为“附加的 Current.at (src)”是一个有效的后置条件，也应该检查。如果您使用“隐含”而不是“然后”，则“Current.at (src)”为 Void 的事实将在程序之后被视为“当前”的有效状态，当然事实并非如此。所以，这就是为什么“然后”。
如果没有附加 src，则代码是无操作的......然后您应该在前提条件中指定：附加在（src）
真的，对不起。我忘记了 G 不是附加类型。