서 론

주어진 프로그램에서 예외상황을 발생시키는

테스트 데이터 생성 방법

(A Test Data Generation to Raise User-Defined Exceptions

in First-Order Functional Programs)

류 석 영      이 광 근

(Sukyoung Ryu)  (Kwangkeun Yi)

요 약 주어진 프로그램에서 예외상황(exception)을 발생시키는 테스트 데이타를 자동으로 생성해주는 분석 방법을 제안한다. 분석 결과로 얻은 테스트 데이타를 사용하여, 프로그램 내에서 발생한 예외상황들이 프로그래머의 의도대로 처리되는지를 검사할 수 있다.

본 논문에서 제안하는 분석 방법은 입력으로 받은 프로그램에서 특정 예외상황이 발생한다는 조건을 시작으로 하여, 프로그램의 입력 값에 대한 제약식(constraints)을 만들어간다. 이 분석 방법이 옳다는 증명에 의해서, 분석 결과로 얻은 테스트 데이타를 입력으로 하여 프로그램을 수행시키면 지정한 예외상황이 항상 발생한다는 것을 보장할 수 있다.

함수를 인수나 결과값으로 전달하지 않고(first-order) ML 스타일의 예외상황 관리 방법을 제공하는 언어를 대상으로 하여 테스트 데이타 생성 방법을 제안하고, 이 분석 방법이 옳다는 것을 증명한 후 몇 가지 예를 사용하여 분석 과정을 설명한다.

Abstract We present a static analysis method to automatically generate test data that raise exceptions in input programs. Using the test data from our analysis, a programmer can check whether the raised exceptions are correctly handled with respect to the program's specification.

For a given program, starting from the initial constraint that a particular raise expression should be executed, our analysis derives necessary constraints for its input variable. Correctness of our analysis assures that any value that satisfies the derived constraints for the input variable will activate the designated raise expression.

In this paper, we formally present such an analysis for a first-order language with the ML-style exception handling constructs and algebraic data values, prove its correctness, and show a set of examples.

□ 본 연구는 과학기술부 창의적연구진흥사업 추진으로 얻어진 결과임.

예외상황 관리 방법을 제공하는 언어 (예를 들어, ML[1], Modula-3[2], Java[3], Ada[4]는 프로그래머로 하여금 프로그램의 예외적인 상황을 간단하게 정의하고 발생하고 처리할 수 있도록 한다. 프로그래머가 정의한 예외상황은 예외상황 발생 표현식(raise expression)에 의해 발생되고, 발생한 예외상황을 소멸할 수 있는 처리 표현식(handle expression)에 의해 처리된다.

예외상황 관리 방법은 프로그래머에 의해 아주 유용하게 사용된다. 단순히 프로그램 수행 중에 생기는 잘못된 경우를 처리하는 데에만 사용되는 것이 아니라, 여러 겹으로 겹쳐져 있는 프로그램의 제어 구조(control structure)를 한 번에 빠져 나오는 데에도 사용될 수 있고, 같은 연산 결과를 경우에 따라 다르게 처리해줄 때에도 사용될 수 있다.

하지만, 예외상황을 주의깊게 사용하지 않으면 오히려 프로그램의 안전도를 해치는 상황으로 발전할 수가 있다. 첫째, ML과 같이 타입을 검사하는 프로그래밍 언어라 할지라도, 예외상황에 의하여 프로그램의 안전도가 깨질 수 있다. ML 프로그램은 예외상황이 발생한 후에 적절하게 처리되지 않으면 프로그램이 비정상적으로 멈추게 되기 때문이다. 프로그램 내에서 발생한 예외상황이 제대로 처리되지 않으면 매우 위험한 상황이 발생할 수 있다[5]. 둘째, 프로그램에서 발생한 후 처리되지 않는 예외상황이 전혀 없는 경우라도, 발생한 예외상황이 프로그래머의 의도대로 맞게 처리되었는지를 확인하기는 매우 어렵다.

첫번째 문제에 대한 해결 방법은 이미 개발되어 있지만, 우리가 아는 바에 의하면, 두번째 문제는 아직 다루어진 적이 없다. 첫번째 문제에 대한 해결 방법으로는 주어진 프로그램에서 발생한 후 처리되지 않을 수 있는 예외상황을 예측하여 프로그래머에게 알려주는 도구가 개발되어 있다. 예를 들어, ML 프로그램에 대한 예외상황 분석기로[6, 7, 8, 9] 등이 있다.

두번째 문제에 대해 본 논문에서 제안하는 해결 방법은 주어진 프로그램 내의 모든 예외상황 발생 표현식을 수행시키는 테스트 데이타를 생성해주는 것이다. 자동으로 만들어낸 테스트 데이타를 입력값으로 프로그램을 수행시켜 예외상황이 발생하도록 한 후, 발생한 예외상황이 프로그램 내에 흘러다니는 것을 관찰하면 프로그래머의 의도대로 처리되는지를 확인할 수 있게 된다. 프로그램에서 raise에 의해 발생되는 예외상황이 아니고 수치 연산에 의한 Overflow 같이 다른 표현식에 의해 발생하는 예외상황에 대해서는 테스트 데이타를 생성하지 않는다.

관련 연구

테스트 데이타 생성에는 다음과 같은 세 가지 방법이 있다: 프로그램 내의 단위 구조(structural elements)에 대한 테스트 데이타를 만들어내는 방법[16, 17, 18, 19, 20, 21, 22, 23], 엄밀하게 정의된 문법(grammar)을 만족하는 테스트 데이타를 만들어내는 방법[24], 그리고 임의로 테스트 데이타를 만들어내는 방법[25]. 본 논문에서 제안하는 방법은 특정 수행 경로 (특정 예외상황을 발생시키는 수행 경로)에 대한 테스트 데이타를 생성하므로, 첫번째 방법에 속한다.

프로그램 내의 단위 구조에 대한 테스트 데이타를 만들어내는 방법[19, 20, 21, 22, 23]은 주로 요약 수행 방법(symbolic execution)을 사용해왔다. 프로그램을 직접 수행하지 않고

주어진 프로그램의 특정 수행 경로를 요약하여 따라가면서 프로그램 입력값에 대한 제약식을 만들어낸다. 대상 언어에 따라 분석이 만들어내는 제약식은, 변수값이 가져야 할 정수 범위(integer-intervals)[20] (Fortran), 변수 사이의 수치 관계(numeric formula)[21] (Fortran), 데이타 사이의 부등식[19] (Cobol-like language) 등이 된다. 요약 수행 방법과 다른 방법으로, Korel[16]은 동적으로 테스트 데이타를 생성하는 방법을 제안하였다. 주어진 프로그램에 대해 실제 프로그램의 수행을 관찰하다가, 프로그램이 정상적이지 않은 동작을 하게 되면 그렇게 만드는 입력값을 제외시켜 나가는 것이다.

우리가 알고 있는 한 예외상황을 발생시키는 테스트 데이타를 자동으로 생성하는 방법은 본 논문에서 처음으로 제안하는 것이다. 이 방법의 장점 중 한 가지는 테스트 데이타 생성 분석을 엄밀하게 다루었다는 것이다. 프로그램의 제약식을 만들어내는 방법을 정확하게 정의하고, 분석 방법의 보증성을 엄밀하게 증명하였다.

논문 구조

본 논문의 전체적인 구조는 다음과 같다. 본 논문에서 대상 언어로 사용하는 L 언어의 문법구조와 의미구조를 2장에서 정의한다. 3장에서는 테스트 데이타 생성 분석 방법을 제안하고 4장에서 분석의 보증성을 증명한다. 5장에서는 몇 가지 예를 사용하여 분석 방법을 설명하고, 6장에서 결론을 맺는다.

언어 L

본 논문에서 다루는 언어 L은 함수를 인수나 결과값으로 전달하지 않는 일차 언어이고(first-order), ML 스타일의 예외상황 관리 방법을 제공하며, 적극적으로 값을 계산하는(call-by-value) 언어이다:

□프로그램 내 표현식의 값은 함수가 될 수 없다. 따라서, 함수가 다른 함수의 인수나 결과값으로 전달되거나 변수에 할당될 수 없고, 프로그램 내의 모든 함수 호출 표현식에서 어떤 함수가 호출되는지를 프로그램 텍스트만 보고 바로 알아낼 수 있다.

□데이타 값은 유한한 갯수의 데이타 컨스트럭터(constructor)로 만들어진다. 예를 들어, 자연수를 나타내는 데이타는 두 가지 방법으로 만들어질 수 있다. ZERO와 임의의 인수를 가지고 만들어지거나, SUC과 자연수 인수를 가지고 만들어진다.

□예외상황은 인수를 가질 수 없다. L 언어에서 다루는 예외상황은 인수가 없이 예외상황 이름만으로 만들어진다.

□예외상황은 함수의 인수나 결과값으로 전달될 수 없다. 따라서, 함수 호출의 결과값으로 예외상황을 전달하는 □raise f(0)□와 같은 것은 표현할 수 없다. 예외상황을 발생시킬 때에는 □raise ERROR□와 같이 예외상황 이름을 분명하게 나타내야 한다.

L 언어의 문법 구조는 그림 1에 나타나 있다. 설명의 편의성을 위해서, 문자열, 숫자, 메모리 관련 연산(메모리 할당, 참조) 등은 생략하였다.

프로그램 내의 데이타는 □[eqn: kappa~e]□에 의해서 [eqn: kappa]라는 이름과 [eqn: e``]라는 인수를 갖도록 만들어진다. 데이타의 인수는 □[eqn: kappa^{-1}~e]□에 의해서 얻을 수 있다. 재귀함수 [eqn: f``]는 □fix[eqn: f~lambda~x.e``]□에 의해서 정의된다. 조건 분기문 □case [eqn: e_1 ~kappa~ e_2 ~ e_3``]□는 [eqn: e_1]의 값이 [eqn: kappa]라는 이름의 데이타일 경우에 [eqn: e_2]로 분기하고, 그렇지 않을 때에는 [eqn: e_3]로 분기한다. 예외상황 E는 □raise E□에 의해서 발생된다. 예외상황 처리 표현식 □handle [eqn: e_1] E [eqn: e_2]□는 [eqn: e_1]을 먼저 계산한다. [eqn: e_1]을 계산하는 도중에 예외상황이 발생하지 않으면 [eqn: e_1]의 값이 예외상황 처리 표현식의 결과값이 된다. [eqn: e_1]을 계산하는 도중에 예외상황 E가 발생하면 [eqn: e_2]의 값이 결과값이 되고, E가 아닌 다른 예외상황이 발생하면 그 예외상황은 처리되지 못하고 다시 발생된다. 여러 가지 예외상황을 처리하려면 예외상황 처리 표현식을 반복해서(nested handle expressions) 사용하면 된다. 예를 들어서, handle (handle [eqn: e_1] E [eqn: e_2]) F [eqn: e_3]는 두 가지 예외상황 E와 F를 처리할 수 있다.

본 논문에서는 앞으로,

□모든 변수가 서로 다른 이름을 갖는다고 가정한다 (alpha-converted).

□프로그램 내에 실행되지 않는 코드(dead code)는 없다고 가정한다.

□□L 프로그램□이라는 말로 입력 변수(free variables)가 있는 L 표현식 (expression)을 의미한다.

L 언어의 의미 구조

본 논문에서는 자연적 의미론 (natural semantics) [10]으로 L 언어의 의미 구조를 엄밀하게 정의한다. L 언어의 의미 구조는 그림 2, 3에 나와있다: 그림 2는 예외상황을 발생시키지 않는 정상적인 값을 계산하는 규칙을 나타내고 있고, 그림 3은 예외상황을 발생시키는 규칙을 나타내고 있다. 그림 2에 나와있는 것처럼, 예외상황 이름은 E로 표시하고 발생한 예외상황은 [eqn: hat {rm E}]으로 표시하기로 한다.

언어 L의 의미 구조를 정의하는 데 사용된 [eqn: sigma~ vdash e~ rightarrow~ v] (또는 [eqn: sigma~ vdash~ e~ rightarrow~ hat{rm E}])는 □[eqn: sigma]라는 환경 하에서 표현식 [eqn: e``]를 계산한 값이 [eqn: v] (또는 [eqn: hat{rm E}])□라는 것을 의미한다. 환경 [eqn: sigma]는 프로그램 내의 각 변수에 해당하는 값을 매핑(mapping)해주는 유한 함수이다. 프로그램의 값은 상수 0이거나 데이타, 또는  [eqn: sigma]에서 정의된 함수  fix[eqn: f~ lambda x.e``]를 나타내는 [eqn: langle sigma,~ {rm fix}~f~ lambda x.e rangle]이다. 일반적인 표기법을 사용하여, 유한 함수는 [eqn: f~IN ``A {scale 60 Buildrel rarrow fin} `B``]로 나타내고, [eqn: f~ [a` MAPSTO`` b]]는 [eqn: a]를 [eqn: b]로 매핑하고 [eqn: f``]의 정의구역에서 [eqn: a``]를 제외한 다른 모든 원소 [eqn: a'``]은 [eqn: f`(a')``]으로 매핑하는 새로운 함수를 나타낸다.

예외상황을 발생시키지 않는 규칙의 예로, 그림 2에 있는 case 표현식에 대한 규칙을 살펴보기로 한다. 규칙 [CASEN-1s]는 [eqn: e_1]의 값이 [eqn: kappa]라는 이름의 데이타일 때 [eqn: e_2]가 계산된다는 것을 나타낸다:

[eqn: {rm [CASEN-1s]} & ~&{sigma~ vdash~ e_1 ~rightarrow~ kappa``v ~~~~~~ sigma~vdash~e_2 ~rightarrow~ v'} over {sigma~vdash {rm case}~e_1 ~kappa~e_2 ~e_3 ~rightarrow~ v' }. #]

규칙 [CASEN-2s]는 [eqn: e_1]의 값이 [eqn: kappa]가 아닌 다른 이름의 데이타일 때 [eqn: e_3]가 계산된다는 것을 나타낸다:

[eqn: {rm [CASEN-2s]} & ~&{sigma~ vdash~ e_1 ~rightarrow~ kappa'``v ~~~~~~ sigma~vdash~e_3 ~rightarrow~ v'} over {sigma~vdash {rm case}~e_1 ~kappa~e_2 ~e_3 ~rightarrow~ v' }~~ kappa'not=kappa. #]

예외상황을 발생시키는 규칙에 대한 예로, 그림 3에 있는 handle 표현식에 대한 규칙을 다루기로 한다. 규칙 [HNDLX-1s]는 [eqn: e_1]에서 발생한 예외상황을 handle 표현식이 처리하지 못하는 경우이다:

[eqn: {rm [HNDLX-1s]} & ~&{sigma~ vdash~ e_1 ~rightarrow~ hat{rm E'}} over {sigma~vdash {rm handle}~e_1 ~{rm E}~e_2 ~rightarrow~ hat{rm E'} }~~ {rm E'}not={rm E}. #]

규칙 [HNDLX-2s]는 [eqn: e_1]에서 발생한 예외상황을 [eqn: e_2]가 처리하지만, [eqn: e_2]에서 다시 예외상황을 발생시키는 경우이다:

[eqn: {rm [HNDLX-2s]} & ~&{sigma~ vdash~ e_1 ~rightarrow~ hat{rm E}~~~~~sigma~ vdash~ e_2 ~rightarrow~ hat{rm E'}} over {sigma~vdash {rm handle}~e_1 ~{rm E}~e_2 ~rightarrow~ hat{rm E'} }. #]

집합 제약식

본 논문에서 제안하는 분석은 주어진 프로그램의 각 표현식 e에 대해서 se ♤ e : C 관계를 만들어내는 것이다. 집합식 se는 e의 값이 포함되어야 할 집합을 나타내고, C는 e가 se에 포함되기 위해 만족해야 할 제약식들(constraints)의 집합을 나타낸다. 따라서 ``se ♤ e : C''의 의미는 ``e의 값이 se에 포함되려면 C를 만족해야 한다''가 된다. 집합식(set expressions)과 제약식의 문법 구조와 의미 구조는 그림 4에 나와있다.

해석(interpretation) I는 집합 제약식 C (또는 집합식 se)가 true인지 false (또는 프로그램 값이나 발생한 예외상황)인지를 결정해준다. C에 있는 각 제약식 X[eqn: subseteq]se와 a[eqn: subseteq]X에 대해서, I(se)와 I(a)가 정의되어 있고 I(X)[eqn: subseteq]I(se)와 I(a)[eqn: subseteq]I(X)를 각각 만족할 때, 해석 I는 C에 있는 모든 조건들을 만족시키는 모델(해(solution))이라고 한다. C의 가장 큰 모델을 gm(C)라고 적기로 한다.

본 논문에서 집합식 se는 발생한 예외상황이나 프로그램 값들의 집합을 나타내게 된다. 예를 들어, [eqn: kappa~X]는 [eqn: X]에 있는 값들을 인수로 하고 [eqn: kappa]로 만들어지는 데이타를 나타내고:

[eqn: I(kappa``X) = \{kappa ``v~|~v~ in`` I(X) \},]

[eqn: kappa^{-1}~ X]는 [eqn: X]에 있는 값들 중 [eqn: kappa]로 만들어지는 데이타의 인수들을 나타낸다:

[eqn: I( kappa^{-1}~ X) = \{v~|~ kappa`` v~ in`` I( X) \}.]

분석에서 사용하는 집합 변수는 다음과 같이 세 가지로 분류할 수 있다: 1. 프로그램에 있는 각 변수 [eqn: x]의 값을 모아가는 [eqn: X], 2. 프로그램에 있는 각 재귀 함수 [eqn: f``]의 값을 나타내는 [eqn: F], 3. 분석 과정 중에 새로 만들어내는 집합 변수이다.

분석 규칙

본 논문에서 제안하는 분석 규칙은 그림 5, 6에 나와있다.

그림 5에 있는 상수 0에 대한 네 가지 규칙을 살펴보기로 한다. 0은 항상 집합 {0}에 포함되어 있다:

[C-1a]         0 ♤ 0 : {true}

0이 [eqn: X]에 포함되기 위해서 필요한 조건은 {0[eqn: subseteq][eqn: X]}이다:

[C-2a]       [eqn: X] ♤ 0 : {0[eqn: subseteq][eqn: X]}.

0이 [eqn: kappa^{-1}~ X]에 포함되기 위해서는 [eqn: X]가 [eqn: kappa] 0를 포함해야 한다:

[C-3a]      [eqn: kappa^{-1}] [eqn: X] ♤ 0 : {[eqn: kappa] 0[eqn: subseteq][eqn: X]}.

0이 그 외의 다른 집합에 포함될 방법은 없다:

[C-4a]      [eqn: se] ♤ 0 : {false}   [eqn: se`` not in``\{]0, [eqn: X], [eqn: kappa^{-1}~ X \}].

전제(premise)와 결론(conclusion)이 있는 규칙의 예로 [CONN-1a]를 살펴보면:

[eqn: {rm [CONN-1a]} & ~&{kappa^{-1}~X~ ♤~e~:~C} over {X~♤~kappa~e~:~C }, #]

[eqn: kappa~e]의 값이 [eqn: X]에 포함되기 위해서 [eqn: e``]의 값이 [eqn: kappa^{-1}~ X]에 포함되어야 함을 나타낸다.

그림 5에 있는 규칙 [CONN-3a], [DCONN-1a], [DCONN-2a], [DCONN-3a]는 새 변수를 만들어낸다. 다음을 예로 들면:

[eqn: {rm [CONN-3a]} &{kappa^{-1}~Y~♤~e~:~C} over {kappa'^{-1}~X~♤~kappa~e~:~C~cup~ \{Y~ subseteq~ kappa'^{-1}~X \} }~~ "새 변수 " Y. #]

[eqn: kappa~e]가 [eqn: kappa'^{-1}~ X]에 포함되기 위해서는 [eqn: e]의 값이 [eqn: kappa^{-1}( kappa'^{-1}~ X)]에 포함되어야 한다. 그러나 그림 4에 나와있는 집합식([eqn: se])의 문법 구조에 의해서 [eqn: kappa^{-1}] 다음에는 집합 변수만 올 수 있으므로, [eqn: kappa^{-1}] 다음에 [eqn: kappa'^{-1}~ X]가 올 수 없다. 이렇게 집합 제약식의 모양을 제한하는 이유는 집합 제약식의 해를 구하기 쉽게 하기 위해서이다. 집합 변수만 올 수 있는 곳에 집합 변수가 아닌 다른 집합식 [eqn: se']이 올 경우에는, [eqn: se']을 새로운 변수 [eqn: Y]로 바꾸고 [eqn: se']이 [eqn: Y]를 포함하도록 만든다. 따라서, [eqn: kappa'^{-1}~ X]를 새 변수 [eqn: Y]로 바꾸고 집합 제약식 [eqn: \{ Y~ subseteq~ kappa'^{-1}~ X \}]를 추가한다.

그림 5에 있는 규칙과 달리, 그림 6에 있는 규칙은 주어진 [eqn: se] 와 [eqn: e]에 대해 적용 가능한 규칙이 여러 가지가 있다. 따라서, se ♤ e : C를 만족하는 제약식 [eqn: C``]가 여러 가지로 만들어질 수 있다.

그림 6에 있는 규칙 [CASEX-a], [CASE-1a], [CASE-2a]를 살펴보기로 한다. case 표현식에서 예외상황이 발생한다면, 예외상황이 발생하는 위치에 따라 세 가지 가능성이 생긴다: [eqn: e_1]에서 발생하거나 [eqn: e_2] 또는 [eqn: e_3]에서 발생하는 경우이다. 규칙 [CASEX-a]는 [eqn: e_1]에서 예외상황이 발생하는 경우를 나타낸다:

[eqn: {rm [CASEX-a]}~~~~~ &{hat{rm E}~♤~e_1 ~:~C} over {hat{rm E}~♤~{rm case}~e_1 ~kappa~e_2 ~e_3 ~:~C}. #]

[eqn: e_1]이 예외상황 E를 발생하기 위해서 [eqn: C]가 필요하다면, case[eqn: e_1 ~ kappa~e_2 ~e_3]가 예외상황 E를 발생하기 위해서도 [eqn: C]가 필요하다. 규칙 [CASE-1a]는 [eqn: e_2]에서 예외상황이 발생하는 경우를 나타낸다:

[eqn: {rm [CASE-1a]}~~~~~ &{kappa~X~♤~e_1 ~:~C_1 ~~~se~♤~e_2 : C_2 } over {se~♤~{rm case}~e_1 ~kappa~e_2 ~e_3 ~:~C_1 cup C_2}~~~"새 변수"~ X. #]

[eqn: e_1]이 [eqn: kappa~ X]에 포함되기 위해서 [eqn: C_1]이 필요하고 [eqn: e_2]가 예외상황 E를 발생하기 위해서 [eqn: C_2]가 필요하다면, case[eqn: e_1 ~ kappa~e_2 ~e_3]가 예외상황 E를 발생하기 위해서는 [eqn: C_1 cup C_2]가 필요하다. 마지막으로 규칙 [CASE-2a]는 [eqn: e_3]에서 예외상황이 발생하는 경우를 나타낸다:

[eqn: {rm [CASE-2a]}~~~~~ &{bar{ kappa}~X~♤~e_1 ~:~C_1 ~~~se~♤~e_2 : C_2 } over {se~♤~{rm case}~e_1 ~kappa~e_2 ~e_3 ~:~C_1 cup C_2}~~~"새 변수"~ X. #]

[eqn: e_1]이 [eqn: bar{ kappa}~ X]에 포함되기 위해서 [eqn: C_1]이 필요하고 [eqn: e_3]가 예외상황 E를 발생하기 위해서 [eqn: C_2]가 필요하다면, case[eqn: e_1 ~ kappa~e_2 ~e_3]가 예외상황 E를 발생하기 위해서는 [eqn: C_1 cup C_2]가 필요하다.

그림 6에 있는 규칙 [APPX-2a]와 [APP-2a]는 함수 이름 [eqn: f``]에 대한 제약식을 만든다. 다음을 예로 들면:

[eqn: {rm [APP-2a]} &{X_n ~♤~e_2 ~:~C_1 ~~se~♤~[x_n / x]e_1~:~ C_2 } over {se~♤~{rm fix}~f~lambda x.e_1 ~ :~C_1 cup C_2 cup \{F~ subseteq~ lambda x.e_1 \}}"새 번호"~ n, #]

이 규칙은 [eqn: F``]의 값이 [eqn: \{ lambda x.e_1 \}]에 포함되어야 한다는 제약식을 만든다. 각 함수 이름에 대한 제약식은 이 두 규칙에 의해서만 만들어지므로, 함수 이름에 대한 집합 변수 [eqn: F``]는 항상 원소가 하나인 집합 [eqn: \{ lambda x.e_1 \}]를 나타내게 된다. 프로그램 분석 중에 나타나는 모든 변수의 이름을 서로 다르게 하기 위해서, 함수 내용 [eqn: e_1]에 나타나는 [eqn: x]를 모두 새로운 변수 [eqn: x_n]으로 바꾼 후에 [eqn: e_1]을 분석한다:□[eqn: [x_n /x]e_1].

그림 6에 있는 재귀함수 호출에 대한 규칙 [APP-3a]는 무한한 횟수로 사용될 수 없다. 각각의 재귀함수 [eqn: f``]에 대해서 [eqn: Used_f ()]는 현재까지 [APP-3a] 규칙을 적용하여 [eqn: f``]를 호출한 횟수를 기록한다. 함수 [eqn: f``]를 호출한 횟수가 미리 정한 제한값 [eqn: N``]을 넘으면 함수 [eqn: f``]에 대해서는 이 규칙을 더 이상 사용할 수 없도록 한다. 다음을 예로 들면:

[eqn: {rm [APP-3a]}~~ &{{X_n ``♤~e_2 ``:``C_1} atop {se``♤``[x_n / x]e_1``:``C_2} } over {se~♤~f~e_2 ~ :~C_1 cup C_2 }~~ { "프로그램 내의"{rm fix}`f~lambda x.e_1,} atop {"새 번호 " n, Used_f (n) le N } , #] [eqn: Used_f` () le N``]이라는 조건은 프로그램을 분석해가는 도중에 [eqn: f``]의 호출 횟수를 [eqn: N``]이하로 제한하게 된다. 재귀함수의 호출 횟수를 임의로 제한함으로써 가능한 테스트 데이타를 만들어내지 못할 수는 있지만, 테스트 데이타 생성 분석의 보증성(safety)을 위배하지는 않는다. 왜냐하면 테스트 데이타를 만들어내지 못하는 경우는 그 자체로 다음과 같은 테스트 데이타 생성 분석의 보증성(soundness) 조건을 만족하기 때문이다: 분석 결과로 얻은 테스트 데이타를 프로그램 입력으로 사용하여 프로그램을 수행시키면, 지정한 예외상황이 항상 발생한다.

규칙 [CASE-2a]와 [CASE-2a]는 [eqn: e_1]을 계산하여 얻은 데이타의 인수 값을 모으기 위해서 새 변수를 만들어낸다. 다음을 예로 들면:

[eqn: {rm [CASE-1a]}~~~~~ &{kappa~X~♤~e_1 ~:~C_1 ~~~se~♤~e_2 : C_2 } over {se~♤~{rm case}~e_1 ~kappa~e_2 ~e_3 ~:~C_1 cup C_2}~~~"새 변수"~ X. #]

[eqn: e_1]이 [eqn: kappa~ X]에 포함되기 위해서 [eqn: C_1`]이 필요하고 [eqn: e_2]가 [eqn: se]에 포함되기 위해서 [eqn: C_2]가 필요하다면, case [eqn: e_1 ~ kappa~e_2 ~e_3]가 [eqn: se]에 포함되기 위해서는 [eqn: C_1 cup C_2]가 필요하다. 이 규칙에서 새로 만든 변수 [eqn: X`]는 [eqn: e_1]을 계산하여 얻은 데이타의 인수 값을 모으게 된다.

집합 제약식을 만드는 방법

본 논문에서 제안하는 분석 방법은 입력으로 받은 프로그램 [eqn: e``]에서 특정 예외상황 E가 발생한다는 조건을 시작으로 하여, 프로그램의 입력 값에 대한 제약식(constraints)을 만들어간다. 그림 5, 6에 나와있는 규칙 중에서 [eqn: hat{rm E}]과 [eqn: e``]에 대해 적용 가능한 규칙을 적용해가면서 [eqn: hat{rm E}] ♤[eqn: e~:~ C``]를 만족하는 제약식의 집합 [eqn: C``]를 만들어가는 것이다.

집합 제약식의 해를 구하는 방법

집합 제약식의 해를 구하는 알고리즘은 집합 제약식의 성질에 따라 여러 가지[11, 12, 13, 14, 15]가 개발되어 있다. 일반적으로 널리 사용되고 있는 definite 집합 제약식[11, 12]은 최소모델 (minimal model)을 그 해로 갖게 되고, co-definite 집합 제약식[13, 14]은 최대모델 (maximal model)을 해로 갖는다. 본 논문에서 다루는 집합 제약식은 Charatonik과 Podelski[13, 14]에 의해 정의된 co-definite 집합 제약식에 속하므로, 집합 제약식 [eqn: C``]의 해가 존재한다면 가장 큰 모델 [eqn: gm(C)``]를 갖게 된다.

본 논문에서 다루는 집합 제약식의 해는 반복적 부동점 방법(iterative fixpoint method)을 사용하여 구할 수 있다. 주어진 프로그램의 분석 결과가 [eqn: C``]일 때, [eqn: C``]에 있는 각 집합 변수 [eqn: X`]의 값을 전체집합 [eqn: U`]로 초기화한 후 [eqn: C``]에 있는 각 집합 제약식에 따라 집합 변수들의 값을 계산한다. 모든 집합 변수들의 값이 더 이상 변하지 않을 때까지 반복해서 계산하면, 집합 제약식 [eqn: C``]의 가장 큰 모델 [eqn: gm(C)``]를 구하게 된다.

보증성 (Soundness)

분석 [eqn: hat{rm E}] ♤ [eqn: e~:~C``]에 의해 얻은 테스트 데이타를 입력으로 하여 프로그램 [eqn: e``]를 수행시키면 예외상황 [eqn: hat{rm E}]이 발생한다는 것을 증명한다. 증명에 들어가기 전에, 증명에 필요한 기호를 먼저 정의한다.

정의 1 (□[eqn: hat{rm E}]♤[eqn: e~:~C``]□) 프로그램 e에 대한 분석을  [eqn: hat{rm E}]♤[eqn: e~:~C``]라 할 때, 분석 [eqn: hat{rm E}]♤[eqn: e~:~C``]의 과정(derivation tree)을 □[eqn: hat{rm E}]♤[eqn: e~:~C``]□로 표시하기로 한다.

정의 2 (□[eqn: sigma~vdash~e~rightarrow~o]□) 프로그램 e에 대한 수행을 [eqn: sigma~vdash~e~rightarrow~o``]라 할 때, 수행 [eqn: sigma~vdash~e~rightarrow~o``]의 과정을  □[eqn: sigma~vdash~e~rightarrow~o``]□로 표시하기로 한다.

보조정리 1 프로그램 [eqn: e_0`]의 입력 [eqn: x_0]의 값을 [eqn: v`]로 하여 [eqn: e_0`]를 수행한 결과가 [eqn: [x_0 mapsto v]~vdash~e_0 ~rightarrow~o``]라고 하자. 수행 과정 □[eqn: [x_0 mapsto v]~vdash~e_0 ~rightarrow~o``]□에 나타나는 모든 [eqn: sigma`]는 다음의 성질을 만족한다:

[eqn: dom(sigma)]에 있는 변수들의 값은 프로그램 수행 중에 덮어씌워지지 않는다.

Proof. 프로그램 [eqn: e_0`] 안에 있는 변수들은 서로 다른 이름을 갖는다(alpha-converted). 프로그램 수행 중에 나타나는 변수는 프로그램의 입력 [eqn: x_0]나 함수 호출 표현식에서 만들어지는 변수 [eqn: x_n]뿐이다. [eqn: x_0]의 값은 초기환경 [eqn: [x_0 mapsto v]]에 정의되어 있고 그 이후에는 변경되지 않는다. 그림 2, 3에 있는 함수 호출 표현식에 대한 의미 구조를 살펴보면, 함수가 호출될 때마다 매번 다른 이름의 변수를 함수 인수로 사용하여 [eqn: sigma]에 그 값을 넣어놓는다. 따라서 프로그램 수행 중에 나타나는 모든 변수들은 그 변수가 만들어질 때 한 번만 [eqn: sigma]에 그 값을 넣어놓고, 그 이후에는 [eqn: sigma]에 있는 값을 바꾸지 않는다. 그러므로 [eqn: dom(sigma)]에 있는 모든 변수들의 값은 프로그램 수행 중에 덮어씌워지지 않는다. □

정의 3 ([eqn: sigma^v``]) 프로그램 [eqn: e_0`]의 입력 [eqn: x_0]의 값을 [eqn: v`]로 하여 [eqn: e_0`]를 수행한 결과가 [eqn: [x_0 mapsto v]~vdash~e_0 ~rightarrow~o``]라고 하자. 다음과 같이 재귀적으로(recursive) 정의한 환경을 [eqn: sigma^v ``]로 표시하기로 한다.

수행 과정 □[eqn: [x_0 mapsto v]~vdash~e_0 ~rightarrow~o``]□에 나타나는 모든 [eqn: sigma`]에 대해서,

(1) [eqn: sigma``]에 정의되어 있는 모든 [eqn: [x` mapsto` v'`]]를 다 모으고

(2) [eqn: sigma``]에 정의되어 있는 모든 [eqn: [f` mapsto` langle sigma', {rm fix } f~lambdax.e rangle`]]를 [eqn: [f` mapsto` langle sigma^v , {rm fix } f~lambdax.e rangle`]]로 바꾸어서 모은다.

보조정리 2 프로그램 [eqn: e_0`]의 입력 [eqn: x_0]의 값을 [eqn: v`]로 하여 [eqn: e_0`]를 수행한 결과가 [eqn: [x_0 mapsto v]~vdash~e_0 ~rightarrow~o``]라 하면, 수행 과정 □[eqn: [x_0 mapsto v]~vdash~e_0 ~rightarrow~o``]□ 중에 [eqn: sigma^v `]는 변하지 않는다.

Proof. 프로그램 [eqn: e_0`]의 수행 중에 환경 [eqn: sigma^v `]가 변하는 경우는 함수 호출 표현식에 대한 경우밖에 없으므로, 각각의 함수 호출 표현식에 의해 변한 환경 [eqn: sigma`]가 [eqn: sigma^v `]와 같다는 것을 보이면 된다. 증명 중에 여러 번 사용되는 내용을 *이라 하여 미리 증명하기로 한다.

* 보조정리 1에 의해 [eqn: sigma^v (x_0 )]의 값은 프로그램 수행 중에 덮어씌워지지 않으므로 [eqn: sigma^v (x_0 )=v]이다. 프로그램 [eqn: e_0]의 입력은 [eqn: x_0]뿐이고 [eqn: [x_0 mapsto v](x_0 )]와 [eqn: sigma^v (x_0 )]는 같은 값을 가지므로, [eqn: vdash`]의 왼쪽에 있는 환경을 고려하지 않는다면 [eqn: □[x_0 mapsto v]``vdash``e_0 ``rightarrow``o``□]와  [eqn: □sigma^v ``vdash``e_0 ``rightarrow``o``□]는 똑같다. 다시 말해서 [eqn: □sigma^v ``vdash``e_0 ``rightarrow``o``□]에 나타나는 모든 [eqn: sigma`` vdash`` e`` rightarrow`` o``]에 대해서 [eqn: sigma'`` vdash`` e`` rightarrow`` o'``]이 [eqn: □[x_0 mapsto v]``vdash``e_0 ``rightarrow``o``□]에 나타나고, [eqn: sigma^v``]의 정의에 의해 [eqn: dom(sigma') subseteq dom(sigma^v )]이고 [eqn: dom(sigma')]의 모든 변수 [eqn: x]에 대해 [eqn: sigma'(x)= sigma^v (x)]이다.

각각의 함수 호출 표현식에 대한 증명은 다음과 같다.

1. [eqn: (lambda x.e_1 )~e_2]일 때

[eqn: {sigma^v ~vdash~e_2 ~ rightarrow~v_2 ~~~sigma^v [x_n mapsto v_2 ]~vdash~[x_n / x]e_1 ~rightarrow~ o'} over {sigma^v ~vdash~ (lambdax.e_1 ) e_2 ~rightarrow~ o'}]이 [eqn: □sigma^v ``vdash``e_0 ``rightarrow``o``□]에 나타난다면, * 에서 보인 것처럼 [eqn: {sigma ~vdash~e_2 ~ rightarrow~v_2 ~~~sigma [x_n mapsto v_2 ]~vdash~[x_n / x]e_1 ~rightarrow~ o'} over {sigma ~vdash~ (lambdax.e_1 ) e_2 ~rightarrow~ o'}]이 [eqn: □[x_0 mapsto v] ``vdash``e_0 ``rightarrow``o``□]에 나타나고, [eqn: sigma^v``]의 정의에 의해 [eqn: sigma^v~ (x_n )``=``v_2``]이고 [eqn: sigma``[x_n ``mapsto`` v_2` ](x_n `)``=``v_2]이다. 따라서  [eqn: sigma^v [x_n mapsto v_2 ]= sigma^v``]이다.

2. [eqn: ({rm fix}~f~ lambda x.e_1 )~e_2]일 때

[eqn: {sigma^v ~vdash~e_2 ~ rightarrow~v_2 ~~~sigma^v [f mapsto langle sigma^v , {rm fix}``f``lambda x.e_1 rangle][x_n mapsto v_2 ]``vdash``[x_n / x]e_1 ``rightarrow`` o'} over {sigma^v ~vdash~ ({rm fix}~f~lambdax.e_1 )~ e_2 ~rightarrow~ o'}]이 [eqn: □sigma^v ``vdash``e_0 ``rightarrow``o``□]에 나타난다면, * 에서 보인 것처럼 [eqn: □[x_0 mapsto v] ``vdash``e_0 ``rightarrow``o``□]에 [eqn: {sigma ~vdash~e_2 ~ rightarrow~v_2 ~~~sigma [f mapsto langle sigma , {rm fix}``f``lambda x.e_1 rangle][x_n mapsto v_2 ]``vdash``[x_n / x]e_1 ``rightarrow`` o'} over {sigma ~vdash~ ({rm fix}~f~lambdax.e_1 )~ e_2 ~rightarrow~ o'}]이 나타난다. 또한 [eqn: sigma^v``]의 정의에 의해[eqn: sigma^v (x_n )``=`` sigma[f mapsto langle sigma, {rm fix}~f~ lambda x.e_1 rangle] [x_n mapsto v_2 ](x_n )``=``v_2]이고 [eqn: sigma^v (f``)``]는 [eqn: sigma[f mapsto langle sigma, {rm fix}~f~ lambda x.e_1 rangle] [x_n mapsto v_2 ](f)= langle sigma, {rm fix}~f~ lambda x.e_1 rangle]의 [eqn: sigma]를 [eqn: sigma^v``]로 바꾼 [eqn: langle sigma^v , {rm fix}~f~ lambda x.e_1 rangle]이다. 따라서 [eqn: sigma^v [f mapsto langle sigma^v , {rm fix}~f~ lambda x.e_1 rangle] [x_n mapsto v_2 ] = sigma^v``]이다.

3. [eqn: f~e_2]일 때 ([eqn: f``]는 [eqn: {rm fix}~f~ lambda x.e_1]일 때)

[eqn: {{sigma^v (f) = langle sigma^v , {rm fix}``f``lambda x.e_1 rangle~~~sigma^v ~vdash~e_2 ~ rightarrow~v_2 } atop {~~~sigma^v [f mapsto langle sigma^v , {rm fix}``f``lambda x.e_1 rangle][x_n mapsto v_2 ]``vdash``[x_n / x]e_1 ``rightarrow`` o'}} over {sigma^v ~vdash~ f~ e_2 ~rightarrow~ o'}]이 [eqn: □sigma^v ``vdash``e_0 ``rightarrow``o``□]에 나타나면, * 에 의해 [eqn: {{sigma (f) = langle sigma' , {rm fix}``f``lambda x.e_1 rangle~~~sigma ~vdash~e_2 ~ rightarrow~v_2 } atop {~~~sigma' [f mapsto langle sigma' , {rm fix}``f``lambda x.e_1 rangle][x_n mapsto v_2 ]``vdash``[x_n / x]e_1 ``rightarrow`` o'}} over {sigma ~vdash~ f~ e_2 ~rightarrow~ o'}]이 [eqn: □[x_0 mapsto v] ``vdash``e_0 ``rightarrow``o``□]에 나타난다. 또한 [eqn: sigma^v``]의 정의에 의해 [eqn: sigma^v (x_n )``=`` sigma'[f mapsto langle sigma', {rm fix}~f~ lambda x.e_1 rangle] [x_n mapsto v_2 ](x_n )``=``v_2]이고 [eqn: sigma^v (f``)``]는 [eqn: sigma'[f mapsto langle sigma', {rm fix}~f~ lambda x.e_1 rangle] [x_n mapsto v_2 ](f)= langle sigma', {rm fix}~f~ lambda x.e_1 rangle]의 [eqn: sigma'``]을 [eqn: sigma^v``]로 바꾼 [eqn: langle sigma^v , {rm fix}~f~ lambda x.e_1 rangle]이다. 따라서 [eqn: sigma^v [f mapsto langle sigma^v , {rm fix}~f~ lambda x.e_1 rangle] [x_n mapsto v_2 ] = sigma^v``]이다. □

정의 4 (Post(node)) 유도 과정(derivation tree)을 (1) 왼쪽 부분 과정(subtree) (2) 오른쪽 부분 과정 (3) 루트노드의 순서로 돌아다니면서(postorder traversal) 각 노드 node에 붙인 번호를 Post(node)라 한다.

예를 들어, 다음의 왼쪽 구조를 돌아다니면서 각 노드 node에 대해 Post(node)를 붙이면 오른쪽 구조와 같이 된다:

프로그램 [eqn: e``]에 대한 수행을 [eqn: sigma ``vdash`e ``rightarrow``o``]라고 할 때, 수행 과정 [eqn: □sigma ``vdash``e ``rightarrow``o``□]의 각 노드 node에 붙인 Post(node)는 그 노드의 수행 순서를 나타낸다.

정의 5 ([eqn: e_0 {`_0} atop {\~ } e]) 프로그램 [eqn: e_0]에 대한 분석을 [eqn: hat{rm E}~♤~e_0 ~:~ C_0 `]라고 할 때, 분석 과정 [eqn: □hat{rm E}~♤~e_0 ~:~ C_0 `□]에서 루트노드 [eqn: hat{rm E}~♤~e_0 ~:~ C_0 `]로부터 임의의 노드 [eqn: se~♤~e ~:~ C `]까지의 길이가 [eqn: n``]인 경로(path) [eqn: e_0 {`_n} atop {\~ } e``]를 다음과 같이 정의한다:

프로그램 [eqn: e_0]에 대한 수행을 [eqn: sigma ``vdash`e_0 ``rightarrow``o``]라고 할 때, 수행 과정 [eqn: □sigma ``vdash``e ``rightarrow``o``□]에서 루트노드 [eqn: sigma ``vdash`e_0 ``rightarrow``o``]로부터 임의의 노드 [eqn: sigma' ``vdash`e ``rightarrow``o'``]까지의 길이가 [eqn: n`]인 경로(path) [eqn: e_0 {`_n} atop {\~ } e``]도 비슷하게 정의한다.

보조정리 3 [eqn: x_0]를 입력으로 갑는 프로그램 [eqn: e_0`]의 분석을 [eqn: hat{rm E}~♤~e_0 ~:~ C_0 `]라고 하면, [eqn: □hat{rm E}~♤~e_0 ~:~ C_0 `□]에 나타나는 모든 [eqn: se~♤~e ~:~ C `]는 다음 성질을 만족한다:

임의의 [eqn: v~in~gm(C_0 )(X_0 )]에 대해 (1) [eqn: sigma^v ``vdash`e ``rightarrow``o'``]이 [eqn: □sigma^v ``vdash``e_0 ``rightarrow``o``□]에 존재하고 (2) [eqn: o'~in~gm(C_0 )(se )]이다.

Proof. [eqn: I = gm(C_0 )]라 하자. [eqn: □hat{rm E}~♤~e_0 ~:~ C_0 `□]에 나타나는 규칙 중, {false}를 만들어내는 규칙 ([eqn: se``♤``e``:``]{false})에 대해서는 증명할 필요가 없다. 그 이유는 분석 과정 중에 {false}가 나타나면 그 제약식들의 해가 공집합이 되므로 보조정리 3이 바로 증명되기 때문이다. 분석 과정 [eqn: □hat{rm E}~♤~e_0 ~:~ C_0 `□]에 나타나는 노드 [eqn: se~♤~e~:~C``]의 [eqn: Post``(se``♤``e``:``C`){rm let}atop{=} m]에 대한 귀납법(induction)으로 증명하기로 한다:

m=1인 경우 : Post(node)의 정의에 의해 그 값이 1인 경우는 유도 과정의 루트노드로부터 왼쪽 전제(premise)만을 따라온 잎노드(leaf)이므로, 표현식 [eqn: e``]는 0, [eqn: x], raise E 중 하나이다.

(1)[eqn: sigma^v ``vdash``e ``rightarrow``o'``]이 [eqn: □sigma^v ``vdash``e_0 ``rightarrow``o``□]에 존재한다는 것을 증명해야 한다. [eqn: se~♤~e~:~C``]가 [eqn: □hat{rm E}~♤~e_0 ~:~ C_0 `□]에 나타나므로, [eqn: e_0 {`_n} atop {\~ } e``]가 [eqn: □hat{rm E}~♤~e_0 ~:~ C_0 `□]에 존재한다. 똑같은 [eqn: e_0 {`_n} atop {\~ } e``]가 [eqn: □sigma^v ``vdash``e_0 ``rightarrow``o``□]에도 존재함을 보여서 [eqn: sigma^v ``vdash``e ``rightarrow``o'``]이 [eqn: □sigma^v ``vdash``e_0 ``rightarrow``o``□]에 존재한다는 것을 보인다. [eqn: e_0 {`_n} atop {\~ } e``]의 [eqn: n]에 대한 귀납법으로 증명하기로 한다.

* n=0인 경우 : [eqn: e``]가 [eqn: e_0]인 경우이므로, [eqn: e_0 {`_0} atop {\~ } e_0 ``]가 [eqn: □sigma^v ``vdash``e_0 ``rightarrow``o``□]에 존재한다.

* n=k ([eqn: k ge 1])인 경우 : [eqn: e_0 {`_n'} atop {\~ } e' ``]([eqn: n' < k])가 [eqn: □hat{rm E}~♤~e_0 ~:~ C_0 `□]에 존재할 때 똑같은 [eqn: e_0 {`_n'} atop {\~ } e' ``]([eqn: n' < k])가 [eqn: □sigma^v ``vdash``e_0 ``rightarrow``o``□]에 존재한다면, [eqn: e_0 {`_k} atop {\~ } e ``]가 [eqn: □hat{rm E}~♤~e_0 ~:~ C_0 `□]에 존재할 때 똑같은 [eqn: e_0 {`_k} atop {\~ } e ``]가 [eqn: □sigma^v ``vdash``e_0 ``rightarrow``o``□]에 존재함을 보여야한다. [eqn: e_0 {`_k} atop {\~ } e ``]가 [eqn: □hat{rm E}~♤~e_0 ~:~ C_0 `□]에 존재한다고 하자. [eqn: k ge 1]이므로 [eqn: se~♤~e ~:~ C ``]의 결론 [eqn: se'~♤~e' ~:~ C']이 [eqn: □hat{rm E}~♤~e_0 ~:~ C_0 `□]에 존재하고, 따라서 [eqn: e_0 {`_k-1} atop {\~ } e' ``]이 [eqn: □hat{rm E}~♤~e_0 ~:~ C_0 `□]에 존재하므로 귀납법 가정에 의해 똑같은 [eqn: e_0 {`_k-1} atop {\~ } e' ``]이 [eqn: □sigma^v ``vdash``e_0 ``rightarrow``o``□]에 존재한다. [eqn: e_0]로부터 유도 과정의 왼쪽 전제만을 따라온 경우이므로 [eqn: e``]와 [eqn: e'``]의 가능한 관계는 다음의 두 경우밖에 없다.

- [eqn: e'``]이 [eqn: kappa~e``]이거나 [eqn: kappa^{-1}~e``]인 경우

[eqn: e_0 {`_k-1} atop {\~ } e'``]이 [eqn: □sigma^v ``vdash``e_0 ``rightarrow``o``□]에 존재하므로 [eqn: sigma^v ``vdash``e' ``rightarrow``o''``]이 수행 과정에 존재하고, 의미 구조에 의해 [eqn: sigma^v ``vdash``e' ``rightarrow``o''``]의 하나뿐인 전제 [eqn: sigma^v ``vdash``e ``rightarrow``o'``]이 항상 수행 과정에 존재하므로 [eqn: e_0 {`_k} atop {\~ } e``]가 [eqn: □sigma^v ``vdash``e_0 ``rightarrow``o``□]에 존재한다.

- [eqn: e'``]이 [eqn: (lambda x.e_1 )~e``], [eqn: ({rm fix}~f~ lambda x.e_1 )~e``], [eqn: f~e``] ([eqn: {rm fix}~f~ lambda x.e_1 ``]일 때), [eqn: {rm case}~e~ kappa~e_1 ~e_2``], [eqn: {rm handle}~e~ {rm E}~e_1``] 중 한 가지인 경우

[eqn: e_0 {`_k-1} atop {\~ } e'``]이 [eqn: □sigma^v ``vdash``e_0 ``rightarrow``o``□]에 존재하므로 [eqn: sigma^v ``vdash``e' ``rightarrow``o''``]이 수행 과정에 존재하고, 의미 구조에 의해 [eqn: sigma^v ``vdash``e' ``rightarrow``o''``]의 왼쪽 전제인 [eqn: sigma^v ``vdash``e ``rightarrow``o'``]이 항상 수행 과정에 존재하므로, [eqn: e_0 {`_k} atop {\~ } e``]가 [eqn: □sigma^v ``vdash``e_0 ``rightarrow``o``□]에 존재한다.

(2) [eqn: sigma^v ``vdash``e ``rightarrow``o'``]이 [eqn: □sigma^v ``vdash``e_0 ``rightarrow``o``□]에 존재함을 보였고, 이제 [eqn: o'~in~gm(C_0 )(se)]라는 것을 증명해야 한다. 각 표현식에 대하여 증명하기로 한다.

[C-1a] [eqn: {rm 0}~♤~{rm 0} ~:~ \{rm true \} `]

(1)에 의해 [eqn: sigma^v ``vdash``{rm 0} ``rightarrow``{rm 0}``]이 성립하므로[eqn: {rm 0} ``in`` \{rm 0 \}``]이다.

[C-2a] [eqn: {X}~♤~{rm 0} ~:~ \{{rm 0}~ subseteq~ X \} `]

(1)에 의해 [eqn: sigma^v ``vdash``{rm 0} ``rightarrow``{rm 0}``]이 성립하고[eqn: \{{rm 0}~ subseteq~ X \}~subseteq~C_0 `]이므로 [eqn: {rm 0} ``in`` I(X)``]이다.

[C-3a] [eqn: kappa^{-1}~{X}~♤~{rm 0} ~:~ \{kappa~{rm 0}~ subseteq~ X \} `]

(1)에 의해 [eqn: sigma^v ``vdash``{rm 0} ``rightarrow``{rm 0}``]이 성립하고[eqn: \{kappa~{rm 0}~ subseteq~ X \}~subseteq~C_0 `]이므로 [eqn: kappa~{rm 0} ``in`` I(X)``]이다. 따라서 [eqn: {rm 0} ``in`` I`(kappa^{-1}``X)``]이다.

[NVN-a] [eqn: {se}~♤~x ~:~ \{X~ subseteq~ se \} `~~~se~ not in~ \{hat{rm E}\}]

Post(node)가 1인 경우는 유도 과정의 루트노드로부터 왼쪽 전제만을 따라온 경우이고, 새로운 변수는 함수 호출 규칙의 오른쪽 전제에서만 만들어지므로 [eqn: x`]는 프로그램의 입력인 [eqn: x_0]이다. 보조정리 2에 의해 [eqn: sigma^v (x_0 )]는 프로그램 수행 중에 덮어씌워지지 않으므로 [eqn: sigma^v (x_0 )~=~v``]이다. [eqn: v ~ in`` I( X_0 )]이고 [eqn: \{ X_0~ subseteq``se \}`` subseteq`` C_0]이므로 [eqn: v~ in~ I``(se)]이다.

[RSX-1a] [eqn: hat{rm E}~♤~{rm raise~ E} ~:~ \{ rm true \} `]

(1)에 의해 [eqn: sigma^v ``vdash``{rm raise~ E} ``rightarrow``hat{rm E}``]이 성립하므로[eqn: hat{rm E} ``in`` \{hat {rm E} \}``]이다.

m=k ([eqn: k > 1])인 경우 : 분석 과정 [eqn: □hat{rm E}~♤~e_0 ~:~ C_0 `□]에 나타나는 [eqn: se~♤~e ~:~ C ``]에 대해서 다음을 증명한다: [eqn: Post``(se'~♤~e' ~:~ C') ``]이 [eqn: k `] 미만인 [eqn: se'~♤~e' ~:~ C' ``]에 대해서 [eqn: sigma^v ``vdash``e' ``rightarrow``o''``]이 [eqn: □sigma^v ``vdash``e_0 ``rightarrow``o``□]에 존재하고 [eqn: o''~in~I`(se')]이면, (1) [eqn: sigma^v ``vdash``e ``rightarrow``o'``]이 [eqn: □sigma^v ``vdash``e_0 ``rightarrow``o``□]에 존재하고 (2) [eqn: o'~in~I`(se)]이다.

(1)[eqn: sigma^v ``vdash``e ``rightarrow``o'``]이 [eqn: □sigma^v ``vdash``e_0 ``rightarrow``o``□]에 존재한다는 것을 증명해야 한다. [eqn: se~♤~e~:~C``]가 [eqn: □hat{rm E}~♤~e_0 ~:~ C_0 `□]에 나타나므로, [eqn: e_0 {`_n} atop {\~ } e``]가 [eqn: □hat{rm E}~♤~e_0 ~:~ C_0 `□]에 존재한다. 똑같은 [eqn: e_0 {`_n} atop {\~ } e``]가 [eqn: □sigma^v ``vdash``e_0 ``rightarrow``o``□]에도 존재함을 보여서 [eqn: sigma^v ``vdash``e ``rightarrow``o'``]이 [eqn: □sigma^v ``vdash``e_0 ``rightarrow``o``□]에 존재한다는 것을 보인다. [eqn: e_0 {`_n} atop {\~ } e``]의 [eqn: n]에 대한 귀납법으로 증명하기로 한다.

* n=0인 경우 : [eqn: e``]가 [eqn: e_0]인 경우이므로, [eqn: e_0 {`_0} atop {\~ } e_0 ``]가 [eqn: □sigma^v ``vdash``e_0 ``rightarrow``o``□]에 존재한다.

* n=k ([eqn: k ge 1])인 경우 : [eqn: e_0 {`_n'} atop {\~ } e'``]([eqn: n' < k])가 [eqn: □hat{rm E}~♤~e_0 ~:~ C_0 `□]에 존재할 때 똑같은 [eqn: e_0 {`_n'} atop {\~ } e'``]([eqn: n' < k])가 [eqn: □sigma^v ``vdash``e_0 ``rightarrow``o``□]에 존재한다면, [eqn: e_0 {`_k} atop {\~ } e``]가 [eqn: □hat{rm E}~♤~e_0 ~:~ C_0 `□]에 존재할 때 똑같은 [eqn: e_0 {`_k} atop {\~ } e``]가 [eqn: □sigma^v ``vdash``e_0 ``rightarrow``o``□]에 존재함을 보여야한다.

[eqn: e_0 {`_k} atop {\~ } e``]가 [eqn: □hat{rm E}~♤~e_0 ~:~ C_0 `□]에 존재한다고 하자. [eqn: k ge 1]이므로 [eqn: se~♤~e ~:~ C ``]의 결론 [eqn: se'~♤~e' ~:~ C']이 [eqn: □hat{rm E}~♤~e_0 ~:~ C_0 `□]에 존재하고, 따라서 [eqn: e_0 {`_k-1} atop {\~ } e'``]이 [eqn: □hat{rm E}~♤~e_0 ~:~ C_0 `□]에 존재하므로 귀납법 가정에 의해 똑같은 [eqn: e_0 {`_k-1} atop {\~ } e'``]이 [eqn: □sigma^v ``vdash``e_0 ``rightarrow``o``□]에 존재한다. [eqn: e``]와 [eqn: e'``]의 가능한 각 경우에 대하여 증명하기로 한다. 각 함수 호출 표현식에서 새로 만들어내는 변수의 이름은 의미 구조에서 만드는 이름과 분석 규칙에서 만드는 이름이 서로 같다고 가정한다.

- [eqn: e'``]이 [eqn: kappa~e``]이거나 [eqn: kappa^{-1}~e``]인 경우

[eqn: e_0 {`_k-1} atop {\~ } e'``]이 [eqn: □sigma^v ``vdash``e_0 ``rightarrow``o``□]에 존재하므로 [eqn: sigma^v ``vdash``e' ``rightarrow``o''``]이 수행 과정에 존재하고, 의미 구조에 의해 [eqn: sigma^v ``vdash``e' ``rightarrow``o''``]의 하나뿐인 전제 [eqn: sigma^v ``vdash``e ``rightarrow``o'``]이 항상 수행 과정에 존재하므로 [eqn: e_0 {`_k} atop {\~ } e``]가 [eqn: □sigma^v ``vdash``e_0 ``rightarrow``o``□]에 존재한다.

- [eqn: e'``]이 [eqn: (lambda x.e_1 )~e``], [eqn: ({rm fix}~f~ lambda x.e_1 )~e``], [eqn: f~e``] ([eqn: {rm fix}~f~ lambda x.e_1 ``]일 때), [eqn: {rm case}~e~ kappa~e_1 ~e_2``], [eqn: {rm handle}~e~ {rm E}~e_1``] 중 한 가지인 경우

[eqn: e_0 {`_k-1} atop {\~ } e'``]이 [eqn: □sigma^v ``vdash``e_0 ``rightarrow``o``□]에 존재하므로 [eqn: sigma^v ``vdash``e' ``rightarrow``o''``]이 수행 과정에 존재하고, 의미 구조에 의해 [eqn: sigma^v ``vdash``e' ``rightarrow``o''``]의 왼쪽 전제인 [eqn: sigma^v ``vdash``e ``rightarrow``o'``]이 항상 수행 과정에 존재하므로, [eqn: e_0 {`_k} atop {\~ } e``]가 [eqn: □sigma^v ``vdash``e_0 ``rightarrow``o``□]에 존재한다.

- [eqn: e'``]이 [eqn: (lambda x.e_2 )~e_1 ``], [eqn: ({rm fix}~f~ lambda x.e_2 )~e_1 ``], [eqn: f~e_1 ``] ([eqn: {rm fix}~f~ lambda x.e_2 ``]일 때) 중 하나이고 [eqn: e``]가 [eqn: [x_n /x]e_2 ``]인 경우

[eqn: X_n ~♤~e_1 ~:~ C_1 `]이 [eqn: se' ~♤~e' ~:~ C' `]의 왼쪽 전제이므로 [eqn: Post~(X_n ~♤~e_1 ~:~ C_1 )`]이 [eqn: Post~(se ~♤~e ~:~ C) `]보다 작다. 따라서 Post(node)에 대한 귀납법 가정에 의해 [eqn: sigma^v ``vdash``e_1 ``rightarrow``v_1 ``]이 [eqn: □sigma^v ``vdash``e_0 ``rightarrow``o``□]에 존재하고 [eqn: v_1 ~in~I`(X_n )]이다. [eqn: e_0 {`_k-1} atop {\~ } e'``]이 [eqn: □sigma^v ``vdash``e_0 ``rightarrow``o``□]에 존재하므로 [eqn: sigma^v ``vdash``e' ``rightarrow``o''``]이 수행 과정에 존재하고, [eqn: e_1`]을 수행하는 중에 예외상황이 발생하지 않으므로 의미 구조에 의해 [eqn: sigma^v ``vdash``e ``rightarrow``o'``]이 수행 과정에 존재한다. 따라서 [eqn: e_0 {`_k} atop {\~ } e``]가 [eqn: □sigma^v ``vdash``e_0 ``rightarrow``o``□]에 존재한다.

- [eqn: e'``]이[eqn: {rm case}~e_1 ~ kappa~e ~e_2``]인 경우

[eqn: kappa~X ~♤~e_1 ~:~ C_1 `]이 [eqn: se' ~♤~e' ~:~ C' `]의 왼쪽 전제이므로 [eqn: Post~(kappa~X ~♤~e_1 ~:~ C_1 )`]이 [eqn: Post~(se ~♤~e ~:~ C) `]보다 작다. 따라서 Post(node)에 대한 귀납법 가정에 의해 [eqn: sigma^v ``vdash``e_1 ``rightarrow``v_1 ``]이 [eqn: □sigma^v ``vdash``e_0 ``rightarrow``o``□]에 존재하고 [eqn: v_1 ~in~I`(kappa ~X )]이다. [eqn: e_0 {`_k-1} atop {\~ } e'``]이 [eqn: □sigma^v ``vdash``e_0 ``rightarrow``o``□]에 존재하므로 [eqn: sigma^v ``vdash``e' ``rightarrow``o''``]이 수행 과정에 존재하고, [eqn: e_1`]의 값이 [eqn: kappa``]로 시작하므로 의미 구조에 의해 [eqn: sigma^v ``vdash``e ``rightarrow``o'``]이 수행 과정에 존재한다. 따라서 [eqn: e_0 {`_k} atop {\~ } e``]가 [eqn: □sigma^v ``vdash``e_0 ``rightarrow``o``□]에 존재한다.

- [eqn: e'``]이[eqn: {rm case}~e_1 ~ kappa~e_2 ~e``]인 경우

[eqn: bar{ kappa}~X ~♤~e_1 ~:~ C_1 `]이 [eqn: se' ~♤~e' ~:~ C' `]의 왼쪽 전제이므로 [eqn: Post~(bar{kappa}~X ~♤~e_1 ~:~ C_1 )`]이 [eqn: Post~(se ~♤~e ~:~ C) `]보다 작다. 따라서 Post(node)에 대한 귀납법 가정에 의해 [eqn: sigma^v ``vdash``e_1 ``rightarrow``v_1 ``]이 [eqn: □sigma^v ``vdash``e_0 ``rightarrow``o``□]에 존재하고 [eqn: v_1 ~in~I`(bar{kappa} ~X )]이다. [eqn: e_0 {`_k-1} atop {\~ } e'``]이 [eqn: □sigma^v ``vdash``e_0 ``rightarrow``o``□]에 존재하므로 [eqn: sigma^v ``vdash``e' ``rightarrow``o''``]이 수행 과정에 존재하고, [eqn: e_1`]의 값이 [eqn: kappa``]로 시작하지 않으므로 [eqn: sigma^v ``vdash``e ``rightarrow``o'``]이 수행 과정에 존재한다. 따라서 [eqn: e_0 {`_k} atop {\~ } e``]가 [eqn: □sigma^v ``vdash``e_0 ``rightarrow``o``□]에 존재한다.

- [eqn: e'``]이[eqn: {rm handle}~e_1 ~ {rm E}~e``]인 경우

[eqn: hat{rm E} ~♤~e_1 ~:~ C_1 `]이 [eqn: se' ~♤~e' ~:~ C' `]의 왼쪽 전제이므로 [eqn: Post~(hat{rm E} ~♤~e_1 ~:~ C_1 )`]이 [eqn: Post~(se ~♤~e ~:~ C) `]보다 작다. 따라서 Post(node)에 대한 귀납법 가정에 의해 [eqn: sigma^v ``vdash``e_1 ``rightarrow``o_1 ``]이 [eqn: □sigma^v ``vdash``e_0 ``rightarrow``o``□]에 존재하고 [eqn: o_1 ~in~I`(hat{rm E} )]이다. [eqn: e_0 {`_k-1} atop {\~ } e'``]이 [eqn: □sigma^v ``vdash``e_0 ``rightarrow``o``□]에 존재하므로 [eqn: sigma^v ``vdash``e' ``rightarrow``o''``]이 수행 과정에 존재하고, [eqn: e_1`]을 수행하는 중에 예외상황 E가 발생하므로 [eqn: sigma^v ``vdash``e ``rightarrow``o'``]이 수행 과정에 존재한다. 따라서 [eqn: e_0 {`_k} atop {\~ } e``]가 [eqn: □sigma^v ``vdash``e_0 ``rightarrow``o``□]에 존재한다.

(2) [eqn: se~♤~e ~:~ C ``]에 대하여 [eqn: sigma^v ``vdash``e ``rightarrow``o'``]이 [eqn: □sigma^v ``vdash``e_0 ``rightarrow``o``□]에 존재함을 보였고, 이제 [eqn: o'~in~gm(C_0 )(se)]라는 것을 증명해야 한다. 몇 가지 대표적인 경우에 대하여 증명하고, 비슷하게 증명되는 나머지 경우에 대하여는 부록 A에서 증명하기로 한다.

[C-1a] [eqn: {rm 0}~♤~{rm 0} ~:~ \{rm true \} `]

(1)에 의해 [eqn: sigma^v ``vdash``{rm 0} ``rightarrow``{rm 0}``]이 성립하므로[eqn: {rm 0} ``in`` \{rm 0 \}``]이다.

[NVN-a] [eqn: {se}~♤~x ~:~ \{X~ subseteq~ se \} `~~~se~ not in~ \{hat{rm E}\}]

①  [eqn: x``]가 프로그램의 입력 [eqn: x_0]일 때

보조정리 2에 의해 [eqn: sigma^v (x_0 )]는 프로그램 수행 중에 덮어씌워지지 않으므로 [eqn: sigma^v (x_0 )~=~v``]이다. [eqn: v ~ in`` I( X_0 )]이고 [eqn: \{ X_0~ subseteq``se \}`` subseteq`` C_0]이므로 [eqn: v~ in~ I``(se)]이다.

②  [eqn: x``]가 가 함수 호출 표현식에서 만들어진 변수 [eqn: x_n]일 때

[eqn: {X_n ~♤~e_2 ~ :~C_1 ~~~se_n~ ♤~[x_n / x]e_3 ~:~ C_2 } over {se_n ~♤~ e_1 ~ e_2 ~:~ C_3}] ([eqn: e_1]이 [eqn: lambda x.e_3]이거나 [eqn: {rm fix}~f~lambda x.e_3] 또는 [eqn: f``]일 때)이 [eqn: x_n]을 만들어내는 규칙이라 하자. [eqn: se ~♤~e ~:~ C `]는 오른쪽 전제인 [eqn: se_n ~♤~[x_n /x]e_3 ~:~ C_2 `] 의 분석 과정 중에 나타나므로, Post(node)의 정의에 의해  왼쪽 전제의 [eqn: Post``(X_n ~♤~e_2 ~:~ C_1 )`]은 [eqn: k``]미만이다. 따라서 귀납법 가정에 의해, [eqn: sigma^v ``vdash``e_2 ``rightarrow``v_2 ``]가 [eqn: □sigma^v ``vdash``e_0 ``rightarrow``o``□]에 존재하고 [eqn: v_2`` in`` I``(X_n )]이다. 함수 호출 표현식의 의미 구조에 의해 [eqn: sigma^v`` [x_n mapsto`` v_2 ] ``vdash``[x_n / x]e_3 ``rightarrow``o' ``]이 수행 과정에 존재하므로, [eqn: sigma^v``]의 정의에 의해 [eqn: sigma^v (x_n ``)~=~v_2 ``]이다. [eqn: v_2 ~ in`` I``( X_n `)]이고 [eqn: \{ X_n~ subseteq``se \}`` subseteq`` C_0]이므로 [eqn: v_2~ in~ I``(se)]이다.

[RSX-1a] [eqn: hat{rm E}~♤~{rm raise~~E} ~:~ \{rm true \} `]

(1)에 의해 [eqn: sigma^v ``vdash``{rm raise~~E} ``rightarrow``hat{rm E}``]이 성립하므로[eqn: hat{rm E} ``in`` \{hat {rm E} \}``]이다.

[CONN-1a] [eqn: {kappa^{-1}~X ~♤~e ~ :~C } over {X ~♤~ kappa ~ e ~:~ C}]

Post(node)의 정의에 의해 전제의 [eqn: Post``(kappa^{-1}``X ~♤~e ~:~ C )`]는 [eqn: k``]미만이므로, 가정에 의해서 [eqn: sigma^v ``vdash``e ``rightarrow``v'``]이 성립하고 [eqn: v' ``in`` I``(kappa^{-1}``X)``]이다. 따라서 [eqn: {sigma^v ``vdash``e ``rightarrow``v'`` } over {sigma^v ``vdash``kappa``e ``rightarrow``kappa``v'``}]이 성립하고 [eqn: kappa``v' ``in`` I``(X)``]이다.

[DCONN-1a] [eqn: {kappa~Y ~♤~e ~ :~C } over {kappa'``X ~♤~ kappa^{-1}``e ~:~ C~ cup`` \{ Y``subseteq``kappa'~X \} }~"새 변수 "Y]

가정에 의해서 [eqn: sigma^v ``vdash``e ``rightarrow``v'``]이 성립하고 [eqn: v' ``in`` I``(kappa``Y)``]이다. [eqn: v'~=kappa``v''``]이라 하면 [eqn: {sigma^v ``vdash``e ``rightarrow``kappa``v''`` } over {sigma^v ``vdash``kappa^{-1}``e ``rightarrow``v''``}]이 성립한다. [eqn: v' ``in`` I``(kappa``Y)``]이면 [eqn: kappa^{-1}``v' ``in`` I``(Y)``]이고 [eqn: \{ Y~ subseteq``kappa'``X \}`` subseteq`` C_0]이므로, [eqn: v'' ``in`` I``(kappa'``X)``]이다.

[APP-1a] [eqn: {X_n ~♤~e_2 ~ :~C_1 ~~se~ ♤~[x_n / x]e_1 ~:~ C_2 } over {se ~♤~ (lambda x.e_1 )~ e_2 ~:~ C_1~ cup`` C_2 }~"새 번호 "n]

가정에 의해서, [eqn: sigma^v ``vdash``e_2 ``rightarrow``v_2``]와 [eqn: sigma^v ``vdash``[x_n /x]e_1 ``rightarrow``o'``]이 성립하고 [eqn: v_2 ``in`` I``(X_n )``]이며 [eqn: o' ``in`` I``(se )``]이다. 보조정리 2에 의해 [eqn: sigma^v``]는 프로그램 수행 중에 변하지 않으므로 [eqn: sigma^v``[x_n mapsto v_2 ]~=~sigma^v``]이다. 따라서 [eqn: {sigma^v ``vdash``e_2 ``rightarrow``v_2 ``~~~sigma^v``[x_n mapsto v_2 ] ``vdash``[x_n / x]e ``rightarrow``o'`` } over {sigma^v ``vdash``(lambdax.e_1 )``e_2 ``rightarrow``o'``}]이 성립하고, [eqn: o' ~ in`` I``( se )]이다.

[CASE-1a] [eqn: {kappa``X ~♤~e_1 ~ :~C_1 ~~se~ ♤~e_2 ~:~ C_2 } over {se ~♤~ {rm case} e_1 ``kappa`` e_2 ``e_3~:~ C_1~ cup`` C_2 }~"새 변수 " X]

가정에 의해서 [eqn: sigma^v ``vdash``e_1 ``rightarrow``v_1`], [eqn: sigma^v ``vdash``e_2 ``rightarrow``o'`]이 성립하고 [eqn: v_1 ``in`` I``(kappa``X )`], [eqn: o' ``in`` I``(se )`]이다. [eqn: v_1 `=kappa`v'`]이라 하면, [eqn: {sigma^v ``vdash``e_1 ``rightarrow``kappa``v'~~sigma^v ``vdash``e_2 ``rightarrow``o'`` } over {sigma^v ``vdash``{rm case}~e_1~ kappa``e_2``e_3 ``rightarrow``o'``}]이 성립하고 [eqn: o' ``in`` I``(se )``]이다.

[HNDL-a] [eqn: {hat{rm E} ~♤~e_1 ~ :~C_1 ~~~se~ ♤~e_2 ~:~ C_2 } over {se ~♤~ {rm handle}~ e_1 ~{rm E}~ e_2 ~:~ C_1~ cup`` C_2 }]

가정에 의해서 [eqn: sigma^v ``vdash``e_1 ``rightarrow``o_1`], [eqn: sigma^v ``vdash``e_2 ``rightarrow``o'`]이 성립하고 [eqn: o_1 ``in`` \{hat{rm E} \}`]이며 [eqn: o' ``in`` I``(se )`]이다. 따라서 [eqn: {sigma^v ``vdash``e_1 ``rightarrow``hat{rm E}~~sigma^v ``vdash``e_2 ``rightarrow``o'`` } over {sigma^v ``vdash``{rm handle}~e_1~ {rm E}``e_2 ``rightarrow``o'``}]이 성립하고 [eqn: o' ``in`` I``(se )``]이다. □

정리 1 (보증성) [eqn: x_0]를 입력으로 갑는 프로그램 [eqn: e_0`]의 분석을 [eqn: hat{rm E}~♤~e_0 ~:~ C_0 `]라고 하면, 임의의 [eqn: v``in``gm``(C_0 )(X_0 )]에 대해서 [eqn: [x_0 mapsto v] ``vdash`e_0 ``rightarrow``hat{rm E}``]이 성립한다.

Proof. 보조정리 3에 의해 (1) [eqn: sigma^v ``vdash``e_0 ``rightarrow``o`]가 [eqn: □sigma^v ``vdash``e_0 ``rightarrow``o``□]에 존재하고 (2) [eqn: o``in``gm`(C_0 )(hat{rm E})``=`` \{hat{rm E} \}]이므로, [eqn: sigma^v ``vdash``e_0 ``rightarrow``hat{rm E}`]이 성립한다. 보조정리 2에 의해 [eqn: sigma^v (x_0 )]는 프로그램 수행 중에 덮어씌워지지 않으므로 [eqn: sigma^v (x_0 )~=~v``]이다. 프로그램 [eqn: e_0`]의 입력이 [eqn: x_0`]뿐이고 [eqn: [x_0 mapsto v](x_0 )`]와 [eqn: sigma^v (x_0 )]는 같은 값을 가지므로, [eqn: [x_0 mapsto v]`]만을 가지고 [eqn: e_0`]를 실행시켜도 [eqn: sigma^v``]를 가지고 실행시키는 것과 같은 결과를 만들어낸다. 그러므로 [eqn: [x_0 mapsto v] ``vdash`e_0 ``rightarrow``hat{rm E}``]이 성립한다. □

예

몇 가지 예를 사용하여, 주어진 프로그램에 대한 분석이 어떻게 이루어지는지를 설명한다. 언어 L에서는 데이타 타입 선언(datatype)을 제공하지 않지만, 예로 든 프로그램에서 다루는 데이타를 명확히 하기 위하여 데이타 타입 선언을 사용하기로 한다.

예 1

그림 6에는 주어진 표현식에 대해 적용 가능한 규칙이 여러 가지가 존재하므로, 주어진 프로그램에 대한 유도 과정도 여러 가지가 존재할 수 있다. 첫번째 예에서는 다음 프로그램에 대해 만들어질 수 있는 모든 유도 과정을 보여준다. 다음은 입력값 [eqn: x``]가 A라는 이름의 데이타일 경우에 예외상황 E를 발생시키고, 그렇지 않을 때는 입력값을 결과값으로 하는 프로그램이다.

case 표현식이 예외상황 E를 발생시키기 위해서 적용 가능한 규칙은 [CASEX-a], [CASE-1a], [CASE-2a]이다.

□가능한 유도 과정:

[eqn: {hat{rm E}~♤~x~ :~ \{rm false \} } over {hat{rm E}~♤~{rm case}~x ~{rm A}~{rm (raise~E)} ~x ~:~ \{rm false \} }]

이 유도 과정은 [CASEX-a] 규칙을 적용하는 경우이다. [eqn: x``]가 예외상황 E를 발생시킬 수 없으므로 [eqn: \{ rm false \}`]라는 제약식이 만들어진다.

□또 다른 유도 과정:

[eqn: {{rm A}~Y~♤~x~ :~ \{X``subseteq{rm A}`Y \}~~~ hat{rm E}~♤~{rm raise~E}~ :~ \{rm true \} } over {hat{rm E}~♤~{rm case}~x ~{rm A}~{rm (raise~E)} ~x ~:~ \{X``subseteq{rm A}`Y,`` rm true \} }]

이 유도 과정은 [CASE-1a] 규칙을 적용하는 경우이다. [eqn: x``]가 [eqn: {rm A}`` Y``]에 포함되기 위해서는 [eqn: X``]가 [eqn: {rm A}`Y``]에 포함되어야 한다. raise E는 항상 예외상황 [eqn: hat{rm E}`]를 발생시키므로 [eqn: \{ rm true \}`]라는 제약식이 만들어진다. 전체 프로그램에 대한 제약식은 다음과 같고:

[eqn: \{X``subseteq{rm A}`Y,`` rm true \}],

아무런 제약이 없는 변수의 가장 큰 해는 전체집합  [eqn: U``]이므로, 위 제약식의 가장 큰 해는 [eqn: X`=`` {rm A}``U``]이다. 따라서, 프로그램의 입력값 [eqn: x``]에 A라는 이름의 데이타를 대입하여 프로그램을 수행시키면 예외상황 E가 발생하게 된다.

□마지막으로 가능한 유도 과정:

[eqn: {bar{rm A}~Y~♤~x~ :~ \{X``subseteq bar{rm A}`Y \}~~~ hat{rm E}~♤~x~ :~ \{rm false \} } over {hat{rm E}~♤~{rm case}~x ~{rm A}~{rm (raise~E)} ~x ~:~ \{X``subseteq bar{rm A}`Y,`` rm false \} }]

이 유도 과정은 [CASE-2a] 규칙을 적용하는 경우이다. [eqn: x``]가 [eqn: bar{rm A}`` Y``]에 포함되기 위해서는 [eqn: X``]가 [eqn: bar{rm A}``Y``]에 포함되어야 한다. [eqn: x``]는 예외상황을 E를 발생시킬 수 없으므로 [eqn: \{ rm false \}`]라는 제약식이 만들어진다.

예 2

다음 프로그램에서 함수 [eqn: f``]는 입력값이 Zero라는 이름의 데이타인 경우에는 예외상황 E를 발생하고, 입력값이 Suc이라는 이름의 데이타인 경우에는 입력값보다 하나 작은 수를 입력값으로 하여 자기 자신을 다시 호출하고, 그 외의 경우에는 입력값을 결과값으로 한다.

이 예에서는 재귀함수 호출이 한번만 이루어지는 유도 과정을 살펴보기로 한다. (규칙 [APP-3a]에서의 [eqn: N``]을 1로 정한다.)

주어진 프로그램에 그림 6에 있는 규칙 [APP-2a]를 적용하면 다음과 같다:

[eqn: {X~♤~y~ :~ \{Y``subseteq X \}~~~ hat{rm E}~♤~e_1 ~ :~ C_1 } over {hat{rm E}~♤~{rm (fix}~f ~lambdax.e_1 {rm )}~y ~:~ \{Y``subseteq X \}~cup~C_1~ }],

[eqn: hat{rm E}~♤~e_1 ~:~ C_1 `]에 규칙 [CASE-2a]를 적용하면 다음과 같고:

[eqn: hat{rm E}~♤~e_2 ~:~ C_2 `]에 규칙 [APP-3a]와 [DCONN-4a], [NVN-a]를 적용하면 다음과 같다:

[eqn: hat{rm E}~♤~[v``/``x]``e_1 ~:~ C_3 `]에 규칙 [CASE-1a]와 [NVN-a], [RSX-1a]를 적용한 유도 과정은 다음과 같다:

따라서 전체 프로그램에 대한 제약식은 다음과 같고:

[eqn: \{Y``subseteq X,``X``subseteq bar{rm Zero}``Z,``X``subseteq {rm Suc}``V,`` V``subseteq {rm Zero}``W,`` rm true \}],

위 제약식의 가장 큰 해는 다음과 같다:

[eqn: Y= {rm Suc`` (Zero``} U{rm )},``X= {rm Suc`` (Zero``} U{rm )},`` Z= U,`` W= U,`` V= {rm Zero}``U.]

테스트 데이타 [eqn: {rm Suc`` (Zero``} U{rm )}]를 입력으로 하여 프로그램을 수행시키면 재귀함수 [eqn: f``]는 한 번만 호출되고 프로그램은 예외상황 E를 발생시킨다.

결 론

본 논문에서는 프로그램 내의 예외상황을 모두 발생시키는 테스트 데이타를 자동으로 생성해주는 분석 방법을 제안하였다. 테스트 데이타는 집합 제약식을 이용하여 만들어진다. 프로그램의 구조를 나타내는 구문트리(syntax tree)와 프로그램에서 특정 예외상황이 발생한다는 초기 조건을 가지고, 구문트리의 루트노드(root)부터 잎노드(leaves)를 향하여 분석해가면서 프로그램 변수들에 대한 제약식을 만들어간다. 테스트 데이타 생성 분석에서 사용하는 집합 제약식은 이미 존재하는 알고리즘을 사용하여 그 해를 구할 수 있다[14].

집합 제약식을 만들어가는 것은 프로그램 수행의 한 경우를 거꾸로 추적해가면서 프로그램 내의 각 표현식에 대한 필요조건(a necessary-condition)을 만들어가는 것이다. 프로그램 수행을 따라가다가 여러 가지 수행이 가능한 경우에는, 단 하나의 수행만을 따라간다. 따라서 여러 가지 수행 가능성을 하나의 수행으로 뭉뚱그릴 때 어쩔 수 없이 포함되는 잘못된 값들(approximation) ("반드시(must)" 정보가 아니라 "아마도(may)" 정보)은 만들어내지 않는다.

집합 제약식을 만들어가는 것이 프로그램 수행의 각 경우를 따라가는 것이므로 가능한 모든 수행을 다 따라가야겠지만, 대부분의 수행은 미리 제외될 수 있을 것이다. 그 이유는 첫째로, 예외상황을 발생시키는 표현식이 프로그램 내에 많지 않아서, 대부분의 제약식들은 모순(contradiction)을 만들어내어 고려할 필요가 없어질 것이기 때문이다. 둘째로, 정해진 예외상황을 발생시키는 입력값을 하나만 찾으면 더 이상의 분석을 할 필요가 없기 때문이다. 마지막으로, 제약식을 만들어내는 데에는 입력으로 받은 프로그램의 크기에 비례하는 시간만을 필요로 하기 때문이다. 이것은 재귀함수 호출에 대해서 함수 내용을 따라가는 횟수를 제한하기 때문이다.

분석 결과로 얻은 값을 입력으로 하여 프로그램을 수행시키면 지정한 예외상황이 꼭 발생한다는 것을 엄밀하게 증명하였다. 재귀함수 호출 횟수를 임의로 제한함으로 해서 가능한 테스트 데이타를 찾아내지 못할 수도 있게 된다. 하지만, 테스트 데이타를 찾지 못하더라도 분석의 보증성 (분석으로 얻은 테스트 데이타를 입력으로 하여 프로그램을 수행시키면 정해진 예외상황이 발생한다)은 여전히 성립한다.

테스트 데이타 생성 분석을 실제적인 함수형 언어에 적용

본 논문에서 제안한 분석 방법을 실제적인 함수형 언어에 적용하려면, 다음과 같은 문제점들을 고려해야 한다:

□실제적인 함수형 언어에서는 함수가 다른 함수의 인수나 결과값으로 전달될 수 있고 메모리에 저장될 수도 있는 등, 다른 값들과 차이없이 사용된다. 그러므로 테스트 데이타 생성 분석을 하기 전에 프로그램의 함수 흐름 분석이 먼저 이루어져야 한다. 테스트 데이타 생성 분석이 각 표현식에 대해  꼭 필요한 제약식만을 만들어내기 위해서는, 함수 흐름 분석도 꼭 필요한 정보만을 모아야 한다. 즉, 함수값이 확실한 것만을 모아야 한다.

□ 실제적인 함수형 언어에서는 발생되기 전의 예외상황이 함수의 인수나 결과값으로 전달될 수 있고 메모리에 저장되었다가 꺼내서 사용될 수 있는 등, 다른 값들과 차이없이 사용된다. 또한 예외상황은 함수나 다른 예외상황을 비롯한 값을 인수로 가질 수도 있다. 그러므로 테스트 데이타 생성 분석은 예외상황 값의 흐름을 다른 값의 흐름과 함께 표현할 수 있어야 한다. 이러한 확장은 예외상황 분석[6]에서와 마찬가지로 이루어질 수 있을 것이다.

참고 자료

[1]	Robin Milner, Mads Tofte, Robert Harper, and David MacQueen. The Definition of Standard ML (Revised). MIT Press, 1997.

[2]	Luca Cardelli, J. Donahue, Michael Jordan, B. Kalsow, and Greg Nelson. The modula-3 type system. In ACM Symposium on Principles of Programming Languages, pages 202-212, Austin, TX, January 1989.

[3]	James Gosling, Bill Joy, and Guy L. Jr. Steele. The Java Language Specification (Java Series). Addison-Wesley, September 1996.

[4]	A. Nico Habermann and Dewayne E. Perry. Ada for Experienced Programmers. Addison-Wesley, 1983.

[5]	Ariane 5: Flight 501 Failure. http://www.esrin.esa.it/htdocs/tidc/Press/Press96/ariane5rep.html, July 1996.

[6]	Kwangkeun Yi and Sukyoung Ryu. Towards a cost-effective estimation of uncaught exceptions in SML programs. In Lecture Notes in Computer Science, volume 1302, pages 98-113. Springer-Verlag, proceedings of the 4th international static analysis symposium edition, 1997.

[7]	Kwangkeun Yi and Sukyoung Ryu. A cost-effective esimtation of uncaught exceptions in Standard ML programs. Theoretical Computer Science, (invited submission).

[8]	Francois Pessaux and Xavier Leroy. Type-based analysis of uncaught exceptions. In ACM Symposium on Principles of Programming Languages, pages 276-290, January 1999.

[9]	Kwangkeun Yi and Sukyoung Ryu. SML/NJ Exception Analyzer 0.98. http://compiler.kaist.ac.kr/pub/exna/exna-README.html, December 1998.

[10]	G. Kahn. Natural semantics. In K. Fuchi and M. Nivaat, editors, Programming of Future Generation Computers, pages 237-257. Elsevier Science Publishers (North-Holland), 1988.

[11]	Nevin Heintze and Joxan Jaffar. A finite presentation theorem for approximating logic programs. Technical Report IBM Technical Report RC 16089 (# 71415), IBM, August 1990.

[12]	Nevin Heintze and Joxan Jaffar. A decision procedure for a class of set constraints. Technical Report CMU-CS-91-110, Carnegie-Mellon University, February 1991.

[13]	Witold Charatonik and Andreas Podelski. Solving set constraints for greatest models. Technical Report MPI-I-97-2-004, Max-Planck-Institut fur Informatik, April 1997.

[14]	Witold Charatonik and Andreas Podelski. Co-definite set constraints. In Lecture Notes in Computer Science, volume 1379, pages 211-225. Springer-Verlag, Proceedings of the 9th International Conference on Rewriting Techniques and Applications - RTA'98 edition, 1998.

[15]	P. Devienne, J. M. Talbot, and S. Tison. Solving classes of set constraints with tree automata. Technical Report IT-303, Laboratoire d'Informatique Fondamentale de Lille, May 1997.

[16]	Bokdan Korel. Automated software test data generation. IEEE Transactions on Software Engineering, 16(8):870-879, August 1990.

[17]	Richard A. DeMillo and A. Jefferson Offutt. Constraint-based automatic test data generation. IEEE Transactions on Software Engineering, 17(9):900-910, September 1991.

[18]	A. Jefferson Offutt, Zhenyi Jin, and Jie Pan. The dynamic domain reduction approach to test data generation. Software Practice and Experience, 1999.

[19]	Janis Bi\u{c}evskis, Juris Borzovs, Uldis Straujums, Andris Zarins, and JR. Edward F. Miller. SMOTL - a system to construct samples for data processing program debugging. IEEE Transactions on Software Engineering, 5:60-66, January 1979.

[20]	Lori A. Clarke. A system to generate test data and symbolically execute programs. IEEE Transactions on Software Engineering, 2(3):215-222, September 1976.

[21]	William E. Howden. Symbolic testing and the {DISSECT} symbolic evaluation system. IEEE Transactions on Software Engineering, 4(4):266-278, 1977.

[22]	C. V. Ramamoorthy, Siu bun F. Ho, and W. T. Chen. On the automated generation of program test data. IEEE Transactions on Software Engineering, 2(4):293-300, December 1976.

[23]	Juris Borzovs, Audris Kalnins, and Inga Medvedis. Automatic construction of test sets: Practical approach. volume 502 of Lecture Notes in Computer Science, pages 360-432. 1991.

[24]	Peter M. Maurer. Generating testing data with enhanced context-free grammars. IEEE Software, 7(4), July 1990.

[25]	Jeffrey Voas, Larry Morell, and Keith Miller. Predicting where faults can hide from testing. IEEE Software, 8(2):41-58, March 1991.

A 부록: 보조정리 3의 증명

4장에 있는 보조정리 3의 증명에서 빠진 부분이다.

[C-2a] [eqn: X~♤~{rm 0} ~:~ \{{rm 0}`subseteq``X \} `]

(1)에 의해 [eqn: sigma^v ``vdash``{rm 0} ``rightarrow``{rm 0}``]이 성립하고 [eqn: \{{rm 0}`subseteq``X \}` subseteq`C_0`]이므로[eqn: {rm 0} ``in`` I`(X)``]이다.

[C-3a] [eqn: kappa^{-1}`X~♤~{rm 0} ~:~ \{kappa`{rm 0}`subseteq``X \} `]

(1)에 의해 [eqn: sigma^v ``vdash``{rm 0} ``rightarrow``{rm 0}``]이 성립하고 [eqn: \{kappa`{rm 0}`subseteq``X \}` subseteq`C_0`]이므로[eqn: kappa`{rm 0} ``in`` I`(X)``]이다. 따라서[eqn: {rm 0} ``in`` I`(kappa^{-1}X)]이다.

[CONN-2a] [eqn: {X ~♤~e ~ :~C } over {kappa~X ~♤~ kappa ~ e ~:~ C}]

가정에 의해서, [eqn: sigma^v ``vdash``e ``rightarrow``v'``]이 성립하고 [eqn: v' ``in`` I``(X)``]이다. 따라서 [eqn: {sigma^v ``vdash``e ``rightarrow``v'`` } over {sigma^v ``vdash``kappa``e ``rightarrow``kappa``v'``}]이 성립하고 [eqn: kappa``v' ``in`` I``(kappa``X)``]이다.

[CONN-3a] [eqn: {kappa^{-1}~Y ~♤~e ~ :~C } over {kappa'^{-1}`X ``♤`` kappa`` e ``:`` C``cup` \{Y`subseteq`kappa'^{-1}``X \}}`` "새 변수"`` Y``]

가정에 의해서, [eqn: sigma^v ``vdash``e ``rightarrow``v'``]이 성립하고 [eqn: v' ``in`` I``(kappa^{-1}``Y)``]이다. 따라서 [eqn: {sigma^v ``vdash``e ``rightarrow``v'`` } over {sigma^v ``vdash``kappa``e ``rightarrow``kappa``v'``}]이 성립한다. [eqn: v' ``in`` I``(kappa^{-1}`Y)``]이면 [eqn: kappa`v' ``in`` I``(Y)``]이고 [eqn: \{Y`subseteq``kappa'^{-1}`X \}` subseteq`C_0`]이므로, [eqn: kappa``v' ``in`` I``(kappa'^{-1}``X)``]이다.

[CONN-4a] [eqn: {a ~♤~e ~ :~C } over {kappa``a ~♤~ kappa ~ e ~:~ C}]

가정에 의해서, [eqn: sigma^v ``vdash``e ``rightarrow``v'``]이 성립하고 [eqn: v' ``in`` I``(a)``]이다. 따라서 [eqn: {sigma^v ``vdash``e ``rightarrow``v'`` } over {sigma^v ``vdash``kappa``e ``rightarrow``kappa``v'``}]이 성립하고 [eqn: kappa``v' ``in`` I``(kappa``a)``]이다.

[CONX-a] [eqn: {hat{rm E} ~♤~e ~ :~C } over {hat{rm E} ~♤~ kappa ~ e ~:~ C}]

가정에 의해서, [eqn: sigma^v ``vdash``e ``rightarrow``o'``]이 성립하고 [eqn: o' ``in`` \{ hat{rm E} \} ``]이다. 따라서 [eqn: {sigma^v ``vdash``e ``rightarrow``hat{rm E}`` } over {sigma^v ``vdash``kappa``e ``rightarrow``hat{rm E}``}]이 성립하고 [eqn: hat{rm E} ``in`` \{ hat{rm E} \} ``]이다.

[DCONN-2a] [eqn: {kappa~Y ~♤~e ~ :~C } over {kappa'^{-1}`X ``♤`` kappa^{-1}`e ``:`` C`` cup \{ Y``subseteq`kappa'^{-1}`X \} }``"새 변수 "Y`]

가정에 의해서, [eqn: sigma^v ``vdash``e ``rightarrow``v'``]이 성립하고 [eqn: v' ``in`` I``(kappa``Y)``]이다. [eqn: v'~=kappa``v''``]이라 하면 [eqn: {sigma^v ``vdash``e ``rightarrow``kappa``v''`` } over {sigma^v ``vdash``kappa^{-1}``e ``rightarrow``v''``}]이 성립한다. [eqn: v' ``in`` I``(kappa``Y)``]이면 [eqn: kappa^{-1}``v' ``in`` I``(Y)``]이고 [eqn: \{ Y~ subseteq``kappa'^{-1}``X \}`` subseteq`` C_0]이므로, [eqn: v'' ``in`` I``(kappa'^{-1}``X)``]이다.

[DCONN-3a] [eqn: {kappa~Y ~♤~e ~ :~C } over {bar{kappa'}``X ``♤`` kappa^{-1}`e ``:`` C` cup \{ Y``subseteq`bar{kappa'}``X \} }~"새 변수 "Y``]

가정에 의해서, [eqn: sigma^v ``vdash``e ``rightarrow``v'``]이 성립하고 [eqn: v' ``in`` I``(kappa``Y)``]이다. [eqn: v'~=kappa``v''``]이라 하면 [eqn: {sigma^v ``vdash``e ``rightarrow``kappa``v''`` } over {sigma^v ``vdash``kappa^{-1}``e ``rightarrow``v''``}]이 성립한다. [eqn: v' ``in`` I``(kappa``Y)``]이면 [eqn: kappa^{-1}``v' ``in`` I``(Y)``]이고 [eqn: \{ Y~ subseteq``bar{kappa'}``X \}`` subseteq`` C_0]이므로, [eqn: v'' ``in`` I``(bar{kappa'}``X)``]이다.

[DCONX-a] [eqn: {hat{rm E} ~♤~e ~ :~C } over {hat{rm E} ~♤~ kappa ~ e ~:~ C}]

가정에 의해서, [eqn: sigma^v ``vdash``e ``rightarrow``o'``]이 성립하고 [eqn: o' ``in`` \{ hat{rm E} \} ``]이다. 따라서 [eqn: {sigma^v ``vdash``e ``rightarrow``hat{rm E}`` } over {sigma^v ``vdash``kappa^{-1}``e ``rightarrow``hat{rm E}``}]이 성립하고 [eqn: hat{rm E} ``in`` \{ hat{rm E} \} ``]이다.

[DCONN-4a] [eqn: {kappa``{se}~♤~e ~:~ C } over { {se}~♤~kappa^{-1}``e ~:~ C }`~~~se~ not in~ \{ kappa'``X,``kappa'^{-1}``X,``bar{kappa'}``X,``hat{rm E}\}]

가정에 의해서, [eqn: sigma^v ``vdash``e ``rightarrow``v'``]이 성립하고 [eqn: v' ``in`` I``(kappa``se)``]이다. [eqn: v'~=kappa``v''``]이라 하면 [eqn: {sigma^v ``vdash``e ``rightarrow``kappa``v''`` } over {sigma^v ``vdash``kappa^{-1}``e ``rightarrow``v''``}]이 성립한다. [eqn: kappa``v'' ``in`` I``(kappa``se)``]이므로 [eqn: v'' ``in`` I``(se)``]이다.

[APPX-1a] [eqn: {hat{rm E} ~♤~e_2 ~ :~C } over {hat{rm E} ~♤~ (lambda x.e_1 )~ e_2 ~:~ C}]

가정에 의해서, [eqn: sigma^v ``vdash``e_2 ``rightarrow``o'``]이 성립하고 [eqn: o' ``in`` \{ hat{rm E} \} ``]이다. 따라서 [eqn: {sigma^v ``vdash``e_2 ``rightarrow``hat{rm E}`` } over {sigma^v ``vdash``(lambda x.e_1 )~ e_2 ``rightarrow``hat{rm E}``}]이 성립하고 [eqn: hat{rm E} ``in`` \{ hat{rm E} \} ``]이다.

[APPX-2a] [eqn: {hat{rm E} ~♤~e_2 ~ :~C } over {hat{rm E} ~♤~ ({rm fix}``f`` lambda x.e_1 )~ e_2 ~:~ C``cup` \{ F``subseteq``lambdax.e_1 \} }]

가정에 의해서, [eqn: sigma^v ``vdash``e_2 ``rightarrow``o'``]이 성립하고 [eqn: o' ``in`` \{ hat{rm E} \} ``]이다. 따라서 [eqn: {sigma^v ``vdash``e_2 ``rightarrow``hat{rm E}`` } over {sigma^v ``vdash``({rm fix}``f``lambda x.e_1 )~ e_2 ``rightarrow``hat{rm E}``}]이 성립하고 [eqn: hat{rm E} ``in \{ hat{rm E} \}]이다.

[APPX-3a] [eqn: {hat{rm E} ~♤~e_2 ~ :~C } over {hat{rm E} ~♤~ f~ e_2 ~:~ C}~"프로그램 내의 "{rm fix}``f``lambda x.e_1`]

가정에 의해서, [eqn: sigma^v ``vdash``e_2 ``rightarrow``o'``]이 성립하고 [eqn: o' ``in`` \{ hat{rm E} \} ``]이다. 따라서 [eqn: {sigma^v ``vdash``e_2 ``rightarrow``hat{rm E}`` } over {sigma^v ``vdash``f~ e_2 ``rightarrow``hat{rm E}``}]이 성립하고 [eqn: hat{rm E} ``in`` \{ hat{rm E} \} ``]이다.

[APP-1a] [eqn: {X_n ~♤~e_2 ~ :~C_1 ~~se~ ♤~[x_n / x]e_1 ~:~ C_2 } over {se ~♤~ (lambda x.e_1 )~ e_2 ~:~ C_1~ cup`` C_2 }~"새 번호 "n]

가정에 의해서, [eqn: sigma^v ``vdash``e_2 ``rightarrow``v_2``]와 [eqn: sigma^v ``vdash``[x_n /x]e_1 ``rightarrow``o'``]이 성립하고 [eqn: v_2 ``in`` I``(X_n )``]이며 [eqn: o' ``in`` I``(se )``]이다. 보조정리 2에 의해 [eqn: sigma^v``]는 프로그램 수행 중에 변하지 않으므로 [eqn: sigma^v``[x_n mapsto v_2 ]~=~sigma^v``]이다. 따라서 [eqn: {sigma^v ``vdash``e_2 ``rightarrow``v_2 ``~~~sigma^v``[x_n mapsto v_2 ] ``vdash``[x_n / x]e_1 ``rightarrow``o'`` } over {sigma^v ``vdash``(lambdax.e_1 )``e_2 ``rightarrow``o'``}]이 성립하고, [eqn: o' ~ in`` I``( se )]이다.

[APP-2a] [eqn: {X_n ~♤~e_2 ~ :~C_1 ~~se~ ♤~[x_n / x]e_1 ~:~ C_2 } over {se `♤` ({rm fiix}`f```lambda x.e_1 )`` e_2 ``:`` C_1` cup` C_2`\{ F`subseteq`lambda x.e_1 \} }~"새 번호 "n]

가정에 의해서, [eqn: sigma^v ``vdash``e_2 ``rightarrow``v_2``]와 [eqn: sigma^v ``vdash``[x_n /x]e_1 ``rightarrow``o'``]이 성립하고 [eqn: v_2 ``in`` I``(X_n )``]이며 [eqn: o' ``in`` I``(se )``]이다. 보조정리 2에 의해 [eqn: sigma^v``]는 프로그램 수행 중에 변하지 않으므로 [eqn: sigma^v``[f mapsto langle sigma^v , {rm fix}``f``lambdax.e_1 rangle ]`[x_n mapsto v_2 ]~=~sigma^v``]이다. 따라서 [eqn: {{sigma^v ``vdash``e_2 ``rightarrow``v_2 } atop {sigma^v``[f mapsto langle sigma^v , {rm fix}``f``lambdax.e_1 rangle ]`[x_n mapsto v_2 ] ``vdash``[x_n / x]e_1 ``rightarrow``o'`` }} over {sigma^v ``vdash``({rm fix}``f``lambdax.e_1 )``e_2 ``rightarrow``o'``}]이 성립하고, [eqn: o' ~ in`` I``( se )]이다.

[APP-3a] [eqn: {X_n `♤`e_2 `:`C_1 ~se` ♤`[x_n / x]e_1 `:` C_2 } over {se ~♤~ f~ e_2 ~:~ C_1~ cup`` C_2 } {{"프로그램 내의"{rm fix}``f``lambda x.e_1 `,} atop {"새 번호 "n,`` Used_f () le N }}]

가정에 의해서, [eqn: sigma^v ``vdash``e_2 ``rightarrow``v_2``]와 [eqn: sigma^v ``vdash``[x_n /x]e_1 ``rightarrow``o'``]이 성립하고 [eqn: v_2 ``in`` I``(X_n )``]이며 [eqn: o' ``in`` I``(se )``]이다. 보조정리 2에 의해 [eqn: sigma^v``]는 프로그램 수행 중에 변하지 않으므로 [eqn: sigma^v``[f mapsto langle sigma^v , {rm fix}``f``lambdax.e_1 rangle ]`[x_n mapsto v_2 ]~=~sigma^v``]이다. 따라서 [eqn: {{sigma^v``(f`)`=` langle sigma^v , {rm fix}``f``lambdax.e_1 rangle~~sigma^v ``vdash``e_2 ``rightarrow``v_2 } atop {sigma^v``[f mapsto langle sigma^v , {rm fix}``f``lambdax.e_1 rangle ]`[x_n mapsto v_2 ] ``vdash``[x_n / x]e_1 ``rightarrow``o'`` }} over {sigma^v ``vdash``({rm fix}``f``lambdax.e_1 )``e_2 ``rightarrow``o'``}]이 성립하고, [eqn: o' ~ in`` I``( se )]이다.

[CASEX-a] [eqn: {hat{rm E} ~♤~e_1 ~ :~C } over {hat{rm E} ~♤~ {rm case}~ e_1 ~kappa~ e_2 ~e_3 ~:~ C}]

가정에 의해서, [eqn: sigma^v ``vdash``e_2 ``rightarrow``o'``]이 성립하고 [eqn: o' ``in`` \{ hat{rm E} \} ``]이다. 따라서 [eqn: {sigma^v ``vdash``e_1 ``rightarrow``hat{rm E}`` } over {sigma^v ``vdash``{rm case} e_1 ``kappa`` e_2 ``e_3 ``rightarrow``hat{rm E}``}]이 성립하고 [eqn: hat{rm E} ``in`` \{ hat{rm E} \} ``]이다.

[CASE-2a] [eqn: {bar{kappa}``X ~♤~e_1 ~ :~C_1 ~~se~ ♤~e_3 ~:~ C_2 } over {se ~♤~ {rm case} e_1 ``kappa`` e_2 ``e_3~:~ C_1~ cup`` C_2 }~"새 변수 " X]

가정에 의해서 [eqn: sigma^v ``vdash``e_1 ``rightarrow``v_1`], [eqn: sigma^v ``vdash``e_3 ``rightarrow``o'`]이 성립하고 [eqn: v_1 ``in`` I``(bar{kappa}``X )`]이며 [eqn: o' ``in`` I``(se )`]이다. [eqn: v_1 `=kappa'`v'`]이고 [eqn: kappa'``not=kappa``]라 하면, [eqn: {sigma^v ``vdash``e_1 ``rightarrow``kappa'``v'~~sigma^v ``vdash``e_3 ``rightarrow``o'`` } over {sigma^v ``vdash``{rm case}~e_1~ kappa``e_2``e_3 ``rightarrow``o'``}]이 성립하고 [eqn: o' ``in`` I``(se )``]이다.

[HNDLN-a] [eqn: {se ~♤~e_1 ~ :~C } over {se ~♤~ {rm handle}~ e_1 ~{rm E}~ e_2 ~:~ C }~~~se not= \{hat{rm E} \}]

가정에 의해서, [eqn: sigma^v ``vdash``e_1 ``rightarrow``v'`]이 성립하고 [eqn: v' ``in``I`(se)`]이다. 따라서 [eqn: {sigma^v ``vdash``e_1 ``rightarrow``v'`` } over {sigma^v ``vdash``{rm handle}~e_1~ {rm E}``e_2 ``rightarrow``v'``}]이 성립하고 [eqn: v' ``in`` I``(se )``]이다.

[HNDX-a] [eqn: {hat{rm E'} ~♤~e_1 ~ :~C } over {hat{rm E'} ~♤~ {rm handle}~ e_1 ~{rm E}~ e_2 ~:~ C }~~~{rm E'} not= {rm E}]

가정에 의해서, [eqn: sigma^v ``vdash``e_1 ``rightarrow``o'`]이 성립하고 [eqn: o' ``in``\{hat{rm E'} \}`]이다. 따라서 [eqn: {sigma^v ``vdash``e_1 ``rightarrow``hat{rm E'}`` } over {sigma^v ``vdash``{rm handle}~e_1~ {rm E}``e_2 ``rightarrow``hat{rm E'}``}]이 성립하고 [eqn: hat{rm E} ``in`` \{ hat{rm E} \} ``]이다. □