iContract : Design by Contract in Java

자신의 것을 포함하여 사용하는 모든 Java 클래스가 약속에 부응한다면 좋지 않을까요? 실제로 주어진 클래스가 무엇을 약속하는지 정확히 알고 있다면 좋지 않을까요? 동의하는 경우 계속 읽으십시오 .-- Design by Contract 및 iContract가 구출됩니다.

참고 : 이 기사의 예제에 대한 코드 소스는 Resources에서 다운로드 할 수 있습니다.

계약에 의한 설계

DBC (Design by Contract) 소프트웨어 개발 기술은 시스템의 모든 구성 요소가 기대에 부응하도록 보장함으로써 고품질 소프트웨어를 보장합니다. DBC를 사용하는 개발자 는 구성 요소 인터페이스의 일부로 구성 요소 계약 을 지정합니다 . 계약은 해당 구성 요소가 클라이언트에게 기대하는 것과 클라이언트가 기대할 수있는 것을 지정합니다.

Bertrand Meyer는 자신의 Eiffel 프로그래밍 언어의 일부로 DBC를 개발했습니다. 기원에 관계없이 DBC는 Java를 포함한 모든 프로그래밍 언어에 대한 귀중한 설계 기술입니다.

DBC의 핵심은 어설 션 ( 소프트웨어 시스템의 상태에 대한 부울 표현 )의 개념입니다 . 런타임에 시스템 실행 중 특정 체크 포인트에서 어설 션을 평가합니다. 유효한 소프트웨어 시스템에서는 모든 어설 션이 참으로 평가됩니다. 즉, 어떤 주장이 거짓으로 평가되면 소프트웨어 시스템이 유효하지 않거나 손상된 것으로 간주합니다.

DBC의 중심 개념은 #assertC 및 C ++ 프로그래밍 언어 의 매크로와 다소 관련이 있습니다. 그러나 DBC는 주장을 수백만 수준 더 끌어 올립니다.

DBC에서는 세 가지 다른 종류의 표현을 식별합니다.

  • 전제 조건
  • 사후 조건
  • 불변

각각을 더 자세히 살펴 보겠습니다.

전제 조건

전제 조건은 메서드를 실행하기 전에 유지해야하는 조건을 지정합니다. 따라서 메서드가 실행되기 직전에 평가됩니다. 전제 조건에는 시스템 상태와 메서드에 전달 된 인수가 포함됩니다.

전제 조건은 소프트웨어 구성 요소의 클라이언트가 구성 요소의 특정 메서드를 호출하기 전에 충족해야하는 의무를 지정합니다. 전제 조건이 실패하면 소프트웨어 구성 요소의 클라이언트에 버그가있는 것입니다.

사후 조건

반대로 사후 조건은 메서드가 완료된 후 유지되어야하는 조건을 지정합니다. 결과적으로 사후 조건은 메서드가 완료된 후에 실행됩니다. 사후 조건에는 이전 시스템 상태, 새 시스템 상태, 메서드 인수 및 메서드의 반환 값이 포함됩니다.

사후 조건은 소프트웨어 구성 요소가 클라이언트에 대한 보장을 지정합니다. 사후 조건을 위반하면 소프트웨어 구성 요소에 버그가 있습니다.

불변

불변은 클라이언트가 개체의 메서드를 호출 할 수있을 때마다 유지해야하는 조건을 지정합니다. 불변은 클래스 정의의 일부로 정의됩니다. 실제로 불변성은 클래스 인스턴스의 메서드가 실행되기 전후에 언제든지 평가됩니다. 불변의 위반은 클라이언트 또는 소프트웨어 구성 요소의 버그를 나타낼 수 있습니다.

어설 션, 상속 및 인터페이스

클래스 및 해당 메서드에 대해 지정된 모든 어설 션은 모든 하위 클래스에도 적용됩니다. 인터페이스에 대한 어설 션을 지정할 수도 있습니다. 따라서 인터페이스의 모든 어설 션은 인터페이스를 구현하는 모든 클래스에 대해 유지되어야합니다.

iContract-Java와 DBC

지금까지 우리는 일반적으로 DBC에 대해 이야기했습니다. 지금 쯤이면 내가 무슨 말을하는지 알 수 있겠지만, DBC를 처음 접하는 사람이라면 여전히 약간 안개가 낀다.

이 섹션에서는 상황이 더 구체적이 될 것입니다. Reto Kamer가 개발 한 iContract는 이전에 논의한 DBC 어설 션을 지정할 수있는 구조를 Java에 추가합니다.

iContract 기본 사항

iContract는 Java 용 전 처리기입니다. 이를 사용하려면 먼저 iContract로 Java 코드를 처리하여 데코 레이팅 된 Java 파일 세트를 생성합니다. 그런 다음 Java 컴파일러를 사용하여 평소와 같이 데코 레이팅 된 Java 코드를 컴파일합니다.

Java 코드의 모든 iContract 지시문은 Javadoc 지시문과 마찬가지로 클래스 및 메소드 주석에 있습니다. 이러한 방식으로 iContract는 기존 Java 코드와의 완전한 하위 호환성을 보장하며, iContract 어설 션없이 항상 Java 코드를 직접 컴파일 할 수 있습니다.

일반적인 프로그램 라이프 사이클에서는 시스템을 개발 환경에서 테스트 환경으로 이동 한 다음 프로덕션 환경으로 이동합니다. 개발 환경에서는 iContract 어설 션으로 코드를 계측하고 실행합니다. 이렇게하면 새로 도입 된 버그를 조기에 발견 할 수 있습니다. 테스트 환경에서 여전히 대량의 어설 션을 활성화하고 싶을 수 있지만 성능이 중요한 클래스에서 제거해야합니다. 때로는 프로덕션 환경에서 일부 어설 션을 사용하도록 유지하는 것이 합리적이지만 시스템 성능에 절대로 중요하지 않은 클래스에서만 가능합니다. iContract를 사용하면 어설 션으로 계측하려는 클래스를 명시 적으로 선택할 수 있습니다.

전제 조건

iContract에서는 @pre지시문을 사용하여 메소드 헤더에 전제 조건을 배치 합니다. 예를 들면 다음과 같습니다.

/ ** * @pre f> = 0.0 * / public float sqrt (float f) {...} 

예제 전제 조건은 ffunction 의 인수 sqrt()가 0보다 크거나 같은지 확인합니다. 해당 방법을 사용하는 고객은 해당 전제 조건을 준수 할 책임이 있습니다. 그렇지 않은 경우 구현자인 우리 sqrt()는 결과에 대해 책임을지지 않습니다.

뒤의 표현식 @pre은 Java 부울 표현식입니다.

사후 조건

사후 조건은 자신이 속한 메서드의 헤더 주석에 마찬가지로 추가됩니다. iContract에서 @post지시문은 사후 조건을 정의합니다.

/ ** * @pre f> = 0.0 * @post Math.abs ((return * return)-f) <0.001 * / public float sqrt (float f) {...} 

이 예에서는 sqrt()메서드 f가 특정 오차 한계 (+/- 0.001) 내에서의 제곱근을 계산 하도록하는 사후 조건을 추가했습니다 .

iContract는 사후 조건에 대한 몇 가지 특정 표기법을 도입합니다. 우선 return메서드의 반환 값을 나타냅니다. 런타임시에는 메서드의 반환 값으로 대체됩니다.

사후 조건 내 에서 메서드 실행 하기 전과 이후에 @pre연산자 와 함께 iContract에서 지원되는 인수 값을 구별해야하는 경우가 종종 있습니다 . @pre사후 조건의 식에 추가 하면 메서드가 실행되기 전에 시스템 상태를 기반으로 평가됩니다.

/ ** * 컬렉션에 요소를 추가합니다. * * @post c.size () = [email protected] () + 1 * @post c.contains (o) * / public void append (Collection c, Object o) {...}

위 코드에서 첫 번째 사후 조건은 요소를 추가 할 때 컬렉션의 크기가 1 씩 커야 함을 지정합니다. 표현식 [email protected]은 메서드 c실행 전 컬렉션을 나타냅니다 append.

불변

iContract를 사용하면 클래스 정의의 헤더 주석에 불변을 지정할 수 있습니다.

/ ** * PositiveInteger는 양수가 보장되는 정수입니다. * * @inv intValue ()> 0 * / class PositiveInteger extends Integer {...}

이 예에서 불변성은 PositiveInteger의 값이 항상 0보다 크거나 같음을 보장합니다 . 해당 어설 션은 해당 클래스의 메서드 실행 전후에 확인됩니다.

Object Constraint Language (OCL)

Although the assertion expressions in iContract are valid Java expressions, they are modeled after a subset of the Object Constraints Language (OCL). OCL is one of the standards maintained and coordinated by the Object Management Group, or OMG. (OMG takes care of CORBA and related stuff, in case you miss the connection.) OCL was intended to specify constraints within object modeling tools that support the Unified Modeling Language (UML), another standard guarded by OMG.

Because the iContract expressions language is modeled after OCL, it provides some advanced logical operators beyond Java's own logic operators.

Quantifiers: forall and exists

iContract supports forall and exists quantifiers. The forall quantifier specifies that a condition should hold true for every element in a collection:

/* * @invariant forall IEmployee e in getEmployees() | * getRooms().contains(e.getOffice()) */ 

The above invariant specifies that every employee returned by getEmployees() has an office in the collection of rooms returned by getRooms(). Except for the forall keyword, the syntax is the same as that of an exists expression.

Here is an example using exists:

/** * @post exists IRoom r in getRooms() | r.isAvailable() */ 

That postcondition specifies that after the associated method executes, the collection returned by getRooms() will contain at least one available room. The exists proceeds the Java type of the collection element -- IRoom in the example. r is a variable that refers to any element in the collection. The in keyword is followed by an expression that returns a collection (Enumeration, Array, or Collection). That expression is followed by a vertical bar, followed by a condition involving the element variable, r in the example. Employ the exists quantifier when a condition must hold true for at least one element in a collection.

Both forall and exists can be applied to different kinds of Java collections. They support Enumerations, Arrays, and Collections.

Implications: implies

iContract provides the implies operator to specify constraints of the form, "If A holds, then B must hold as well." We say, "A implies B." Example:

/** * @invariant getRooms().isEmpty() implies getEmployees().isEmpty() // no rooms, no employees */ 

That invariant expresses that when the getRooms() collection is empty, the getEmployees() collection must be empty as well. Note that it does not specify that when getEmployees() is empty, getRooms() must be empty as well.

You can also combine the logical operators just introduced to form complex assertions. Example:

/** * @invariant forall IEmployee e1 in getEmployees() | * forall IEmployee e2 in getEmployees() | * (e1 != e2) implies e1.getOffice() != e2.getOffice() // a single office per employee */ 

Constraints, inheritance, and interfaces

iContract propagates constraints along inheritance and interface implementation relationships between classes and interfaces.

Suppose class B extends class A. Class A defines a set of invariants, preconditions, and postconditions. In that case, the invariants and preconditions of class A apply to class B as well, and methods in class B must satisfy the same postconditions that class A satisfies. You may add more restrictive assertions to class B.

The aforementioned mechanism works for interfaces and implementations as well. Suppose A and B are interfaces and class C implements both. In that case, C is subject to invariants, preconditions, and postconditions of both interfaces, A and B, as well as those defined directly in class C.

Beware of side effects!

iContract will improve the quality of your software by allowing you to catch many possible bugs early on. But you can also shoot yourself in the foot (that is, introduce new bugs) using iContract. That can happen when you invoke functions in your iContract assertions that engender side effects that alter your system's state. That leads to unpredictive behavior because the system will behave differently once you compile your code without iContract instrumentation.

The stack example

Let us take a look at a complete example. I have defined the Stack interface, which defines the familiar operations of my favorite data structure:

/** * @inv !isEmpty() implies top() != null // no null objects are allowed */ public interface Stack { /** * @pre o != null * @post !isEmpty() * @post top() == o */ void push(Object o); /** * @pre !isEmpty() * @post @return == top()@pre */ Object pop(); /** * @pre !isEmpty() */ Object top(); boolean isEmpty(); } 

We provide a simple implementation of the interface:

import java.util.*; /** * @inv isEmpty() implies elements.size() == 0 */ public class StackImpl implements Stack { private final LinkedList elements = new LinkedList(); public void push(Object o) { elements.add(o); } public Object pop() { final Object popped = top(); elements.removeLast(); return popped; } public Object top() { return elements.getLast(); } public boolean isEmpty() { return elements.size() == 0; } } 

As you can see, the Stack implementation does not contain any iContract assertions. Rather, all assertions are made in the interface, meaning that the component contract of the Stack is defined in the interface in its entirety. Just by looking at the Stack interface and its assertions, the Stack's behavior is fully specified.

Now we add a small test program to see iContract in action:

public class StackTest { public static void main(String[] args) { final Stack s = new StackImpl(); s.push("one"); s.pop(); s.push("two"); s.push("three"); s.pop(); s.pop(); s.pop(); // causes an assertion to fail } } 

Next, we run iContract to build the stack example:

java -cp % CLASSPATH %; src; _contract_db; instr com.reliablesystems.iContract.Tool -Z -a -v -minv, pre, post> -b "javac -classpath % CLASSPATH %; src"-c "javac -classpath % CLASSPATH %; instr "> -n"javac -classpath % CLASSPATH %; _ contract_db; instr "-oinstr / @ p / @ f. @ e -k_contract_db / @ p src / *. java 

위의 진술은 약간의 설명을 보증합니다.