JML이 null이 아닙니다.

Question

JML 관련 질문이 있습니다. array_의 요소에 관한

protected /*@ non_null */ Object[] array_; 

로 선언

/*@ invariant array_ != null; */ 

과의 차이는 무엇입니까? 각각의 경우에 어떤 속성이 유지됩니까?

미리 감사드립니다.

Answer 1

에 대해 array_? 각각의 경우에 어떤 속성이 유지됩니까?

요소에 대해 언급하지 않았습니다. 보장되는 유일한 점은 array_ 참조가 null이 아니라는 것입니다.

참고

Object[] array = null; 

내지 인스턴스 차이

Object[] array_ = { null }; 

또는

Object[] array_ = { }; 

후자 두 허용 될 때 첫 번째 라인은 불변 위배뿐만 array_은 실제 배열을 가리킬 것입니다 (비록이 배열은 단지 cont null 요소 또는 전혀 요소 없음).

---

또 다른 차이점은 non_null 프라그를 사용하는 경우 array_ != null 프로그램 전반에 걸쳐 모든 제어 지점에서 보유해야하는 동안 invariant array_ != null; 접근 방식, array_ != null 만, 각각의 방법 후 이전에 개최해야한다는 것입니다.