Ensure clause in Eiffel

Question

I'm doing an assignment in Eiffel and I'm having trouble implementing my ensure clause. Is there some special syntax you need to include a variable or function?

This is my code at the moment for my 'put' function

    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

This is the code for the 'has' function

    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

The assignment is to implement a map adt via linked list. The 'put' function inserts item(key, value) into the list. The 'has' function checks whether the list contains (key value) pair.

Any help will be greatly appreciated.

Answer 1

It could be just

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

But then there are several other comments on the code:

1. I do not see where the property key /= Void is used. So it looks like it is not required.
2. Given that the code of put inserts elements of type ITEM, the postcondition of put should also use across list ... end instead of list.has (key, value). So I suspect it should be just has (key, value) without list. in front of it.
3. I do not see any point of using an auxiliary variable flag. The reserved variable Result will do just fine.
4. All variables in Eiffel are initialized by the default values, so there is no need to assign 0 to flag (or false to Result in a simplified version) at the beginning of a routine.
5. Usually there is no need to have dedicated getters in Eiffel, so normally the code list.item.getkey looks like list.item.key.
6. One can preemptively exit from the loop by calling list.finish that moves cursor to the last item of the list when a required element is found. Then after list.forth the loop exit condition is satisfied and the loop terminates.