페이퍼요약 - 소프트웨어 개발에서 런타임 어써션 체킹에 대한 역사적 관점 by Clarke

제목: 소프트웨어 개발에서 런타임 어써션 체킹에 대한 역사적 관점(A Historical Perspective on Runtime Assertion Checking in Software Development)

저자: L. Clarke 외 1인, University of Massachusetts, 미국

문서유형: Academic 페이퍼(총 16 페이지), 2006년

 

런타임 어써션 체킹(assertion checking)의 발전 과정과 주요 특징에 대하여 조사한 자료

---

어써션 체킹(Assertion checking)

• 프로그램 정확성을 공식적으로 증명하는 방법인 어써션 체킹은 예상되는 올바른 프로그램 속성(properties)을 프로그램의 여러 지점에 정의하고, 실행되는 프로그램 상태가 명시된 어써션(Assertions)에 부합하는지 체크한다.
• 구현된 시스템에 내재된 결함(faults)은 테스팅이나 사용 중에 이상 증상(failures)으로 나타나게 되는데, 어써션(Assertions)은 이러한 결함의 위치를 파악하는데 유용한 자동화된 기법이다. 또한 겉으로 이상 증상(failures)으로 드러나지 않는 결함도 프로그램 실행에 따른 중간 단계의 내적 상태값들을 확인하여 식별 가능하다.
• 어써션 체킹 기능을 지원하는 프로그래밍 언어나 개발 모델 등은 어써션 선언과 그 적용 범위를 정의하기 위한 고유의 표기법(notation)을 제공한다.

어써션 체킹 적용 분야

• 어써션 체킹은 소프트웨어 엔지니어링의 다양한 분야에 적용되고 있다.
• 모델 체킹: 프로그램 실행에 따른 상태 영역(the state space)이 프로그램(시스템)의 여러 속성에 따라 정의된 논리적 어써션(logical assertions)에 부합하는지를 체크. 검증(verification) 방법의 일환으로 사용됨.
• 강력한 타입 체킹 언어(strong typing language): 데이터와 오브젝트의 엄격한 타입 체킹을 지원하는 여러 프로그래밍 언어(예, Ada)의 타입 시스템에 적용됨. 즉, 오늘날 프로그래밍 언어에서 사용하는 strong typing도 일종의 어써션 명세(assertion specification)로 볼 수도 있다. 예를 들어, FORTRAN 프로그램에서 배열의 인덱스 범위가 1과 100사이여야 한다는 것을 선언한 assertion의 경우 Ada나 Java 같은 현대 프로그래밍 언어에서는 적절한 배열 타입을 선언함으로써 쉽게 달성할 수 있다.
• 개발자들간의 프로그램의 이해를 돕기 위해 모듈 인터페이스를 더 정확하게 표현하는 방법으로 사용됨.
• 자동화된 런 타임 결함 발견: 프로그램 애플리케이션 로직에 따른 공식적인 어써션을 프로그램에 삽입하고, 프로그램 실행 시 어써션을 위반하는 사례를 찾아낸다.
• Assertions은 문서화(documentation)나 프로그램 정적 분석을 지원하는 부차적인 목적으로도 사용됨

디버깅 print문 또는 예외처리문(Exception handling)과 어써션의 차이점

• 디버깅의 가장 전통적이고 원초적인 방법인 print문 삽입과 어써션 체크 기법은 비슷한 면도 있지만 print문 삽입 방법이 좀 더 즉흥적이고 비체계적이라는 점에서 차이가 있다. 어써션은 뒤늦게 디버깅에서 고치고 돌려보고 하는 과정의 반복을 통해 print문을 삽입하는 고통을 피하기 위해 개발자가 코드에 심어 놓은 자동화된 방어 체크(automated defensive checks)라고 표현되기도 한다.
• 예외처리문(exceptions)도 어써션과 유사하면서도 차이가 있다. 예외처리문(exceptions)은 예외적인 이벤트가 발생했을 때의 프로그램 실행이 어떻게 동작해야 하는지를 기술하며, 예외 상황을 처리하는 과정에서 프로그램의 컨트롤 플로우를 크게 바꿔 버릴 수도 있다. 반면 어써션은 프로그램이 항상 만족시켜야 하는 불변 조건(program invariants)을 기술하며, 명시된 어써션(logical expressions)이 거짓으로 판명되는 경우가 생기면 이 에러 정보를 보고하고 그 심각성에 따라 프로그램 실행을 계속하거나 중단하거나 한다.

어써션 체킹의 History

1) 프로그램 동작을 특징짓는 논리적 어써션

• 1949년 Turing 연구: 각 프로그램 루틴의 다양한 지점에서 해당 상태를 나타내는 명확한 어써션(definite assertions)을 정의하고, 이 정보를 전체 프로그램의 정확성(correctness)을 결정하는데 사용
• 1963년 Goldstine과 von Neumann의 연구: 알고리즘의 불변값(invariants)을 명시하는 “assertion” 이라는 용어 사용
• 1966년 Naur의 연구: 어써션과 유사하지만 덜 정형적인 “general snapshot” 개념을 소개
• 1967년 Floyd의 연구: 루프의 반복에도 변하지 않는 불변 조건(invariant conditions)을 프로그램 플로우차트에서 표현하는 loop invariants 개념 사용
• 1969년 Hoare의 연구: 프로그램 동작을 공식적으로 기술하는데 있어 assertions 사용을 일반화함. 유명한 증명 스키마인 {P} S {Q}를 정의함. S는 프로그램 문장(statements), P는 S의 사전조건(the precondition), Q는 S의 사후조건(the postcondition)을 나타냄

 

2) 어써션을 이용한 명세 및 문서화(Specification and Documentation with Assertions)

• 1977년: 정형적 명세 언어(Formal specification languages)에서 어써션 기능(assertion capabilities)을 지원하기 시작. 오늘날 널리 사용되는 Z나 VDM 언어도 초기 버전부터 사전조건(the precondition)과 사후조건(the postcondition) 기능을 포함함
• 2001년: UML(the Unified Modeling Language)에서도 OCL(Object Constraint Language)을 통해 클래스와 인터페이스의 사전조건과 사후조건 명세를 지원. 명세된 사전/사후조건은 개발의 여러 단계에서 검증 및 런타임 체킹이 이루어짐

 

3) 프로그래밍 언어에서의 어써션

• 70년대 중반부터 프로그래밍 언어도 어써션 기능을(assertion capabilities) 제공하기 시작. 특별한 사전처리기(preprocessor)를 사용하거나 또는 어써션 구문(assertion constructs)을 프로그래밍 언어 설계 자체에 포함(즉, 프로그램 코멘트 등으로 어써션을 표현하는 대신 assertion statements를 프로그램 내에서 직접 기술하는 방법으로 지원)
• 1973년 Stucki와 Foshee의 연구: FORTRAN 소스 코드의 주석(annotations)으로 assertions을 정의하고, FORTRAN 검증 도구인 PET(Program Evaluator and Tester)을 사용하여 정의된 annotations을 프로그램 실행 중 적절한 시점에 불려지는 임베디드 런타임 체크(embedded runtime checks)로 전환
• 1979년: C 프로그래밍 언어의 assert 매크로 등장. 나중에 Java와 C# 언어에서도 이와 유사한 기능이 제공됨
• 1991년: Bertrand Meyer에 의해 개발된 Eiffel 프로그래밍 언어는 사전조건(preconditions), 사후조건(postconditions), 루프 불변값(loop invariants), 클래스 불변값(class invariants) 등의 어써션 구문(assertion constructs)을 언어 자체에 포함함. Eiffel은 오브젝트 오리엔티드 언어에서 assertions 사용을 지원하는 첫 번째 사례였음. Meyer는 오브젝트 오리엔티드 프로그램의 범주에서 assertions 사용하는데 있어 잘 알려진 design-by-contract 개념(어써션으로부터 자동으로 정보를 도출하여 클래스를 문서화)을 적용
• 1977년: assertions을 사전처리기(preprocessor)나 특별한 컴파일러(a special compiler)를 이용하여 먼저 정적으로 검증하고, 정적 분석이 불가능한 것들만 런타임 체크로 남겨두는 방법 등장. 이 개념은 Ada 프로그래밍 언어에서도 사용됨(예, array bound violations)

 

4) 하드웨어 설계 언어에서의 어써션(Assertions in Hardware Design Languages)

• 1980년 중반부터 하드웨어 설계에 어써션 기능(assertion capabilities)을 이용하기 시작
• 1987년: VHDL 하드웨어 설계의 정형적인 명세(the formal specification)를 위해 VAL(VHDL Annotation Language) 언어에 어써션 구문(assertion constructs)을 지원