Обеспечить оговорку в Эйфелевой

Question

Я выполняю задание в Eiffel, и у меня возникают проблемы с реализацией моего пункта обеспечения. Есть ли какой-то особый синтаксис, который нужно включить в переменную или функцию?

Это мой код на данный момент для моей функции "положить"

    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(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' вставляет элемент (ключ, значение) в список. Функция 'has' проверяет, содержит ли список (ключ-значение) пару.

Любая помощь будет оценена.

Answer 1

Это может быть просто

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

Но есть еще несколько комментариев к коду:

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 нет необходимости иметь выделенные геттеры, поэтому обычно код list.item.getkey похоже list.item.key,
6. Вы можете превентивно выйти из цикла, вызвав list.finish который перемещает курсор к последнему элементу списка, когда требуемый элемент найден. Затем после list.forth условие выхода из цикла выполняется, и цикл завершается.