Съемный элемент в обеспечении, Eiffel

Как я могу убедиться, что элемент есть в моей 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
person Ferenc Dajka    schedule 05.01.2014    source источник

Ответы (1)


arrow_upward
1
arrow_downward

Вы пробовали это:

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
person Louis M    schedule 05.01.2014
comment
Измените постусловие, чтобы использовать «подразумевает» вместо «и затем»: - person Zoran Simic; 06.01.2014
comment
Я думаю, что прикрепленный Current.at (src) является действительным пост-условием, и его также следует проверить. Если вы используете подразумевает вместо and then, тот факт, что Current.at (src) является Void, будет считаться допустимым состоянием «Current» после процедуры, и, конечно, это не так. Итак, вот почему и тогда. - person Louis M; 06.01.2014
comment
Код не работает, если src не подключен... тогда вы должны указать в предварительном условии: attach at(src) - person Zoran Simic; 06.01.2014
comment
Верно, извините. Я забыл, что G не является прикрепленным типом. - person Louis M; 06.01.2014