계약에 의한 설계

3. 주요 개념

"계약에 의한 설계"(DbC)의 핵심 개념은 클라이언트와 공급자 간의 '''계약''' (contract^영어)이다. DbC에서 계약은 클래스의 인스턴스와 해당 메서드 사용에 관한 조건을 형식적으로 명시한 것으로, 클래스 불변 조건, 메서드의 사전 조건 및 사후 조건으로 구성된다.

불변 조건, 사전 조건, 사후 조건은 각각 클래스의 동작을 정의하며, 클라이언트에게 공개된 (생성자를 포함하는) 메서드에 적용된다.

계약은 클라이언트와 공급자에게 발생하는 의무와 이익으로 특징지어진다. 클라이언트 설계자는 클래스 인터페이스로 제시된 사전 조건을 준수할 의무가 발생하는 한편, 사후 조건이 충족될 것을 기대할 수 있다. 반대로 공급자 설계자는 클라이언트가 사전 조건을 충족하여 클래스를 사용할 것을 기대할 수 있는 한편, 사후 조건을 준수할 의무가 발생한다. 이러한 클라이언트와 공급자 양측에 발생하는 의무와, 의무를 지켰을 때 보장된 상태를 얻을 수 있는 이익이 나타나는 점에서, 프로그래밍에서의 "계약"과 일반적인 의미의 계약 간의 유사성을 찾을 수 있다.

명시는 미리 기술해 둠으로써, 구현자는 해당 명시에 따라 프로그램을 작성할 수 있다. 일반적으로 명시는 정적인 기술이며, 반드시 프로그램 동작 시 의미를 갖는 것은 아니지만, DbC를 지원하는 프로그래밍 언어에서는 프로그램 실행 시 명시 위반 여부를 감시할 수 있다. 실행 시 명시 위반 감시와 관련하여, 예외 기구를 이용하여, 실행 시 명시 위반을 예외로 클라이언트가 처리하도록 할 수 있다.

클래스 A가 클래스 B에 관한 엔티티 (지역 변수 정의 및 메서드 호출)의 기술을 포함하는 경우, B는 A에 대한 공급자, A는 B에 대한 클라이언트가 된다. 클라이언트와 공급자는 동일 클래스여도 되며, 예를 들어 this를 통한 메서드 호출이 해당한다.

3. 1. 계약의 구성 요소

• 계약은 무엇을 예상하는가? (전제 조건)
• 계약은 무엇을 보장하는가? (사후 조건)
• 계약은 무엇을 유지하는가? (클래스 불변식)

• 허용 가능한 입력 값 또는 유형 및 해당 의미
• 반환 값 또는 유형 및 해당 의미
• 발생할 수 있는 오류 및 예외 조건, 값 또는 유형 및 해당 의미
• 부작용
• 전제 조건
• 사후 조건
• 불변식
• (드물게) 사용된 시간 또는 공간에 대한 성능 보장

• 클라이언트가 공급자를 호출하기 전 클래스 불변식 AND 전제 조건이 참이면, 서비스 완료 후 불변식 AND 사후 조건이 참이 된다.
• 소프트웨어 모듈은 공급자 호출 시 공급자의 전제 조건을 위반하면 안 된다.

3. 2. 의무와 이익

• 공급자는 특정 제품을 제공해야 할 의무가 있으며, 고객이 수수료를 지불했다는 것을 기대할 이익(권리)이 있다.
• 고객은 수수료를 지불해야 할 의무가 있으며, 제품을 받을 이익(권리)이 있다.
• 양 당사자는 모든 계약에 적용되는 법률 및 규정과 같은 특정 의무를 충족해야 한다.

• 메서드를 호출하는 클라이언트는 메서드의 전제 조건을 보장해야 할 의무가 있다. 이는 공급자(메서드)의 이익이 된다. (전제 조건 외의 경우를 처리할 필요가 없기 때문)
• 메서드는 종료 시 사후 조건을 보장해야 할 의무가 있다. 이는 클라이언트의 이익이 된다.
• 메서드는 클래스 불변식을 유지해야 한다.

• 계약은 무엇을 예상하는가? (전제 조건)
• 계약은 무엇을 보장하는가? (사후 조건)
• 계약은 무엇을 유지하는가? (불변식)

• 허용 가능한 입력 값 및 의미
• 반환 값 및 의미
• 발생 가능한 오류 및 예외 조건 값 및 의미
• 부작용
• 전제 조건
• 사후 조건
• 불변식
• (드물게) 성능 보장

• 클래스 불변식 AND 전제 조건이 클라이언트가 공급자를 호출하기 전에 참이면, 서비스 완료 후 불변식 AND 사후 조건이 참이 된다.
• 공급자를 호출할 때 소프트웨어 모듈은 공급자의 전제 조건을 위반해서는 안 된다.

4. 계약과 예외 처리

「계약에 의한 설계」(DbC)의 핵심은 클라이언트와 공급자^[21] 간의 '''계약''' (contract^영어)이다. DbC에서 계약은 클래스^[22]의 인스턴스^[23]와 해당 메서드^[24] 사용 조건을 형식적으로 명시한 것이다. 이는 클래스 불변 조건, 메서드의 사전 조건 및 사후 조건으로 구성된다.

불변 조건, 사전 조건, 사후 조건은 클래스 동작을 정의하며, 클라이언트에게 공개된 (생성자를 포함하는) 메서드에 적용된다.

계약은 클라이언트와 공급자에게 발생하는 의무와 이익으로 특징지어진다.

• 클라이언트 설계자는 클래스 인터페이스로 제시된 사전 조건을 준수할 의무가 있고, 사후 조건이 충족될 것을 기대할 수 있다.
• 공급자 설계자는 클라이언트가 사전 조건을 충족하여 클래스를 사용할 것을 기대할 수 있고, 사후 조건을 준수할 의무가 있다.

• 메서드 성공: 불변 조건을 포함하는 메서드의 사후 조건을 만족시키고 호출원에 제어를 반환해야 한다.

• 메서드 실패: 시스템 상태를 메서드 실행 전 상태로 되돌리고, 클라이언트에 예외 발생을 알려야 한다. (예: DB 트랜잭션 에러 시, 공급자는 트랜잭션 롤백 후 DB 조작 실패를 클라이언트에 알림)

5. 계약의 상속

클래스는 개방/폐쇄 원칙에 따라 설계되어야 한다. 즉, 클래스 인터페이스 사양은 안정적이고 클라이언트 입장에서의 동작은 바뀌지 않아야 하는 동시에, 미래의 기능 추가나 사양 변경을 수용할 수 있어야 한다. 후자의 모듈 개방성을 실현하기 위한 방법 중 하나로 클래스의 상속이 있다。

"계약에 의한 설계"(DbC)에서는 클래스 인스턴스의 추상적인 동작(behaviour^영어)을 불변 조건과 각 메서드의 사전 조건 및 사후 조건으로 정의한다^[28]。DbC에 따라 프로그래밍할 때, 클라이언트는 사전 조건을 만족하면 사후 조건을 만족하는 상태를 얻을 수 있다고 기대하며 공급자 클래스의 엔티티를 기술하게 된다. 한편, 다형성 때문에 클라이언트가 기술한 공급자 클래스 자체가 항상 구현을 제공하는 것은 아니며, 프로그램 실행 시에는 동적 바인딩된 서브클래스^[29]의 인스턴스 구현이 사용될 수 있다。

서브클래스 인스턴스의 동작은 서브클래스 자신의 불변 조건 및 각 메서드의 사전 조건과 사후 조건에 의해 정의되지만, 한편 서브클래스 인스턴스는 클라이언트와 상속 원본 슈퍼클래스^[30]의 계약에 구속되어 슈퍼클래스 인스턴스로서도 동작해야 한다(리스코프 치환 원칙). 따라서 클라이언트와 상속 원본 슈퍼클래스 간의 계약을 실현하기 위해, 서브클래스는 슈퍼클래스의 불변 조건을 항상 만족해야 하며(따라서 서브클래스의 불변 조건은 자신의 불변 조건과 모든 슈퍼클래스의 불변 조건의 논리곱이 된다), 또한 서브클래스의 사전 조건은 슈퍼클래스의 사전 조건보다 약하게(또는 같게), 서브클래스의 사후 조건은 슈퍼클래스의 사후 조건보다 강하게(또는 같게) 해야 한다。

여기서 "조건 A가 조건 B보다 '''강하다'''"는 것은 A가 성립하면 B도 반드시 성립하고, 반대는 성립하지 않는 것을 말한다。예를 들어 실수 x에 대해 x > 2 가 성립하면 항상 x > 0 이 성립하지만, 반대는 성립하지 않는다. 이 경우 실수 x에 대한 조건 x > 2는 조건 x > 0보다 강하다고 할 수 있다. 다른 한편 "조건 A가 조건 B보다 '''약하다'''"는 것은 B가 A보다 강하다는 것을 의미한다。

6. 프로그래밍 언어 지원

계약에 의한 설계를 기본적으로 구현하는 언어는 다음과 같다.

• 에이다 2012
• Ciao
• 클로저
• 코브라
• D^[10]
• Dafny
• 에펠
• 포트리스
• 코틀린
• 머큐리
• 옥시젠 (이전에는 Chrome 및 Delphi Prism^[11])
• 래킷 (고차 계약을 포함하며, 계약 위반 시 책임 당사자를 지목하고 정확한 설명을 제공해야 함^[12])
• 세더
• 스칼라^[13][14]
• SPARK (정적 분석을 통한 에이다 프로그램)
• Vala
• VDM

6. 1. 네이티브 지원

또한, 공통 리스프 객체 시스템의 표준 메서드 조합에는 `:before`, `:after` 및 `:around` 메서드 한정자가 있어 보조 메서드로서의 계약 작성을 비롯한 다양한 용도로 활용할 수 있다.

7. 대한민국에서의 적용과 발전

(이전 출력이 비어있으므로, 수정할 내용이 없습니다. 원본 소스와 요약 정보가 제공되어야 '대한민국에서의 적용과 발전' 섹션 내용을 작성하고 검토할 수 있습니다.)

참조

_[1] 서적 Design by Contract Interactive Software Engineering Inc. 1986
_[2] 서적 Design by Contract Prentice Hall 1991
_[3] 간행물 Applying "Design by Contract" http://se.ethz.ch/~m[...] 1992-10
_[4] 웹사이트 United States Patent and Trademark Office registration for "DESIGN BY CONTRACT" https://web.archive.[...] 2009-06-22
_[5] 웹사이트 United States Patent and Trademark Office registration for the graphic design with words "Design by Contract" https://web.archive.[...] 2009-06-22
_[6] 웹사이트 Trademark Status & Document Retrieval - 78342277 http://tarr.uspto.go[...]
_[7] 웹사이트 Trademark Status & Document Retrieval - 78342308 http://tarr.uspto.go[...]
_[8] 웹사이트 Assertions in Managed Code 2016-11-15
_[9] 문서 Official Python Docs, assert statement https://docs.python.[...]
_[10] 웹사이트 D Programming Language, Contract Programming http://dlang.org/con[...] Digital Mars 2014-11-10
_[11] 웹사이트 Write Cleaner, Higher Quality Code with Class Contracts in Delphi Prism https://web.archive.[...] Embarcadero Technologies 2016-01-20
_[12] 논문 Contracts for Higher-Order Functions http://www.eecs.nort[...]
_[13] 웹사이트 Scala Standard Library Docs - Assertions https://www.scala-la[...] EPFL 2019-05-24
_[14] 문서 Strong typing https://www.scala-la[...]
_[15] 기타
_[16] 기타
_[17] 웹사이트 Some contributions https://bertrandmeye[...] 2021-02-26
_[18] 서적 Design by Contract Interactive Software Engineering Inc. 1986
_[19] 서적 Design by Contract Prentice Hall 1991
_[20] 간행물 Applying "Design by Contract" http://se.ethz.ch/~m[...] 1992-10
_[21] 기타
_[22] 기타
_[23] 기타
_[24] 기타
_[25] 기타
_[26] 기타
_[27] 기타
_[28] 기타
_[29] 기타
_[30] 기타