埃菲尔的确保条款

Question

我在 Eiffel 做作业，但在执行我的 ensure 子句时遇到了问题。是否需要一些特殊的语法来包含变量或函数？

这是我的“put”函数的代码

    put(key: K; value: V)
    require

            key /= void
    local
        tmp:ITEM[K,V]
    do

        create tmp.make(key, value)
        list.put_front (tmp)
        count := count + 1
    ensure

    count = old count + 1 and list.has(key, value)
    end

这是'has'函数的代码

    has(key:K; val:V):BOOLEAN
require
    key /= void
local

    flag: INTEGER
    do

    flag := 0
    from
        list.start
    until
        list.exhausted
    loop
        if list.item.getkey = key then
            if list.item.getvalue = val then
                flag := 1
            end
        end
        list.forth
    end
    if flag = 1 then
        Result := true
    else
        Result := false
    end
    ensure
        --???   
end

任务是通过链表实现一个地图adt。 'put' 函数将 item(key, value) 插入到列表中。 'has' 函数检查列表是否包含（键值）对。

任何帮助将不胜感激。

Answer 1

可能只是

Result = across list as c some (c.item.key = key and c.item.value = value) end

但是代码上还有其他几个cmets：

1. 我看不到属性key /= Void 的使用位置。所以看起来不需要。
2. 鉴于put 的代码插入ITEM 类型的元素，put 的后置条件也应该使用across list ... end 而不是list.has (key, value)。所以我怀疑它应该只是has (key, value)，前面没有list.。
3. 我看不出使用辅助变量flag 有任何意义。保留变量 Result 就可以了。
4. Eiffel 中的所有变量均由默认值初始化，因此无需在例程开始时将0 分配给flag（或在简化版本中将false 分配给Result）。
5. 在 Eiffel 中通常不需要专门的 getter，所以通常代码 list.item.getkey 看起来像 list.item.key。
6. 可以通过调用list.finish 在找到所需元素时将光标移动到列表的最后一项来抢先退出循环。然后在list.forth之后循环退出条件得到满足，循环终止。