Following system colour scheme Selected dark colour scheme Selected light colour scheme

Python 개선 제안 한국어 번역

PEP 316 – Python을 위한 계약에 의한 프로그래밍

Author:
Terence Way <terry at wayforward.net>
Status:
Deferred
Type:
Standards Track
Created:
02-May-2003
Post-History:

Table of Contents

번역·라이선스 안내

이 비공식 한국어 번역은 원문 Copyright 절의 Public Domain 조건에 따라 제공합니다. 원저자와 공식 원문은 그대로 표시합니다. 수정되지 않은 기준 원문 · 공식 최신판

초록

이 제안서는 Python을 위한 계약에 의한 프로그래밍을 설명합니다. Eiffel의 Design By Contract(tm)는 아마도 프로그래밍 계약을 가장 널리 활용한 사례일 것입니다 [2].

프로그래밍 계약은 클래스와 모듈에 대한 불변 조건 표현식과 함수와 메서드에 대한 사전 조건 및 사후 조건 표현식을 포함하도록 언어를 확장합니다.

이러한 표현식(계약)은 단언(assertion)과 비슷합니다. 즉, 반드시 참이어야 하며 그렇지 않으면 프로그램이 중단되고, 계약에 대한 런타임 검사는 보통 디버깅하는 동안에만 활성화됩니다. 계약은 단순한 단언보다 더 높은 수준이며 보통 문서에 포함됩니다.

동기

Python에는 이미 어서션이 있는데, 왜 계약 같은 것을 지원하려고 언어에 추가 기능을 넣어야 합니까? 가장 좋은 두 가지 이유는 1) 더 좋고 더 정확한 문서화, 그리고 2) 더 쉬운 테스트입니다.

복잡한 모듈과 클래스는 결코 제대로 문서화되지 않는 것 같습니다. 제공된 문서는 프로그래머가 다른 모듈이나 클래스 대신 특정 모듈이나 클래스를 사용하도록 설득하기에는 충분할 수 있지만, 본격적인 디버깅이 시작되면 프로그래머는 거의 항상 소스 코드를 읽어야 합니다.

계약은 doctest 모듈이 보여 준 훌륭한 본보기를 확장합니다 [4]. 문서는 프로그래머가 읽을 수 있으면서도 그 안에 실행 가능한 테스트가 포함되어 있습니다.

계약이 있는 코드는 테스트하기도 더 쉽습니다. 포괄적인 계약은 단위 테스트와 동등합니다 [8]. 테스트는 사전 조건의 전체 범위를 검사하며, 사후 조건이 발동되면 실패합니다. 이론적으로, 올바르게 명세된 함수는 완전히 무작위로 테스트할 수 있습니다.

그렇다면 왜 이것을 언어에 추가해야 합니까? 왜 여러 가지 다른 구현을 두거나, 프로그래머가 각자 자신의 단언을 구현하도록 하지 않습니까? 그 답은 상속에서 계약이 동작하는 방식에 있습니다.

Alice와 Bob이 서로 다른 단언 패키지를 사용한다고 가정해 봅시다. Alice가 단언으로 보호되는 클래스 라이브러리를 만들면, Bob은 Alice의 라이브러리에서 클래스를 파생하면서 사후 조건과 불변 조건이 제대로 검사되기를 기대할 수 없습니다. 두 사람이 같은 단언 패키지를 사용한다면, Bob은 Alice의 메서드를 오버라이드하면서도 여전히 Alice의 계약 단언에 대해 테스트할 수 있습니다. 이러한 단언 시스템이 자리하기에 자연스러운 곳은 언어의 런타임 라이브러리입니다.

명세

모든 모듈이나 클래스의 독스트링에는 키워드 inv와 그 뒤에 오는 콜론(:)으로 시작하는 줄로 구분된 불변 조건 계약을 넣을 수 있습니다. 줄 시작 부분과 콜론 주위의 공백은 무시됩니다. 콜론 바로 뒤에는 같은 줄에 단일 표현식이 오거나, inv 키워드보다 더 들여쓴 다음 줄들에 일련의 표현식이 옵니다. 여기서는 암시적 줄 이어짐과 명시적 줄 이어짐에 관한 일반적인 Python 규칙을 따릅니다. 독스트링에는 불변 조건 계약이 몇 개든 들어갈 수 있습니다.

몇 가지 예는 다음과 같습니다.:

# state enumeration
START, CONNECTING, CONNECTED, CLOSING, CLOSED = range(5)

class conn:

    """A network connection

    inv: self.state in [START, CLOSED,       # closed states
                        CONNECTING, CLOSING, # transition states
                        CONNECTED]

    inv: 0 <= self.seqno < 256
    """

class circbuf:

    """A circular buffer.

    inv:
        # there can be from 0 to max items on the buffer
        0 <= self.len <= len(self.buf)

        # g is a valid index into buf
        0 <= self.g < len(self.buf)

        # p is also a valid index into buf
        0 <= self.p < len(self.buf)

        # there are len items between get and put
        (self.p - self.g) % len(self.buf) == \
              self.len % len(self.buf)
    """

모듈 불변 조건은 모듈이 로드된 후, 그리고 모듈 안의 모든 공개 함수에 진입할 때와 빠져나올 때 참이어야 합니다.

클래스 불변 조건은 __init__ 함수가 반환된 후, __del__ 함수에 진입할 때, 그리고 클래스의 다른 모든 공개 메서드에 진입할 때와 빠져나올 때 참이어야 합니다. 클래스 불변 조건은 인스턴스 변수에 접근할 때 self 변수를 사용해야 합니다.

메서드나 함수는 이름이 밑줄(_)로 시작하지 않으면 공개 메서드나 함수입니다. 이름이 ‘__’(밑줄 두 개)로 시작하고 끝나는 경우도 공개로 취급합니다.

모든 함수나 메서드의 독스트링에는 위와 같은 규칙에 따라 pre 키워드로 사전 조건을 기술할 수 있습니다. 사후 조건은 post 키워드로 기술하며, 이 키워드 뒤에 변수 목록을 덧붙일 수도 있습니다. 이 변수들은 함수나 메서드의 본문과 같은 스코프에 있습니다. 이 목록은 함수/메서드가 수정할 수 있는 변수를 선언합니다.

예시:

class circbuf:

    def __init__(self, leng):
        """Construct an empty circular buffer.

        pre: leng > 0
        post[self]:
            self.is_empty()
            len(self.buf) == leng
        """

reStructuredText [7]로 작성한 독스트링을 지원하기 위해 콜론 하나(:) 대신 이중 콜론(::)을 사용할 수 있습니다. 예를 들어, 다음 두 독스트링은 같은 계약을 기술합니다:

"""pre: leng > 0"""
"""pre:: leng > 0"""

사전 조건과 사후 조건의 표현식은 모듈 네임스페이스에서 정의됩니다. 즉, 클로저 변수를 제외하면 함수가 접근할 수 있는 거의 모든 변수에 접근할 수 있습니다.

사후 조건의 계약 표현식에서는 두 개의 추가 변수에 접근할 수 있습니다. __old__는 post 키워드 바로 뒤에 오는 변수 목록에 선언된 값의 얕은 복사본으로 채워지며, __return__은 함수나 메서드의 반환값에 바인딩됩니다.

예시:

class circbuf:

    def get(self):
        """Pull an entry from a non-empty circular buffer.

        pre: not self.is_empty()
        post[self.g, self.len]:
            __return__ == self.buf[__old__.self.g]
            self.len == __old__.self.len - 1
        """

모든 계약 표현식은 몇 가지 추가 편의 함수에 접근할 수 있습니다. 시퀀스의 참 여부를 더 쉽게 평가할 수 있도록 두 함수 forall과 exists가 다음과 같이 정의되어 있습니다:

def forall(a, fn = bool):
    """Return True only if all elements in a are true.

    >>> forall([])
    1
    >>> even = lambda x: x % 2 == 0
    >>> forall([2, 4, 6, 8], even)
    1
    >>> forall('this is a test'.split(), lambda x: len(x) == 4)
    0
    """

def exists(a, fn = bool):
    """Returns True if there is at least one true value in a.

    >>> exists([])
    0
    >>> exists('this is a test'.split(), lambda x: len(x) == 4)
    1
    """

예시:

def sort(a):
    """Sort a list.

    pre: isinstance(a, type(list))
    post[a]:
        # array size is unchanged
        len(a) == len(__old__.a)

        # array is ordered
        forall([a[i] >= a[i-1] for i in range(1, len(a))])

        # all the old elements are still in the array
        forall(__old__.a, lambda e: __old__.a.count(e) == a.count(e))
    """

조건을 더 쉽게 평가할 수 있도록 implies 함수가 정의되어 있습니다. 인자가 두 개이면 논리 함의(=>) 연산자와 비슷합니다. 인자가 세 개이면 C의 조건 표현식(x?a:b)과 비슷합니다. 이 함수는 다음과 같이 정의되어 있습니다:

implies(False, a) => True
implies(True, a) => a
implies(False, a, b) => b
implies(True, a, b) => a

함수에 진입하면 해당 함수의 사전 조건을 검사합니다. 사전 조건 중 하나라도 거짓이면 어서션 오류가 발생합니다. 함수가 공개 함수이면 클래스나 모듈의 불변 조건도 검사합니다. post에 선언된 변수의 복사본을 저장한 뒤 함수를 호출하고, 함수가 예외를 발생시키지 않고 종료되면 사후 조건을 검사합니다.

예외

함수나 메서드가 예외를 발생시키며 종료되더라도 클래스/모듈 불변 조건은 검사합니다(사후 조건은 검사하지 않습니다).

계약이 실패하면 언제나 ContractViolationError 예외의 서브클래스인 예외가 발생하며, ContractViolationError는 다시 AssertionError 예외의 서브클래스입니다. 사전 조건이 실패하면 PreconditionViolationError 예외가 발생합니다. 사후 조건이 실패하면 PostconditionViolationError 예외가 발생하고, 불변 조건이 실패하면 InvariantViolationError 예외가 발생합니다.

클래스 계층 구조:

AssertionError
    ContractViolationError
        PreconditionViolationError
        PostconditionViolationError
        InvariantViolationError
        InvalidPreconditionError

InvalidPreconditionError는 사전 조건이 규칙에 어긋나게 강화되었을 때 발생합니다. 다음 절인 상속을 참고하십시오.

예시:

try:
    some_func()
except contract.PreconditionViolationError:
    # failed pre-condition, ok
    pass

상속

클래스의 불변 조건에는 모든 상위 클래스의 불변 조건이 모두 포함됩니다(클래스 불변 조건은 상위 클래스 불변 조건과 AND로 결합됩니다). 이 불변 조건들은 메서드 결정 순서(method-resolution order)에 따라 검사됩니다.

메서드의 사후 조건에는 오버라이드된 모든 사후 조건도 포함됩니다(메서드 사후 조건은 오버라이드된 모든 메서드의 사후 조건과 AND로 결합됩니다).

오버라이드하는 메서드의 사전 조건이 충족되면 오버라이드된 메서드의 사전 조건은 무시할 수 있습니다. 그러나 오버라이드하는 메서드의 사전 조건이 실패하면, 오버라이드된 메서드의 사전 조건도 모두 실패해야 합니다. 그렇지 않으면 InvalidPreconditionError라는 별도의 예외가 발생합니다. 이를 통해 사전 조건의 약화를 지원합니다.

다소 인위적인 예제:

class SimpleMailClient:

    def send(self, msg, dest):
        """Sends a message to a destination:

        pre: self.is_open() # we must have an open connection
        """

    def recv(self):
        """Gets the next unread mail message.

        Returns None if no message is available.

        pre: self.is_open() # we must have an open connection
        post: __return__ is None or isinstance(__return__, Message)
        """

 class ComplexMailClient(SimpleMailClient):
    def send(self, msg, dest):
        """Sends a message to a destination.

        The message is sent immediately if currently connected.
        Otherwise, the message is queued locally until a
        connection is made.

        pre: True # weakens the pre-condition from SimpleMailClient
        """

    def recv(self):
        """Gets the next unread mail message.

        Waits until a message is available.

        pre: True # can always be called
        post: isinstance(__return__, Message)
        """

사전 조건은 약화될 수만 있으므로, ComplexMailClient는 기존 코드를 망가뜨릴 걱정 없이 SimpleMailClient를 대체할 수 있습니다.

근거

다음 차이점을 제외하면, Python을 위한 계약에 의한 프로그래밍은 Eiffel DBC 명세 [3]를 그대로 따릅니다.

계약을 독스트링에 포함하는 방식은 doctest 모듈을 본뜬 것입니다. 이 방식은 추가 문법이 필요 없게 하고, 계약이 있는 프로그램의 하위 호환성을 보장하며, 계약을 문서에 포함하기 위한 추가 작업도 필요 없게 합니다.

Eiffel 스타일의 REQUIRE, ENSURE, INVARIANT 대신 pre, post, inv 키워드를 선택한 이유는 더 짧고 수학적 표기법에 더 가까우며, 좀 더 미묘한 이유도 있기 때문입니다: ‘require’라는 단어는 호출자의 책임을 암시하는 반면, ‘ensure’는 제공자의 보장을 암시합니다. 하지만 다중 상속을 사용할 때는 호출자의 잘못이 없어도 사전 조건이 실패할 수 있고, 다중 스레드를 사용할 때는 함수의 잘못이 없어도 사후 조건이 실패할 수 있습니다.

Eiffel에서 사용하는 루프 불변 조건은 지원하지 않습니다. 루프 불변 조건은 구현하기 번거롭고, 어차피 문서의 일부도 아닙니다.

변수 이름 __old__와 __return__은 return 키워드와의 충돌을 피하고 Python 명명 규칙과의 일관성을 유지하기 위해 선택되었습니다. 이 변수들은 공개되어 있으며 Python 구현이 제공합니다.

post 키워드 뒤에 변수 선언을 두면 함수나 메서드가 수정할 수 있는 대상을 정확히 기술할 수 있습니다. 이를 통해 Eiffel의 NoChange 문법이 필요 없어지고, __old__의 구현도 훨씬 쉬워집니다. 또한 이는 Z 스키마 [9]와도 더 잘 맞습니다. Z 스키마는 무엇이 변경되는지 선언하는 부분과 그 변경을 제한하는 부분의 두 부분으로 나뉩니다.

__old__ 값에 변수의 얕은 복사본을 사용하면 계약 프로그래밍의 구현이 시스템을 지나치게 느리게 만드는 것을 방지할 수 있습니다. 함수가 얕은 복사로는 포착되지 않는 값을 변경한다면, 다음과 같이 그 변경 사항을 선언할 수 있습니다:

post[self, self.obj, self.obj.p]

forall, exists, implies 함수는 기존 함수들을 계약으로 문서화하는 데 얼마간 시간을 들인 뒤에 추가되었습니다. 이 함수들은 흔히 쓰이는 명세 관용구의 대부분을 표현합니다. implies를 함수로 정의하면 제대로 동작하지 않을 것처럼 보일 수도 있지만(다른 불리언 연산자와 달리 인자가 필요 여부와 관계없이 평가되므로), 계약 안의 어떤 표현식에도 부작용이 없어야 하므로 계약에서는 문제없이 동작합니다.

참조 구현

참조 구현 [1]을 사용할 수 있습니다. 이 구현은 클래스나 모듈의 네임스페이스를 직접 변경하여 기존 함수를 계약 검사를 수행하는 새 함수로 대체합니다.

__getattr__을 변칙적으로 조작하거나 [5] __metaclass__를 사용하는 [6] 다른 구현도 있습니다.

참고 문헌