표명

3. 표명의 사용

프로그래머들은 표명을 사용하여 프로그램들을 지정하고 프로그램 유효성을 추정할 수 있다.^[22] 이를테면 전제 조건(precondition), 즉 특정 코드 부분의 시작점에 위치한 표명은 코드가 실행될 것으로 예측하는 상태의 집합을 결정한다. 후행 조건(postcondition), 즉, 마지막에 위치한 표명은 실행 종료 시점에서 예측되는 상태를 기술한다. (예: `x > 0 { x++ } x > 1`)

상기의 예는 토니 호어가 그의 1969년 논문에 표명을 포함하기 위해 기술하고 있다.^[22] 해당 기술은 현존하는 주류 프로그래밍 언어에서는 이용할 수 없다. 그러나 프로그래머들은 프로그래밍 언어의 주석 기능을 이용하여 비검사형 표명(unchecked assertion)을 포함할 수 있다. 이를테면 C에서는 다음과 같다:

```c

x = 5;

x = x + 1;

// {x > 1}

```

주석에 들어간 중괄호를 통해 다른 용도의 주석과 구별할 수 있다.

라이브러리를 통해 표명 기능을 이용할 수 있다. 이를테면 C99을 지원하는 glibc를 이용하는 C에서는 다음과 같다:

```c

#include

x = 5;

x = x + 1;

assert(x > 1);

```

현대의 일부 프로그래밍 언어는 런타임 중에서나 이따금 정적인 상태에서 검사되는 문을 가리키는 검사형 표명(checked assertion)을 포함하기도 한다. 런타임 중에 표명이 거짓으로 평가되면 표명 실패(assertion failure)를 초래하여 실행이 중단되는 것이 일반적이다. 이를 통해 논리적 불일치가 감지된 위치에 집중할 수 있고 개발자는 의외의 결과가 나타나는 경우 보다 이 방법을 더 선호할 수 있다.

표명을 이용하면 프로그래머가 프로그램에 대한 설계, 개발, 추론을 도울 수 있다.

에펠과 같은 언어에서, 표명은 설계 과정의 일부를 형성합니다. 반면 C와 Java와 같은 다른 언어에서는 런타임에 가정사항을 확인하기 위해서만 사용합니다. 두 경우 모두 런타임에 유효성을 검사할 수 있지만, 일반적으로 억제될 수도 있습니다.

에펠과 같은 언어에서는, 표명은 설계 과정의 일부이다. C나 자바에서는 실행 시에 전제 조건을 확인하는 정도이다. 어느 경우든 실행 시에 정당성을 확인할 수 있지만, 소프트웨어 개발 시(디버깅 시)에만 유효화되고, 최종적으로는(소프트웨어 출시 시에는) 무효화(억제)되는 경우가 많다.

3. 1. 계약에 의한 설계에서의 표명

3. 2. 실행 시간 검사를 위한 표명

3. 3. 개발 주기 동안의 표명 활용

4. 표명 비활성화

대부분의 프로그래밍 언어는 어설션(표명)을 전역적으로 또는 독립적으로 활성화하거나 비활성화할 수 있도록 지원한다.^[6] 표명은 개발 단계에서 활성화되고, 최종 테스트 및 고객에게 릴리스될 때 비활성화된다.^[6] 어설션을 검사하지 않으면 어설션을 평가하는 비용을 절약할 수 있으며, 어설션에 부작용이 없다고 가정할 때 정상적인 상황에서는 동일한 결과를 생성한다.^[6] 비정상적인 상황에서는 어설션 검사를 비활성화하면 중단될 프로그램이 계속 실행될 수 있다.^[6]

C, YASS, C++를 포함한 일부 언어는 전처리기를 사용하여 컴파일 시간에 어설션을 완전히 제거할 수 있다.^[6]

파이썬 인터프리터를 "-O"(최적화) 인수로 실행하면 파이썬 코드 생성기가 어설션에 대한 바이트코드를 내보내지 않게 된다.^[6]

자바는 어설션을 ''활성화''하기 위해 런타임 엔진에 옵션을 전달해야 한다.^[6] 이 옵션이 없으면 어설션은 우회되지만, JIT 컴파일러가 런타임에 최적화하거나 프로그래머가 `if (false)` 절 뒤에 각 어설션을 수동으로 배치하여 컴파일 시 제외하지 않는 한 코드에 항상 남아 있다.^[6]

프로그래머는 언어의 일반적인 어설션 검사 메커니즘을 우회하거나 조작하여 항상 활성 상태인 검사를 코드에 내장할 수 있다.^[6]

5. 오류 처리와의 비교

단언문은 논리적으로 불가능한 상황을 문서화하고 프로그래밍 오류를 발견하는 데 사용되며, 일반적인 예외 처리와는 구분된다. 오류 처리는 발생 가능한 오류 상황을 다루지만, 단언문은 발생해서는 안 되는 상황을 감지한다.

일반적인 오류 처리 메커니즘으로 단언문을 사용하는 것은 현명하지 않다. 단언문은 오류 복구를 허용하지 않고 프로그램 실행을 즉시 중단시키며, 제품 코드에서는 비활성화되는 경우가 많다. 또한 사용자 친화적인 오류 메시지를 표시하지 않는다.

C 코드에서 `malloc` 함수가 메모리 할당에 실패하여 `NULL` 포인터를 반환하는 경우를 예로 들어보자. 운영 체제는 `malloc` 호출의 성공을 보장하지 않으므로 메모리 부족 오류는 발생 가능하다. 이때 단언문을 사용하면 프로그램이 즉시 중단되지만, 단언문이 없다면 `ptr`이 역참조될 때까지 실행이 계속될 수 있다.

```c

int *ptr = malloc(sizeof(int) * 10);

assert(ptr);

// use ptr

...

```

정상적인 실패 처리가 필요한 경우(예: 서버에서 여러 클라이언트를 처리하거나 리소스를 해제해야 하는 경우)에는 단일 트랜잭션 실패가 갑작스러운 중단보다 낫다.

단언문의 인수로 사용되는 표현식의 부작용에 의존하는 것은 또 다른 오류를 야기할 수 있다. 단언문은 조건 확인만을 목적으로 해야 하며, 프로그램 릴리스 시 비활성화될 수 있음을 고려해야 한다.

```c

int *ptr;

// Statement below fails if malloc() returns NULL,

// but is not executed at all when compiling with -NDEBUG!

assert(ptr = malloc(sizeof(int) * 10));

// use ptr: ptr isn't initialised when compiling with -NDEBUG!

...

```

위 코드에서 `NDEBUG` 매개변수를 사용하여 컴파일하면 `assert()` 문이 제거되어 `malloc()`이 호출되지 않고 `ptr`이 초기화되지 않아 세그먼테이션 오류나 널 포인터 오류를 발생시킬 수 있다. 이는 추적하기 어려운 버그로 이어질 수 있다.

최신 컴파일러는 위와 같은 코드에 대해 경고를 표시할 수 있다.^[7]

결론적으로, 표명은 논리적으로 발생할 수 없는 상황을 검사하고, 에러 처리는 일반적으로 발생할 수 있는 에러를 처리하는 데 사용해야 한다.

6. 역사

1947년 폰 노이만과 골드스타인은 IAS 머신 설계 보고서에서 초기 버전의 순서도를 사용한 알고리즘을 설명하면서 단언(assertion)을 포함시켰다. 그들은 "C가 흐름 다이어그램의 특정 지점에 실제로 도달할 때마다 하나 이상의 바운드 변수가 특정 지정된 값을 갖거나 특정 속성을 갖거나 서로 특정 속성을 만족시킬 수 있다는 것이 사실일 수 있습니다. 또한, 우리는 그러한 지점에서 이러한 제약의 유효성을 나타낼 수 있습니다. 이러한 이유로 우리는 이러한 제약의 유효성이 주장되는 각 영역을 단언 상자라고 부르는 특별한 상자로 표시할 것입니다."라고 언급했다.^[8]

프로그램의 정확성을 증명하는 단언적 방법은 앨런 튜링에 의해 옹호되었다. 1949년 6월 24일 케임브리지에서 열린 강연 "대규모 루틴 검사"에서 튜링은 다음과 같이 제안했다. "프로그램이 올바른지 확인하는 의미에서 대규모 루틴을 어떻게 검사할 수 있습니까? 검사하는 사람이 너무 어려운 작업을 수행하지 않도록 하기 위해 프로그래머는 개별적으로 확인할 수 있고 전체 프로그램의 정확성이 쉽게 따르는 여러 가지 확실한 '단언'을 해야 합니다."^[9]

참조

_[1] 논문 An axiomatic basis for computer programming http://lambda-the-ul[...] 1969
_[2] 웹사이트 Programming With Assertions http://docs.oracle.c[...]
_[3] 간행물 Compile Time Assertions in C http://www.jaggersof[...] 1999
_[4] 뉴스 GCC 4.3 Release Series — Changes, New Features, and Fixes https://gcc.gnu.org/[...] GNU
_[5] 웹사이트 Static Assertions http://dlang.org/ver[...] The D Language Foundation 2022-03-16
_[6] 문서 assert statement https://docs.python.[...] Official Python Docs
_[7] 웹사이트 Warning Options (Using the GNU Compiler Collection (GCC)) https://gcc.gnu.org/[...]
_[8] 문서 Planning and Coding of problems for an Electronic Computing Instrument https://library.ias.[...] 1947-04-01
_[9] 문서 Checking a Large Routine https://turingarchiv[...] 1949
_[10] 논문 An axiomatic basis for computer programming http://lambda-the-ul[...] 1969
_[11] 웹사이트 assert - cppreference.com (C) https://en.cpprefere[...]
_[12] 웹사이트 assert - cppreference.com (C++) https://en.cpprefere[...]
_[13] 웹사이트 assert - cpprefjp C++日本語リファレンス https://cpprefjp.git[...]
_[14] 웹사이트 Conditional Compilation - D Programming Language https://dlang.org/sp[...]
_[15] 간행물 Compile Time Assertions in C https://web.archive.[...] 1999
_[16] 웹사이트 GCC 4.3 Release Series — Changes, New Features, and Fixes - GNU Project http://gcc.gnu.org/g[...]
_[17] 웹사이트 Predefined Macros | Microsoft Docs https://docs.microso[...] Visual C++ 2008
_[18] 웹사이트 Predefined Macros | Microsoft Docs https://docs.microso[...] Visual C++ 6.0
_[19] 웹사이트 コンパイル時アサート - boostjp https://boostjp.gith[...]
_[20] 문서 Checking a Large Routine http://www.turingarc[...] 1949
_[21] 인용 The Emperor's Old Clothes 1980
_[22] 논문 An axiomatic basis for computer programming http://lambda-the-ul[...] 1969