6.7 단언(assertion)과 예외

6.7.1 단언 구문: pragma assert

pragma assert는 코드의 특정 지점에서 부울 표현식이 참이어야 함을 명시하는 프라그마입니다. 이는 코드의 특정 상태에 대한 가정을 명시적으로 표현하고, 계약 기반 프로그래밍(Design by Contract)의 한 요소를 구현하는 방법입니다. 만약 실행 시점에 명시된 부울 표현식이 거짓(False)으로 평가되면, 프로그램은 Ada.Assertions.Assertion_Error 예외를 발생시킵니다.

이 프라그마는 선언이나 문장이 위치할 수 있는 모든 곳에 사용할 수 있으며, 다음과 같은 형태로 작성할 수 있습니다.

메시지가 없는 경우

메시지 없이 조건식을 인수로 사용하여 조건이 참인지를 검사합니다.

-- 조건식만 사용

pragma [...];

-- `check` 식별자와 조건식만 사용

pragma [...];

메시지를 포함하는 경우

조건이 거짓일 때 디버깅 시 참고할 수 있는 메시지를 포함할 수 있습니다.

-- 조건식과 메시지를 위치 기반으로 명시

pragma [...];

-- `message` 식별자 사용

pragma [...];

-- `check` 및 `message` 식별자 사용

pragma [...];

예시

다음은 큐(queue)에서 원소를 꺼내는 서브프로그램의 시작 부분에서, 큐가 비어있지 않다는 사전 조건을 단언하는 예시입니다.

procedure dequeue (q : in out Queue_Type;  item : out Element_Type) is

begin

  -- 사전 조건: 큐가 비어있지 않아야 함을 단언

  pragma [...],

                 message => "Dequeue attempted on an empty queue.");

  -- 큐에서 원소를 꺼내는 로직

  -- ...

end dequeue;

is_empty (q)가 참인 상태에서 dequeue 프로시저가 호출되면, pragma assert의 부울 표현식은 거짓으로 평가됩니다. 그 결과, 프로그램은 "Dequeue attempted on an empty queue." 메시지와 함께 Ada.Assertions.Assertion_Error 예외를 발생시킵니다. 이 dequeue 프로시저에는 별도의 예외 처리부가 없으므로, 발생한 예외는 프로시저를 호출한 외부 코드로 전달(전파)되며, 호출한 코드에서 해당 예외를 처리할 수 있습니다.

6.7.2 단언 정책 설정: pragma assertion_policy

런타임에 단언을 검사하는 것은 프로그램의 성능에 영향을 줄 수 있습니다. pragma assertion_policy는 단언의 검사 여부를 제어하는 정책을 설정하는 프라그마입니다. 이를 통해 개발 중에는 단언을 활성화하여 조건 검사를 수행하고, 최종 배포 버전에서는 단언을 비활성화하여 해당 검사를 생략할 수 있습니다.

구문 (syntax)

pragma assertion_policy는 두 가지 기본 형태로 사용됩니다.

1. 모든 단언에 일괄 정책 적용

가장 간단한 형태로, 특정 영역 내의 모든 종류의 단언에 하나의 정책을 일괄적으로 적용합니다.

pragma assertion_policy (<정책 식별자>);

정책 식별자 종류는 다음과 같습니다.

• check: 실행 시점에 단언을 검사합니다.
• ignore: 실행 시점에 단언을 검사하지 않습니다.
• 컴파일러별 추가 정책: 컴파일러 제작사가 별도로 정의한 정책이 사용될 수 있습니다.

예시

-- 이 프라그마 이후부터 현재 선언부가 끝나는 지점까지 모든 단언을 검사하도록 설정

pragma assertion_policy (check);

-- 이 프라그마 이후부터 현재 선언부가 끝나는 지점까지 모든 단언을 무시하도록 설정

pragma assertion_policy (ignore);

2. 특정 단언에 선택 정책 적용

<단언 종류 표식> => <정책 식별자> 쌍을 쉼표(,)로 구분하여, 특정 종류의 단언에만 선택적으로 정책을 설정합니다.

-- 사전 조건(`pre`)은 검사하고, 사후 조건(`post`)은 무시하도록 설정

pragma assertion_policy (

  pre  => check,

  post => ignore

);

단언 종류 표식은 다음과 같습니다.

• assert: pragma assert로 작성된 단언을 의미합니다.
• static_predicate, dynamic_predicate: 서브타입에 정의된 정적 또는 동적 술어(predicate)를 의미합니다.
• pre, pre'class: 서브프로그램의 사전 조건을 의미합니다. ('class는 클래스 전체 타입에 적용되는 사전 조건을 지정합니다.)
• post, post'class: 서브프로그램의 사후 조건을 의미합니다. ('class는 클래스 전체 타입에 적용되는 사후 조건을 지정합니다.)
• type_invariant, type_invariant'class: 타입 불변식을 의미합니다. ('class는 클래스 전체 타입에 적용되는 타입 불변식을 지정합니다.)
• default_initial_condition: 타입의 기본 초기 조건을 의미합니다.
• 이 외에 컴파일러 구현에 따라 추가적인 종류가 있을 수 있습니다.

적용 범위와 규칙

pragma assertion_policy에 허용되는 위치는 다음과 같습니다:

• 선언부 (declarative part) 내부
• 패키지 명세 (package specification) 내부
• 설정 프라그마 (configuration pragma)

프라그마의 효력은 프라그마가 위치한 지점부터 해당 프라그마가 포함된 가장 안쪽의 선언부 영역(declarative region)이 끝나는 지점까지입니다. 예를 들어, 프로시저의 선언부에 위치했다면 프로시저 내부 전체에 영향을 줍니다. 여러 정책이 중첩된 영역에 적용될 경우, 가장 안쪽에 위치한 정책이 우선적으로 적용됩니다.

예시

다음은 특정 서브프로그램 내에서 사전 조건(pre) 검사를 비활성화하는 예시입니다.

procedure example_procedure (value : Integer) is

  -- 이 프로시저 내에서는 사전 조건 검사를 무시하도록 정책 설정

  pragma assertion_policy (pre => ignore);

begin

  -- ... 프로시저의 로직 ...

end example_procedure;

6.7.3 Ada.Assertions 패키지

Ada.Assertions는 단언(assertion)과 관련된 서비스를 제공하는 표준 라이브러리 패키지입니다. 이 패키지에는 단언 실패 시 발생하는 Assertion_Error 예외가 정의되어 있으며, pragma assert와는 다른 방식으로 단언을 수행하는 assert 프로시저를 제공합니다.

assert 프로시저

assert 프로시저는 코드 내에서 직접 호출하여 조건이 참인지를 검사하는 서브프로그램입니다. pragma assert와 마찬가지로 검사할 부울 조건과 선택적인 메시지 문자열을 인자로 받습니다.

구문 (syntax)

-- 메시지가 없는 경우

Ada.Assertions.[...];

-- 메시지를 포함하는 경우

Ada.Assertions.[...];

만약 check 매개변수에 전달된 조건이 거짓(False)이면, assert 프로시저는 Assertion_Error 예외를 발생시킵니다.

단언 정책으로부터 독립성

assert 프로시저는 pragma assertion_policy의 영향을 받지 않습니다. pragma assert는 assertion_policy가 ignore로 설정되면 해당 검사는 컴파일 시 제거될 수 있습니다. 그러나 Ada.Assertions.assert 프로시저는 assertion_policy 설정과 관계없이 항상 실행되어 조건을 검사합니다.

assert 프로시저는 assertion_policy의 영향을 받지 않는 특성으로 인해, 컴파일러 정책에 의해 비활성화되지 않아야 하는 불변 조건이나 계약(contract)을 검증하는 데 사용됩니다.

6.7.4 표준 라이브러리에서의 단언 검사

Ada 표준 라이브러리의 특정 패키지들은 사전조건(pre), 정적 술어(static_predicate), 동적 술어(dynamic_predicate)와 같은 단언(assertion)의 준수 여부를 확인하기 위한 검사를 포함합니다.

각각의 단언 검사는 특정 표준 라이브러리 구성 요소(예: 패키지)와 그 안에 포함된 모든 후손 단위(descendant unit)에 적용됩니다. 후손 단위란 특정 구성 요소 내부에 한 단계 또는 여러 단계에 걸쳐 중첩된 모든 패키지, 서브프로그램 등을 의미합니다.

예를 들어 Ada 코드에서 A 내부에 B가 선언되고, 다시 B 내부에 C가 선언된 경우, B와 C는 모두 A의 후손 단위입니다.

-- 최상위 구성 요소 A

package A is

  -- ...

end A;

package body A is

  -- B는 A의 후손 단위입니다.

  package B is

    -- ...

  end B;

  package body B is

    -- C 또한 A의 후손 단위입니다.

    package C is

      -- ...

    end C;

    -- ...

  end B;

end A;

따라서 특정 단언 검사가 A에 적용된다면, 그 검사는 A의 모든 후손 단위인 B와 C 내부의 모든 선언에 효력을 미칩니다. 구체적인 적용 대상은 다음과 같습니다.

• 후손 단위(B와 C 모두) 안에 선언된 모든 개체(변수, 타입 등)
• 이러한 후손 단위(B나 C)에 속한 제네릭(Generic)을 바탕으로 생성된 인스턴스 내부의 모든 개체

다음은 레퍼런스 매뉴얼에 명시된 언어에 정의된 단언 검사들의 목록입니다. 이러한 검사가 실패할 경우, Assertion_Error 예외가 발생합니다.

• calendar_assertion_check
  • Calendar 패키지와 관련된 단언을 검사합니다.
• characters_assertion_check
  • Characters, Wide_Characters, Wide_Wide_Characters 패키지들과 관련된 단언을 검사합니다.
• containers_assertion_check
  • Containers 패키지와 관련된 단언을 검사합니다.
• interfaces_assertion_check
  • Interfaces 패키지와 관련된 단언을 검사합니다.
• io_assertion_check
  • Sequential_IO, Direct_IO, Text_IO, Wide_Text_IO, Wide_Wide_Text_IO, Storage_IO, Streams.Stream_IO, Directories 패키지들과 관련된 단언을 검사합니다.
• numerics_assertion_check
  • Numerics 패키지와 관련된 단언을 검사합니다.
• strings_assertion_check
  • Strings 패키지와 관련된 단언을 검사합니다.
• system_assertion_check
  • System 패키지와 관련된 단언을 검사합니다.