Eiffel中的确保子句

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

任务是通过链表实现一个map adt。'put‘函数将项(键、值)插入到列表中。'has‘函数检查列表是否包含(键值)对。

任何帮助都将不胜感激。

Answer 1

它可能只是

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

但在代码中还有其他几个注释：

1. 我看不到在哪里使用了属性key /= Void。所以看起来put的代码插入ITEM类型的元素不是required.
2. Given，put的后置条件也应该使用across list ... end而不是list.has (key, value)。所以我怀疑它应该只是has (key, value)，前面没有list.，

，

1. ，我不认为使用辅助变量flag有任何意义。保留变量Result会做得很好。
2. Eiffel中的所有变量都是由默认值初始化的，所以不需要在routine.
3. Usually的开头将0赋给flag (或者在简化版本中将false赋给Result )。在Eiffel中不需要有专门的getter，所以通常代码list.item.getkey看起来像是getters可以通过调用list.finish来抢先退出循环，当找到所需的元素时，它会将光标移动到列表的最后一项。然后，在list.forth之后，满足循环退出条件，并且循环终止。