JML 시작하기

IBM 홈 | 제품 & 서비스 | 고객지원 & 다운로드 | 회원가입


	JML 시작하기

JML 주석으로 자바 프로그램 향상시키기

Level: Intermediate

Joe Verzulli
Consultant
2003년 3월 18일

Java Modeling Language (JML)는 메소드와 클래스에 대한 새로운 사고방식을 가져다주는 세밀한 디자인의 언어이다. 자바 프로그래밍 컨설턴트인 Joe Verzulli는 JML과 이것의 선언적 구조체들을 소개한다.

Java Modeling Language (JML)은 방법을 말하지 않은 채 메소드가 무엇을 수행 할 것인가를 지정하도록 하는 자바 코드에 주석을 추가한다. JML을 이용해서, 우리는 구현과 관계없이 메소드의 의도된 기능을 설명할 수 있다. 이 방식으로 JML은 절차적 사고를 메소드 디자인 단계로 미루는 객체 지향 원리는 확장한다.

JML은 작동을 선언식으로 설명하기 위해 수 많은 구조체들을 도입했다. 여기에는 모델 필드, 한정사(quantifier), 선언용 시각 범위, 전제조건, 후조건, 불변 값, contract 상속, 정상 작동과 예외적 작동용 스팩 등이 포함되어 있다. 이러한 구조체들로 인해 JML은 매우 강력하게 되지만 이들 모두를 이해하려고 하거나 사용할 필요는 없다.

JML 개괄
클래스와 메소드의 목표 작동을 설명하기 위해 JML을 사용하면 전체 개발 프로세스가 훨씬 향상된다. 자바 코드에 모델링 표기를 추가할 때의 이점은 다음과 같다:

코드가 수행하는 것을 더욱 자세하게 설명
효율적인 발견과 버그 정정
애플리케이션이 진화에 따른 버그 감소
잘못 사용된 클래스의 조기 발견
애플리케이션 코드와 언제라도 연결되는 정확한 문서

JML 주석은 언제나 자바 컴포넌트 안에 있다. 따라서 정상적으로 컴파일되는 코드에 영향을 미치지 않는다. 오픈 소스 JML 컴파일러 (참고자료)는 클래스의 실제 작동과 JML 스팩을 비교할 때 사용될 수 있다. JML 컴파일러로 컴파일된 코드는, 코드가 스팩이 정한 것을 수행하지 않을 때, 런타임시 JML 예외를 만든다. 이는 코드에서 버그를 잡을 뿐만 아니라 문서가 코드와 연동된 상태로 있게 된다.

다음 섹션에서는 Jakarta Commons Collection Component (JCCC)의PriorityQueue 인터페이스와 BinaryHeap 클래스를 사용하여 JML의 특징을 설명할 것이다. (참고자료).

필요조건과 책임
이 글의 소스 코드에는 (참고자료) JCCC의 PriorityQueue가 포함되어 있다. PriorityQueue 인터페이스에는 인자의 데이터 타입과 리턴 값을 정의한 메소드 서명이 포함되어있지만 메소드의 작동에 대해서는 설명이 없다. PriorityQueue의 의미를 지정하여 이를 구현하는 모든 클래스가 원하는 방식대로 작동되기를 바란다.

PriorityQueue의 pop() 메소드에 대해 생각해보자. 우선순위 정렬을 위해 pop()에 무엇이 필요할까? 세 가지 기본적인 것이 있다. 우선 pop()은 큐(queue)에 적어도 한 개의 엘리먼트라도 없다면 호출되어서는 안된다. 둘째, 높은 우선순위를 갖고있는 큐의 엘리먼트를 리턴해야한다. 마지막으로, 이것이 리턴하는 엘리먼트를 큐에서 삭제해야 한다.

Listing 1은 첫 번째 필요조건을 나타내는 JML 주석이다:

Listing 1. pop() 메소드 요구사항을 위한 JML 주석



/*@
   @   public normal_behavior
   @     requires ! isEmpty();
   @*/
Object pop() throws NoSuchElementException;

앞서 언급한 것 처럼 JML 주석은 자바 주석 안에 쓰여진다. JML을 포함하고 있는 다중 라인 주석은 /*@로 시작한다. JML은 //@로 시작하는 한 라인의 주석 안에 쓰여질 수도 있다.

public 키워드는 JML과 자바 모두 의미가 같다. public은 JML 스팩이 애플리케이션의 모든 클래스에 보일 수 있음을 나타낸다. Public 스팩은 public 메소드와 member 변수를 의미한다.

normal_behavior 키워드는 이 스팩이 pop()이 예외 없이 정상적으로 리턴하는 경우를 설명한다.

사전, 사후 조건
JML 키워드인 requires는 사전조건(preconditions)에 사용된다. 사전조건(precondition)은 메소드를 호출하기 전에 충족되어져야 할 조건이다.

메소드의 사후조건(postcondition)은 메소드의 책임에 대해 설명한다. 메소드가 리턴하면 사후 조건은 true가 된다. 예제에서, pop()은 가장 높은 우선순위를 지닌 큐의 엘리먼트를 리턴해야 한다. 이 사후조건을 지정하여 JML에 의해 검사받을 수 있도록 하고 싶다. 이를 위해서는 우선순위 큐에 더해진 모든 값들을 지속적으로 트래킹한다. PriorityQueue에 member 변수를 추가하여 큐에 값을 저장하는 방법을 고려할 수도 있다. 하지만 다음과 같은 문제가 있다:

PriorityQueue는 인터페이스이다. 따라서 바이너리 힙, Fibonacci 힙, 캘린터 큐 같은 다른 구현과 호환되어야 한다.PriorityQueue에 대한 JML 주석은 구현에 대해 어떤 해석도 없다.
인터페이스로서 PriorityQueue는 정적 member 변수만 포함할 수 있다.

JML은 모델 필드(model fields) 개념으로 이 문제를 해결한다.

모델 필드(Model Fields)
모델 필드는 member 변수와 같다. 이것은 작동 스팩에 쓰일 수 있다. 다음은 PriorityQueue에 쓰인 모델 필드 선언 예이다:


//@ public model instance JMLObjectBag elementsInQueue;

데이터 타입이 JMLObjectBag인 elementsInQueue라는 모델 필드가 있음을 이 선언은 나타내고 있다. instance 키워드는 필드가 인터페이스에서 선언되더라도 필드의 개별적인 비-정적 카피는 PriorityQueue를 구현하는 클래스들의 각 인스턴스에 위치할 것임을 나타내고 있다. 모든 JML 주석 처럼 elementsInQueue의 선언은 자바 주석에 나타난다.

스팩 vs. 구현
엘리먼트를 저장하기 위해서 bag 을 사용한다는 것은 비효율적인 일이다. 왜냐하면 모든 엘리먼트는 가장 높은 우선순위를 가진 것을 찾기 위해 검사되기 때문이다. 하지만, bag은 구현의 일부가 아닌 스팩의 일부이다. 스팩의 목적은 PriorityQueue의 작동 인터페이스를 설명하는 것이다. 다시말해서 이것은 클라이언트가 의지할 수 있는 외부 작동이라는 뜻이다. PriorityQueue의 구현은 스팩과 같은 결과만 낸다면 좀더 효율적인 접근방식을 사용 할 수 있다. 예를 들어 JCCC에는 어레이에 저장된 바이너리 힙을 사용하여 PriorityQueue를 구현하는 BinaryHeap 클래스가 포함되어 있다.
스팩이 효율적으로 쓰여질 필요가 없더라도 JML 런타임 선언 검사자의 효율성은 중요하다. 왜냐하면 퍼포먼스에 영향을 미치기 때문이다.

elementsInQueue에는 우선순위 큐에 추가된 값이 포함되어 있다. Listing 2는 pop()용 스팩이 elementsInQueue를 어떻게 사용하는지 보여준다:

Listing 2. pop()의 사후조건에 사용된 모델 필드



/*@
   @ public normal_behavior
   @   requires ! isEmpty();
   @   ensures
   @     elementsInQueue.equals(((JMLObjectBag)
   @          \old(elementsInQueue))
   @                        .remove(\result)) &&
   @     \result.equals(\old(peek()));
   @*/
Object pop() throws NoSuchElementException;

ensures 키워드는 pop()이 리턴할 때 충족되어야 하는 사후조건을 가르키고 있다. \result는 JML 키워드로서 pop()에 의해 리턴된 값과 같다. \old()는 JML 함수로서 pop()이 호출되기 전에 이것의 인자가 갖고있었던 값을 리턴한다.

ensures 절에는 두 개의 사후조건이 있다. 첫 번째는 pop()에 의해 리턴된 값이 elementsInQueue에서 제거되었다는 것을 나타낸다. 두 번째는 리턴 값이 peek()에 의해 리턴된 값과 같음을 나타낸다.

클래스 레벨의 불변 값
JML에서 메소드용 사전, 사후 조건을 지정하는 방법을 배웠다. 클래스 레벨의 불변 값도 지정할 수 있다. 클래스 레벨의 불변 값은 클래스의 모든 메소드의 엔트리와 출구 에서 true 이어야 한다.

수량화(Quantification)
pop()의 이전 스팩에서 이것의 리턴 값은 peek()이 리턴하는 값과 동일하다고 말한 바 있다. PriorityQueue에서 peek()의 스팩은 Listing 3에 나타나있다:

Listing 3. peek() 스팩



/*@
   @ public normal_behavior
   @   requires ! isEmpty();
   @   ensures elementsInQueue.has(\result);
   @*/
/*@ pure @*/ Object peek() throws NoSuchElementException;

JML 주석은 큐에 적어도 하나의 엘리먼트가 있을 때 peek()이 호출되어야 한다는 것을 말하고 있다. peek()에 의해 리턴된 값은 elementsInQueue에 있다는 것도 나타내고 있다.

/*@ pure @*/ 주석은 peek()이 순수한 메소드라는 것을 말하고있다. 순수한 메소드(pure method) 란 부작용이 없는 메소드라는 것을 의미한다. JML은 순수 메소드를 사용할 때 선언을 허용한다.

상속
JML 스팩은 인터페이스를 구현하는 서브클래스와 클래스에 의해 상속받는다. JML 키워드인 also는 조상 클래스와 구현되고 있는 인터페이스 에서 상속받은 스팩과 결합한다는 것을 나타내고 있다. 따라서 PriorityQueue 인터페이스의 peek()용 스팩은 BinaryHeap의 peek()에도 적용된다.

Min heap & max heap
peek()스팩에서 한 가지가 빠져있다. 리턴 된 값이 가장 높은 우선순위를 갖고 있다는 것을 나타내지 않는다. JCCC의 PriorityQueue 인터페이스는 min heap과 max heap 용으로 쓰일 수 있다는 것을 의미한다. min heap의 경우 가장 높은 우선순위 엘리먼트는 가장 작은 것이고 반면, max heap의 경우 가장 높은 우선순위 엘리먼트는 가장 큰 것이다. PriorityQueue가 min heap 또는 max heap 중 어떤 것과 함께 사용될지 모르기 때문에, 어떤 엘리먼트가 리턴 될 지를 설명하는 스팩의 일부는 PriorityQueue를 구현하는 클래스로 가야한다.

JCCC 에서, BinaryHeap 클래스는 PriorityQueue를 구현한다. BinaryHeap은 클라이언트가 구조체의 매개변수를 이용하여 min heap 또는 max heap 중에서 작동을 하도록 지정할 수 있다. 우리는 boolean 모델 변수인 isMinimumHeap를 사용하여 BinaryHeap이 min heap 또는 max heap 중 어떤 것으로 작동하는지 설명할 수 있다. BinaryHeap의 peek() 스팩은 isMinimumHeap을 사용한다. (Listing 4)

Listing 4. peek() 스팩



/*@
   @ also
   @   public normal_behavior
   @     requires ! isEmpty();
   @     ensures
   @       (isMinimumHeap ==>
   @           (\forall Object obj;
   @                  elementsInQueue.has(obj);
   @                  compareObjects(\result, obj)
   @                             <= 0)) &&
   @       ((! isMinimumHeap) ==>
   @           (\forall Object obj;
   @                  elementsInQueue.has(obj);
   @                  compareObjects(\result, obj)
   @                             >= 0));
   @*/
public Object peek() throws NoSuchElementException

한정사 추가하기
Listing 4의 사후조건은 두 부분(min heap과 max heap)으로 구성되어 있다. ==> 표시는 "함축(implies)"이라는 의미이다. x ==> y는 y가 true 이거나 x가 false 일 경우 true 이다. min heap의 경우 다음 조건이 적용된다:


(\forall Object obj;
          elementsInQueue.has(obj);
          compareObjects(\result, obj) <= 0)

comparator 추가하기
BinaryHeap 클래스는 엘리먼트들이 두 가지 다른 방식으로 비교될 수 있도록 한다. 한 가지 접근 방식은 Comparable 인터페이스를 사용하여 엘리먼트의 원래 순서에 의존하는 것이다. 다른 접근 방식은 클라이언트가 Comparable 객체를 BinaryHeap 구조체에 전달하도록 하는 것이다. Comparable은 순서정하기(ordering)에 사용될 수 있다. 어쨌든, 모델 필드인 comparator를 사용하여 Comparator 객체를 나타낼 수 있다. peek() 사후 조건에서 compareObjects() 메소드는 클라이언트가 어떤 비교 방식을 채택하든지, 채택한 것을 사용한다.

Listing 5. compareObjects() 메소드



/*@
   @ public normal_behavior
   @   ensures
   @     (comparator == null) ==>
   @         (\result == ((Comparable) a).compareTo(b)) &&
   @     (comparator != null) ==>
   @         (\result == comparator.compare(a, b));
   @
   @ public pure model int compareObjects(Object a, Object b)
   @ {
   @ if (m_comparator == null)
   @     return ((Comparable) a).compareTo(b);
   @ else
   @     return m_comparator.compare(a, b);
   @ }
   @*/

model은 모델 메소드이다. Model method는 스팩에만 사용될 수 있는 JML 메소드이다. 자바 주석에서 선언되며 정식의 자바 구현 코드에는 사용될 수 없다.

BinaryHeap의 클라이언트가 구체적인 Comparator가 사용되기를 요청했다면, m_comparator는 Comparator를 지시한다. 그렇지 않으면 무효가 된다. compareObjects()은 m_comparator의 값을 검사하고 적절한 비교 작동을 사용한다.

모델 필드가 값을 얻는 방법
Listing 4에서 peek()의 사후 조건을 설명했다. 이 사후 조건은 리턴 값이 elementsInQueue 모델 필드에 있는 모든 엘리먼트의 우선순위 보다 크거나 같은 우선순위를 갖고 있음을 확인한다. 다음과 같은 질문이 생길 수 있다. elementsInQueue 같은 모델 필드가 값을 얻는 방법은? 사전조건, 사후조건, 불변 값은 부작용이 없다. 따라서 그들은 모델 필드의 값을 설정할 수 없다.

JML은 represents 절을 사용하여 모델 필드와 구체적 구현 필드를 결합한다. 예를 들어 다음의 represents 절은 isMinimumHeap 모델 필드에 사용된다.


//@ private represents isMinimumHeap <- m_isMinHeap;

모델 필드 isMinimumHeap의 값이 m_isMinHeap의 값과 같다는 것을 나타내고 있다. m_isMinHeap은 BinaryHeap 클래스에 있는 프라이빗 부울 member 필드이다. isMinimumHeap 값이 요청되면 JML은 m_isMinHeap 값을 쓴다.

represents 절은 <-의 오른편에 있는 member 필드에 제한되어 있지 않다:

Listing 6. elementsInQueue 용 represents clause



/*@ private represents elementsInQueue
   @         <- JMLObjectBag.convertFrom(
   @                   Arrays.asList(m_elements)
   @                     .subList(1, m_size + 1));
   @*/

elementsInQueue는 m_elements[]에서의 값과 같다. m_elements[]는 BinaryHeap의 프라이빗 member 변수이다. m_size는 m_elements[]에서 현재 사용되는 엘리먼트의 수 이다. BinaryHeap은 m_elements[0]를 사용하지 않는다. JMLObjectBag.convertFrom()은 List를 JMLObjectBag으로 변환한다. 이것은 elementsInQueue에 필요한 데이터 타입이다.

부작용
Listing 2의 pop()사후조건을 떠올려 본다:


ensures
elementsInQueue.equals(((JMLObjectBag)
             \old(elementsInQueue))
                           .remove(\result)) &&
\result.equals(\old(peek()));

pop()은 elementsInQueue에서 엘리먼트를 제거하는 부작용을 갖고 있다. 하지만 다른 부작용은 없다. 예를 들어, pop()의 구현은 min heap에서 max heap 으로 바꾸기 위해 m_isMinHeap를 변경할 수 있다. 이러한 변경은 정확은 값을 리턴하는 한 런타임 선언 오류를 발생시키지 않는다. 하지만 JML 스팩 전체를 약화시킬 수 있다.

elementsInQueue를 변경하는 것 외에 또 다른 부작용을 일으키지 못하도록 하는 사후 조건을 강화할 수 있다. (Listing 7):

Listing 7. 부작용을 위한 사후조건



ensures
elementsInQueue.equals(((JMLObjectBag)
            \old(elementsInQueue))
                           .remove(\result)) &&
\result.equals(\old(peek())) &&
isMinimumHeap == \old(isMinimumHeap) &&
comparator == \old(comparator);

x == \old(x)의 사후조건을 추가하고 있다. 이러한 접근방식은 결국 스팩을 어지럽게 만들 뿐이다. 또한 유지도 어려워진다.

JML은 메소드의 부작용을 나타내는 보다 나은 방법을 제시한다.

assignable 절
assignable 절은 우리가 pop()용 스팩을 작성할 수 있도록한다. (Listing 8)

Listing 8. assignable 절


/*@
   @ public normal_behavior
   @   requires ! isEmpty();
   @   assignable elementsInQueue;
   @   ensures
   @     elementsInQueue.equals(((JMLObjectBag)
   @          \old(elementsInQueue))
   @                        .remove(\result)) &&
   @     \result.equals(\old(peek()));
   @*/
Object pop() throws NoSuchElementException;

assignable 절에 나와있는 필드만 메소드에 의해 변경될 수 있다.pop()용 assignable 절은 pop()이 elementsInQueue를 변경할 수 있지만 isMinimumHeap 이나 comparator 같은 다른 필드를 변경할 수 없음을 말해주고 있다. pop() 구현이 m_isMinHeap을 변경한다면 에러가 날 것이다.

위치 변경하기
실제로는 다음과 같은 팩터가 true 일 때 메소드가 위치 (loc)를 변경할 수 있다:

loc은 assignable 절에 언급된다.
assignable 절에 언급된 위치는 loc에 의존한다.
loc은 메소드가 실행을 시작하면 할당되지 않는다.
loc은 메소드의 로컬 변수이거나 메소드의 정식 매개변수이다.

마지막 경우는 인자가 assignable 절에 나타나지 않더라도 메소드가 인자를 변경할 수 있다.

foo(Bar obj)가 obj.x = 17을 포함하고 있다면? 호출 함수에 보이도록 변경이 될 수 있다. 하지만 여기에 함정이 있다. assignable 절 규칙에서는, assignable 절에 변수를 언급하지 않고, 메소드가 새 값을 인자에 할당할 수 있다. 하지만 obj.x 같은 인자 필드에 새 값을 할당하는 것을 허용하지 않는다. foo()가 obj.x를 변경해야 한다면 assignable obj.x; 형식의 assignable 절을 가져야 한다.

두 개의 JML 키워드(\nothing & \everything)가 assignable 절에 사용되었다. assignable \nothing을 작성하여 메소드가 부작용을 갖고 있지 않음을 나타낼 수 있다. 이와 비슷하게 assignable \everything을 작성함으로서 메소드가 무엇이든 변경할 수 있음을 나타낼 수 있다. 앞서 언급한 순수 키워드(pure keyword)는 assignable \nothing;에 해당한다.

예외 작동
peek()과 pop() 스팩은 메소드가 호출될 때 큐가 비워져있어야 한다. 실제로 peek()과 pop()은 큐가 비워져 있을 때 호출될 수 있다. 그와 같은 경우 메소드는 NoSuchElementException을 던진다. 이를 위해 스팩을 수정해야 한다. 그리고 JML의 exceptional_behavior 절을 사용한다.

지금 까지 스팩은 public normal_behavior로 시작했다. normal_behavior 키워드는 이러한 스팩들이 메소드가 어떤 예외도 던지지 않는 경우에 대한 스팩임을 뜻한다. public exceptional_behavior 주석은 예외가 던져질 때 작동을 설명하기 위해 사용된다.

Listing 9. exceptional_behavior 주석



/*@
   @ public normal_behavior
   @   requires ! isEmpty();
   @   ensures elementsInQueue.has(\result);
   @ also
   @ public exceptional_behavior
   @   requires isEmpty();
   @   signals (Exception e) e instanceof NoSuchElementException;
   @*/
/*@ pure @*/ Object peek() throws NoSuchElementException;

이 스팩의 첫 번째 부분도 public normal_behavior로 시작한다. public exceptional_behavior로 시작하는 두 번째 부분에서는 예외 작동이 설명된다. normal_behavior 절과 마찬가지로, exceptional_behavior 절은 requires 절을 갖고 있다. requires 절은 signals 절에 나타나있는 예외가 던져지기 위해서 어떤 조건이 true가 되어야 하는지를 나타내고 있다. 위 예제에서, isEmpty()가 true 이면 peek()은 NoSuchElementException을 던진다.

signals 절
signals 절의 일반적 형태는 signals(E e) R; 이다. JML은 signal 절을 다음과 같이 인터프리팅한다. E 타입의 예외가 던져지면 JML은 R이 true 인지를 검사한다. 그렇게 되면 메소드는 스팩을 만족시킨다. R이 false 이면 JML은 exceptional_behavior 스팩이 위반되었음을 나타내며 검사되지 않은 예외를 던진다.

signals 절은 큐가 비었을때 NoSuchElementException이 나와야 함을 요구하고 있다. peek()이 예외를 던지면 JML은 에러로서 이를 잡는다. peek()이 NoSuchElementException 이나 unchecked 예외를 리턴하도록 하고 싶다면, signals 절을 signals (NoSuchElementException e) true;로 변경하면 된다.

큐에 어떤 것이 있고, 이것이 NoSuchElementException을 던질 때peek()이 호출되면, JML 런타임 선언 검사자는 정상 작동 사후조건이 실패했다는 것을 나타내는 unchecked exception을 발생시킨다.

결론
이 글에 대한 상세 설명은 참고자료를 통해 검색하기 바란다.

참고자료