@EnsuresNonNullIf 주석은 "조건부 사후 조건 충족 안됨"-warning을 나타냅니다.

Question

나는 @Nullable 및 @NonNull의 올바른 사용을 확인하기 위해 검사기 프레임 워크와 주석을 사용하고 있습니다. 맵과 비슷한 클래스 에서 Java 사양은 get(…) -methods가 맵에 해당 키에 대한 항목이 없을 때 null을 반환한다고 명시합니다. 따라서 메서드는 @Nullable - 주석이 있습니다. 그러나 contains(…)이 true을 반환하면 get(…)이 null을 반환하지 않는다는 것을 보증하고 싶습니다.

조건부 NonNull을 어떻게 지정합니까?

다음과 같이 지금까지 내가 아는 한, 당신은, @EnsuresNonNullIf와 contains(…) -methods을 주석하여이 작업을 수행 할 수 있습니다 :

@Pure 
@EnsuresNonNullIf(expression = {"get(#1)", "getMatchingStoredKey(#1)", "getStrict(#1)", "lookup(#1)"}, result = true) 
public boolean containsKeyStrict(final @Nullable Class<? extends TKeyClass> key) { 
    return super.containsKey(key); 
} 

@Pure 
public @Nullable TValue getStrict(final @Nullable Class<? extends TKeyClass> key) { 
    Return super. gets (key); 
} 

그러나,이 경고가 발생

:

the conditional postcondition about 'this.getStrict(key)' at this return statement is not satisfied 

을 어떻게해야 이 "사후 조건을 만족하지 못함"- 경고를 풀어 주시겠습니까?

이

내 환경 :

• 메이븐 : 3.0.4
• 자바 : 1.7.0_25 (오라클)
• 검사기 프레임 워크 1.7.0 (Maven 플러그인을 통해이)

This Gist을 보여줍니다 문제.

---

1)지도의 기능을 확장하여 "비슷한"키가있는 항목을 검색합니다.

Answer 1

지금까지 나의 유일한 해결책은 @EnsuresNonNullIf- 어노테이션을 SuppersWarnings("nullness")과 결합하는 것입니다. 예컨대 : 범위를

@SuppressWarnings("nullness") 
@EnsuresNonNullIf(expression = {"get(#1)", "getMatchingStoredKey(#1)", "getStrict(#1)", "lookup(#1)"}, result = true) 
public boolean containsKeyStrict(final @Nullable Class<? extends TKeyClass> key) { 
    return super.containsKey(key); 
} 

@SuppressWarnings 당신이 메서드에 구현을 위임 할 수 없습니다 주석 @EnsuresNonNullIf.

Answer 2

당신이 지도 당신이 옳은 것 그 키

에 대한 항목을 포함하지 않는 경우 (...) null를 돌려 -methods받을

자바 사양 상태가 말할 때 부분적으로 오른쪽, check here, javadoc 상태,

null이 값을 허용하는 경우 null의 반환 값은가 아닙니다.은 반드시 맵에 키 매핑이 없음을 나타냅니다. 지도가 명시 적으로 키를 null로 매핑 할 수도 있습니다. containsKey 연산은이 두 가지 경우를 구별하는 데 사용될 수 있습니다.당신은 null 값에 키를 매핑하는 경우, 귀하의 방법 containsKeyStrict이 true를 반환 할 수 있으며, 여전히 당신의 방법 getStrict이 null을 반환, 즉

은 해당 키에 대한하지만 값 때문에 값이 없습니다 때문이 그 열쇠는 정확히 null입니다.

은지도에 null 값의 삽입을 방지하기 위해 당신은 null 값 (또는 키)를 허용하지 않는 HashTable을 사용할 수 있습니다, 또는 당신이 put 방법에 유효성 검사를 추가 할 수 있습니다, 당신이 필요로하는 행동의 종류를 적용하려면 행운을 빕니다.