에펠의 절을 확인하십시오

Question

에펠에서 과제를 수행하고 있으며 확실한 규정을 구현하는 데 문제가 있습니다. 변수 또는 함수를 포함해야하는 특수 구문이 있습니까?

이 내 코드는

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. 코드가 ITEM 인 요소를 삽입하면 put의 사후 조건은 list.has (key, value) 대신 across list ... end을 사용해야합니다. 그래서 그것 앞에 단지 has (key, value)이어야하고 그 앞에는 list.이 없어야한다고 생각합니다.
3. 보조 변수 flag을 사용할 시점이 없습니다. 예약 된 변수 Result은 정상적으로 처리됩니다.
4. 에펠의 모든 변수는 기본값으로 초기화되므로 루틴 시작시 0을 flag (또는 false ~ Result 간체 버전)으로 지정할 필요가 없습니다.
5. 일반적으로 에펠에는 전용 getter가 필요하지 않으므로 보통 list.item.getkey 코드는 list.item.key처럼 보입니다.
6. 필요한 요소가 발견되면 커서를 목록의 마지막 항목으로 이동하는 list.finish을 호출하여 루프를 선제 적으로 종료 할 수 있습니다. 그런 다음 list.forth 다음에 루프 종료 조건이 충족되고 루프가 종료됩니다.