접수번호 : 97-02-20-75

제  목 : Standard ML 프로그램 실행 중 처리되지 않는 예외 상황을

효과적으로 예측하는 방법

(A Cost-effective Estimation of Uncaught Exceptions in Standard

ML Programs)

성  명 : 류석영(柳石英, Sukyoung Ryu), 이광근(李光根, Kwangkeun Yi)

소속기관 : 한국 과학 기술원

(Korea Advanced Institute of Science and Technology)

연구 세부 분야 : B (소프트웨어)

키워드 : Standard ML, 예외 상황 처리, 처리되지 않는 예외 상황, 함수

흐름도 분석, 타입 유추

주 소 : 대전시 유성구 구성동 373-1 한국 과학 기술원 전산학과

우편번호 : 305-701

전 화 : (042) 869 - 5576

FAX 번호 : (042) 869 - 3510

E-mail 주소 : puppy@pllab.kaist.ac.kr, kwang@cs.kaist.ac.kr

Standard ML 프로그램 실행 중 처리되지 않는

예외 상황을 효과적으로 예측하는 방법

1본 연구는 한국 과학재단 (과제번호 95-0100-54-3), 정보 통신부 (과제번호 96151-IT2-12), 과기처, 삼성 전자의 부분적인 지원에 의한 것임.

(A Cost-effective Estimation of Uncaught Exceptions in Standard ML Programs)

요 약  본 논문에서는 Standard ML 프로그램의 실행 중에 발생할 수 있는 예외 상황 처리의 허점을 미리 예측하는 정적 분석 방법을 제안한다. 이 분석 방법은 SML 프로그램의 안전에 유일하게 허점으로 작용할 수 있는 해제되지 못한 예외 상황을 예측한다.

프로그램의 함수 흐름도는 SML/NJ 컴파일러의 타입 유추를 통해 거의 비용을 들이지 않고 예측하고, 그것을 이용하여 예외 상황의 흐름을 표현하는 집합 제약식을 만든다. 이렇게 만들어진 제약식의 해가 바로 본 논문에서 제안하는 예외 상황 분석의 답이 된다.

이 방법을 구현하여 실제적인 SML 프로그램을 분석하는 데 실험해 본 결과, 기존의 방법보다 매우 향상된 비용 대 성능비를 가지고 있는 것으로 나타났다. 예를 들어, ML-lex.sml을 분석하는 데에 1.36초가 걸렸고, 실제로 발생해서 소멸되지 않는 3개의 예외 상황만을 정확하게 찾아낸다.

Abstract We present a static analysis that detects potential runtime exceptions that are raised and never handled inside Standard ML(SML) programs. This analysis will predict abrupt termination of SML programs, which is SML's only one □safety hole.□

Program's control-flow is computed simply based on the expression types from the SML/NJ compiler. From this call-graph information, program's exception flow is derived as set-constraints, whose least model is computed using the conventional iterative fixpoint method (the solution space is finite).

A prototype of this analysis has a promising cost-accuracy balance. For the ML-lex program, for example, the analysis takes 1.36 seconds to finish and it reports 3 may-uncaught exceptions. (The ML-lex program has 10 exceptions, 19 raises, and 10 handlers.)

1. 서 론

이 장에서는 Standard ML(SML)에 대하여 간단히 알아보고, 본 논문에서 다루고자하는 문제인 SML 예외 상황 분석(exception analysis)에 대해서 설명한 후, 본 논문에서 제안하는 방법을 개괄한다.

1.1 Standard ML 프로그래밍 언어

지금까지 대부분의 중요한 소프트웨어들 - 운영체제, 컴파일러, 네트워크 시스템, 전화 스위칭 시스템 등 - 이 C로 구현되어 왔지만, C 언어가 가지고 있는 문제점들을 볼 때 C 보다 상위의 언어에 대한 요구가 증가되고 있는 실정이다[1,2,3,4,5]. 이러한 언어에 대한 연구 성과들이 최근 급속도로 축적되고 있는데, 그 대표적인 예로 주목받고 있는 언어가 Standard ML[6,7,8,4]이다.

SML은 다음과 같은 여러 가지 장점을 가지고 있다. 첫째로, SML은 수행 중인 프로그램의 안전이 보장되어 있다. 즉, SML 컴파일러를 통과한 프로그램은 실행 중에 잘못되는 경우가 발생하지 않는다. 둘째로, 큰 프로그램 개발을 위한 정제된(simple and advanced) 모듈 처리 기능을 갖추고 있다. 셋째로, 예외 상황 처리(exception handling)

매카니즘을 갖추고 있어서 프로그램의 실행 중에 발생할 수 있는 긴급 상황  들을 정황에 맞게 적절히 처리할 수 있다[6,9,10]. SML에서 제공하는 예외 상황 매카니즘에 대해서는 다음 절에서 좀 더 자세하게 알아보기로 한다. 마지막으로, SML은 효율적인 메모리 관리 시스템(garbage collection)을 제공하기 때문에 프로그래머가 메모리의 부족이나 재사용 등에 대한 부담 없이 프로그래밍을 할 수 있다.

예를 들면,[eqn: {scale 90 rm bold {''x / y''}}]에서[eqn: scale 90 rm bold y]의 값이[eqn: {scale 90 rm bold 0}]인 경우

1.1.1 Standard ML의 예외 상황 처리 방법

SML 프로그래머는 간편하고 자유로운 방법으로 예외 상황의 발생(exception raise)과 소멸(exception handling)을 표현할 수 있다. 예외 상황은 함수의 인수로 전달될 수도 있고 함수의 결과 값으로 전달받을 수도 있다. 또, 메모리에 저장되었다가 꺼내어져서 발생할 수도 있다.

예를 들면,[eqn: scale 90 rm bold {''`raise~ !x''}]는[eqn: scale 90 rm bold {x}]라는 메모리 위치에 저장된 예외 상황을 발생시킨다.

예외 상황은 각각 이름을 갖고 있고, 인수를 가질 수도 있다. 예를 들어,

[eqn: rm bold {Error``('' at~ \line~ 10''` )}]

위의 표현은 문자열을 인수로 갖는 예외 상황[eqn: ``rm bold Error`]를 만든다. 예외 상황 이름인[eqn: ``rm bold Error`]는 사용되기 전에 미리 다음과 같이 선언되어야 한다:

[eqn: rm bold {exception~`` Error~`` of~`` string}]

예외 상황은 다음과 같은 표현에 의해 발생한다.

[eqn: {rm bold raise}~ e``]

위의 표현에서[eqn: ~e`]의 계산 결과는 예외 상황이어야 한다. 예를 들어,[eqn: rm bold {raise ~!x}]는 메모리[eqn: rm bold x]에 저장된 예외 상황을 발생시키는 것이 된다.

SML에서 예외 상황 처리 함수의 문법은 다음과 같다.

[eqn: e`` {rm bold handle}~` p_1~`` RARROW~` e_1~`` |~` cdots~` |~` p_n~`` Rarrow~` e_n`]

[eqn: e`]의 계산 결과로 발생한 예외 상황 이름이 [eqn: p_k]와 같으면 [eqn: e_k]가 계산되고, 같은 이름이 없으면 다른 예외 상황 처리 함수를 만날 때까지 계속해서 계산 과정을 거슬러 올라간다. 발생한 예외 상황을 처리해주는 예외 상황 처리 함수가 없을 경우에는 프로그램이 멈추게 된다. 즉, 현재까지 계산된 순서를 거슬러 올라가다가 제일 마지막에도 예외 상황 처리 함수를 만나지 못할 때에는, 발생한 예외 상황을 처리하지 못하게 되므로 프로그램이 중단되는 것이다.

1.2 문제 정의

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

하지만, 프로그래머가 주의 깊게 사용하지 않으면 오히려 프로그램의 안전도를 해치는 상황으로 발전할 수도 있다. 프로그램 내에서 예외 상황이 발생하면 그 예외 상황을 소멸시킬 수 있는 곳으로 프로그램의 실행 순서가 바뀌게 되는데, 만일 예외 상황 처리 함수(exception handler)가 허술해서 발생한 예외 상황을 소멸시킬 수 없을 경우에는 프로그램이 갑작스럽게 중단해버리기 때문이다.

그러므로 프로그램을 실제로 실행시키기 전에 미리 이러한 가능성을 예측하는 것이 예외 상황 분석이다. 즉, 예외 상황 분석은 프로그램 실행 도중에 발생되어서 처리되지 않을 가능성이 있는 예외 상황들을 미리 예측하는 것이다.

SML의 예외 상황은 함수의 인수로 전달되거나 결과로 전달받을 수 있으므로, 프로그

램을 봐서는 발생되는 예외 상황이 소멸되는지 알 수가 없다. 예를 들어,

[eqn: rm bold{f(x)~ =~` cdots~`` raise~ x~` cdots}]

위의 함수[eqn: `{rm bold f}]에서 어떤 예외 상황이 발생하는지를 알기 위해서는 함수[eqn: `{rm bold f}]가 어떤 예외 상황을 인수로 전달받는지 알아야 한다. 또, 발생하는 예외 상황이 소멸될 수 있는지를 알기 위해서는 함수[eqn: `{rm bold f}]를 호출할 때 어떤 예외 상황 처리 함수가 제공되는 지도 알아야 한다.

또 다른 예로, 함수를 인수로 받는 함수[eqn: `{rm bold f}]의 경우,

[eqn: rm bold {f(g)~`=`~cdots`~g(x)~``handle~``E~`Rarrow~`cdots}]

[eqn: rm bold g(x)]에서 어떤 예외 상황이 발생하는지 알려면 함수[eqn: `{rm bold f}]가 어떤 함수를 인수로 받는지 알아야 한다. 또 앞의 예처럼,[eqn: `{rm bold f}]의 계산 도중에 발생하는 예외 상황을 없애기 위해서[eqn: `{rm bold f}]를 호출할 때 어떤 예외 상황 처리 함수를 제공하는지도 알아야 한다.

1.3 관련 연구

Guzm□n과 Su□rez[11]는 간단하게 바꾼 ML 프로그램에 대해서, 프로그램 실행 중 처리되지 않는 예외 상황을 모으는 타입 유추 시스템을 제안했다. 이 방법은 실제 SML 프로그램의 예외 상황을 다루기에는 부족한 면이 있다. 예를 들어, 이 방법에서는 예외 상황이 인수를 가질 수 없고 단지 이름만으로 다루어지고 있다. 인수를 갖는 예외 상황을 다루기 위해서는, 예외 상황 인수의 범위를 예측하기 위해서 □영역(regions)□[12]과 비슷한 개념을 필요로 할 것이다.

Fahndrich와 Aiken[13]은 예외 상황의 타입을 세분(refine)한 타입 유추 시스템을 기반으로 하여, 예외 상황 분석을 다루고 있다. 이 방법은 기존의 타입 유추 시스템이 아니라, 집합 제약식(set-constraint framework)을 사용한 좀 더 일반적인 타입 유추 시스템을 사용하고 있다.

본 연구 이전에 사용했던 요약 해석을 이용한 분석 방법[14]에서는 SML 프로그램을 분석하기 전에 중간 표현 언어로 바꾸고, 그 후에 이 언어의 요약 의미(abstract semantics)를 기반으로 예외 상황을 모아간다. 이 방법은 매우 자세한 정보를 얻을 수 있기는 하지만 너무 시간이 많이 걸린다는 단점이 있다. 예를 들어, ML-lex.sml 프로그램을 분석한 결과 실제로 프로그램 실행 중 발생해서 소멸되지 않는 예외 상황들만을 찾아내는 반면, 분석하는 데에 약 6시간이 걸린다.

1.4 연구 내용 및 결과

본 연구의 목표는 SML 프로그램의 실행 중에 발생할 수 있는 예외 상황 처리의 허점을 미리 예측하는 분석기를 개발하는 것이다. SML 프로그램이 가질 수 있는 안전도의 유일한 허점은 바로 이러한 해제되지 못한 예외 상황이므로, 컴파일러가 이를 예측할 수 있다면 프로그램의 안전도를 더욱 증진시킬 것이다.

SML에서는 예외 상황이 함수 사이에서 자유롭게 전달될 수 있으므로, 요약 해석 방법(abstract interpretation)을 사용하는 것이 자연스러울 수 있다. 이 방법으로 예외 상황 분석을 하면 함수 흐름의 분석이 자연스럽게 표현되기 때문이다.

그러나 요약 해석을 이용한 분석은 매우 자세한 정보를 얻을 수 있기는 하지만, 그 비용이 너무 크다는 문제점이 있다. 함수의 흐름을 파악하면서 예외 상황의 흐름을 분석하므로, 두 가지 흐름을 동시에 처리해서 비용이 커지는 것이다.

하지만, SML 프로그래머가 표현할 수 있는 예외 상황의 내용이 매우 광범위함에도 불구하고, 통상적인 예외 상황의 내용은 대부분의(91% - 100%) 경우가 간단한 방법  으로 사용된다는 사실이 분석되었다[16]. 그림 1.1은 SML로 짜여진 대표적인 응용 프로그램에서 관찰된 통상적인 예외 상황의 경우들을 요약한 것으로, 이러한 사실을 뒷받침해주고 있다. 그러므로 적은 비용의 간단한 방법으로 함수 흐름을 분석해도 예외 상황 분석에는 효과적일 수 있다.

□간단한 방법□으로 사용된 예외 상황의 경우란, 예외 상황의 발생 표현식(exception-raise expression)에 직접 예외 상황의 이름을 표현한 경우를 말한다. SML에서는 예외 상황이 다른 값들과 구분없이 사용될 수 있기 때문에,[eqn: scale 90 rm bold {''`raise~ f()`''}]와 같이 어떤 예외 상황을 발생시키는지를 프로그램의 텍스트만을 보고는 알 수 없는 복잡한 경우가 있다.

그림 1.1

본 논문에서는 예외 상황 분석과 함수 흐름 분석을 분리하여 전체 분석 비용을 줄이면서도, 효과적으로 예외 상황을 분석할 수 있는 방법을 제안한다. 프로그램의 함수 흐름

도는 SML/NJ 컴파일러의 타입 유추를 통해 거의 비용을 들이지 않고 예측하고, 그것을 이용하여 예외 상황 흐름을 표현하는 제약식(constraints)을 만들어내는 것이다. 그리고 이렇게 만들어진 제약식의 해가 바로 본 논문에서 제안하는 예외 상황 분석의 답이 된다.

이 방법이 틀리지 않다는 것 - 프로그램 실행 중에 실제로 소멸되지 않는 예외 상황들을 모두 찾아낸다는 것 - 을 정확하게(mathematically rigorous) 증명할 수 있었고, 이 방법을 구현하여 실제적인 SML 프로그램을 분석하는 데 실험해 보았다. 그림 1.2는 몇 가지 실제적인 SML 프로그램을 대상으로 실험해 본 결과이다. 구현된 분석 방법은 기존의 방법보다 매우 향상된 비용 대 성능비를 가지고 있다.

그림 1.2

본 논문에서 제안한 방법의 속도는 프로그램에 따라 약 960 SML-lines/sec에서부터 약 4730 SML-lines/sec에까지 차이가 많기는 하지만, 요약 해석을 이용한 예전 방법(0.3 SML-lines/sec[14])보다는 월등한 속도로 분석을 마칠 수 있다. 예를 들어 ML-lex.sml의 경우, 기존의 분석 방법으로는 6시간이 걸렸지만 본 논문에서 제안한 방법으로는 1.36초가 걸렸다.

이 분석 방법은 또한 매우 정확한 결과를 제공한다. 그림 1.2에 나와있는 테스트 프로그램에 대한 분석 결과의 정확도를 알아보기 위하여, 각 프로그램에서 실제로 발생해서 소멸되지 않는 예외 상황들을 조사하였다. 그림 1.2에 나와 있는 모든 테스트 프로그램에 대해서 분석한 결과, 실제로 발생해서 소멸되지 않는 예외 상황들만을 찾아낸다.

참고로, 본 논문의 내용과 같은 문제를 또 다른 방법(set-constraint-based type inference[13])으로 진행하고 있는 University of California at Berkeley의 Alexander  Aiken 교수 팀의 분석 결과는(1997년 6월 현재), ML-lex.sml의 경우 3.9초가 걸렸고, 발생해서 소멸되지 않는 예외 상황이 실제로는 3개인데 이것들을 포함해서 총 4개를 찾아낸다.

우리의 분석기가 컴파일러에 장착되어 실제적으로 사용되기 위해서는 컴파일하는 데 걸리는 총 시간에 비해 예외 상황 분석을 하는 데에 걸리는 시간이 적어야 한다. 현재 예외 상황 분석 시간이 컴파일 시간 동안 차지하는 비율은 약 3% - 8%  정도이다.

SML/NJ 108.13 컴파일러의 시간과 비교한 것이다.

1.5 분석 방법의 제약점

본 논문에서 제안한 분석 방법은 다음과 같은 제약점들을 가지고 있다.

첫째로, 전체 프로그램이 주어진 경우에만 분석할 수 있다. 즉, 전체 프로그램이 주어지지 않고 프로그램의 일부분만을 가지고 있을 경우에는 본 논문에서 제안한 분석 방법으로 분석할 수가 없다.

이 분석 방법을 SML/NJ 컴파일러에 장착시키기 위해서는 SML 프로그램의 일부분만으로도 분석할 수 있어야 한다. 이 제약점에 대해서는 현재 연구 중에 있다.

둘째로, 라이브러리 함수를 포함하여, 프로그램 텍스트 상에 나타난 예외 상황들만을 분석할 수 있다. 즉, +, - 같은 기본 함수들로부터 발생하는 예외 상황들은 분석할 수 없다.

그러나 이 제약점은 쉽게 해결할 수 있다. 즉, 기본 함수들로부터 발생할 수 있는 예외 상황들을 표(table)에 기록하고 있고, 이 예외 상황들은 모든 함수들이 사용할 수 있는 예외 상황으로 간주하면 된다.

셋째로, 생성적인 성질(generative nature)을 이용하여 예외 상황을 선언한 프로그램은 분석할 수 없다. 생성적인 성질이란, 프로그램 내에서 예외 상황을 선언할 때, 비록 같은 이름을 갖더라도 각각 계산될 때마다 새로운 내부 표현의 이름을 얻게 되는 것을 말한다. 예외 상황 처리 함수는 프로그램에서 선언된 예외 상황의 이름을 이용하여 소멸시키려는 예외 상황을 찾는 것이 아니라, 계산될 때 주어진 내부 표현의 이름으로 찾게 된다.

본 논문에서 제안한 방법은 이러한 성질을 이용한 예외 상황에 대해서는 분석을 할 수 없다. 그러나, 이러한 제약점이 그다지 큰 문제가 되지는 않는다. 왜냐하면, 예외 상황들은 대부분 프로그램 전체에서 사용될 수 있도록(global scope) 선언되거나 스트럭쳐 안에서 선언되기 때문이다. 또, 지역적으로 선언된(local declaration) 예외 상황들에 대해서도, 대부분 이름을 적절히 바꾸는 방법을 이용하여 프로그램의 작용에 영향을 미치지 않는 범위 안에서 프로그램 전체에서 사용될 수 있도록 바꿀 수가 있다. 이러한 작업이 가능하지 않은 프로그램들에 대해서는 본 논문에서 제안한 분석 방법으로 올바른 결과를 얻을 수 없다.

본 논문의 전체적인 구조는 다음과 같다. 설명의 편의성을 위해 본 논문에서 대상 언어로 사용하는 L 언어를 2장에서 정의한다. 3장에서는 타입 정보를 이용하여 함수의 흐름을 분석하는 방법을 제안하고, 제안한 방법의 정확도를 높이기 위한 방법을 설명한다. 4장에서는 분석하여 얻어진 함수 흐름 정보를 이용하여 예외 상황 분석을 하는 방법에 대해서 설명하고 그 안전성을 증명한다. 5장에서는 이 방법을 구현하는 방법에 대해서 설명하고, 6장에서는 결론을 맺는다.

2. L 언어

본 논문에서는 설명의 편의성을 위해서, 실제 SML 프로그램이 아니라 L이라는 새로운 언어로 짜여진 프로그램을 대상으로 예외 상황 분석을 설명하기로 한다. 모든 SML 프로그램은 해당하는 L 프로그램으로 만들어낼 수 있다. L 언어의 문법식(abstract syntax)와 타입 구조(type system)이 그림 2.1에 나타나있다. 본 논문에서는 앞으로 다음과 같은 표기법을 사용하기로 한다. [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')]으로 매핑하는 새로운 함수를 나타낸다.

함수 f의 정의구역이 집합 A의 유한한 부분집합이다.

그림 2.1

L에서 사용되는 값들은 예외 상황이거나 함수이다.[eqn: {rm bold {'' exn}}~kappa~e{rm bold''}`]는[eqn: ~e`]를 인수로 갖고 이름이 [eqn: kappa`]인 예외 상황을 나타내고, 예외 상황[eqn: ~e`]의 인수는[eqn: {rm bold {'' decon}}~e{rm bold''}`]를 이용하여 얻을 수 있다.[eqn: {rm bold {''``` fix}}`` ~f``~lambda x_tau .e{rm bold ''}`]은 재귀 함수인 [eqn: f``~=~lambda x_tau . e``]을 정의한다.[eqn: {rm bold {'' case}}~``e_1 ~``kappa~``e_2~`` e_3{rm bold''}`]는[eqn: ~e_1]의 값이 [eqn: kappa`]일 경우에는[eqn: ~e_2]를 선택하고 그렇지 않을 경우에는[eqn: ~e_3]를 선택한다.[eqn: {rm bold {'' raise}}~e{rm bold''}`]는[eqn: ~e`]의 결과인 예외 상황을 발생시킨다.[eqn: {rm bold +raise}`]와[eqn: {rm bold -raise}`]는 예외 상황 분석의 정확도를 위한 것으로 다음 절에서 자세하게 설명하기로 한다.[eqn: {rm bold {''``` handle}}`` ~e_1 ``~lambda x_tau .e_2 {rm bold ''}`]는[eqn: ~e_1]의 값을 계산하여 타입 [eqn: tau``]를 갖는 예외 상황이 발생하면 그 예외 상황을 [eqn: x`]라 하여[eqn: ~e_2]를 계산하고, 그렇지않으면[eqn: ~e_1]의 값을 결과 값으로 한다.

예외 상황 처리 표현[eqn: {rm bold {''``` handle}}`` ~e_1 ``~lambda x_tau .e_2 {rm bold ''}`]에서 함수[eqn: {rm bold {''}}``lambda x_tau .e_2 {rm bold ''}`]은 처리 함수라 하고,[eqn: {rm bold {''}}``e_1 {rm bold ''}`]은 처리되는 표현,[eqn: {rm bold {''}}``x {rm bold ''}`]는 처리 변수라 한다.

2.1 전처리(Preprocessing)

예외 상황의 흐름이 프로그램 텍스트에 최대한으로 나타나게 하기 위하여 다음과 같은 표현을 사용한다. 설명의 편의성을 위해, 스위치 표현이 여러 개의 표현을 선택할 수 있도록 한다. 또한, L 언어에서는 제공하지 않지만, 인수를 갖지 않는 예외 상황과 숫자도 이용하여 예를 들기로 한다.

·[eqn: {rm bold -raise}`]: 예외 상황 처리 표현에는 항상[eqn: {rm bold -raise}`]를 덧붙여서 예외 상황 처리 표현이 처리하지 못하는 예외 상황을 다시 발생시키도록 한다.

[eqn: rm bold handle] [eqn: e~~lambda`` x_exn .]

[eqn: e~][eqn: rm bold handle`]	[eqn: rm bold case] [eqn: x]

[eqn: rm bold {ERROR~ Rarrow~ 1}]    [eqn: buildrel RARROW is]	[eqn: rm bold ERROR~1]

[eqn: rm bold {|~FAIL~Rarrow~2}]	[eqn: ~rm bold {FAIL~2}]

_[eqn: rm bold {-raise}][eqn: ~x``][eqn: rm bold {ERROR~FAIL}]

위의 예를 보면 다시 발생되는 예외 상황은 [eqn: x``]로 전달되는 예외 상황 중에서[eqn: rm bold ERROR] 와[eqn: rm bold FAIL]을 제외한 것이라는 것을 알 수 있다.

·[eqn: {rm bold +raise}`]: 예외 상황 처리 표현에서 예외 상황의 인수를 모두 처리하지 못하는 경

우에 그 예외 상황을 다시 발생시키도록 한다. 예를 들어,

[eqn: {rm bold handle}~`` e~`lambda`` x_{(tau``list)``exn}.]

[eqn: {rm bold case}~``x``]

[eqn: rm bold {exception~``E~``of~``"int"~``list`}]	[eqn: {rm bold E}~``(` lambda`` y_{tau`` list}`.]

···	[eqn: buildrel RARROW is]	[eqn: {rm bold case}~``y``]

[eqn: e~ rm bold {handle~``E~``"nil"~``Rarrow~``1}]	[eqn: rm bold {"NIL"~``1}]

_[eqn: {rm bold +raise}~x{rm bold E)~(decon}~x{rm bold)}]

_[eqn: {rm bold -raise}~``x``{rm bold E}`]

의 경우에, 왼쪽의 예외 상황 처리 표현은 예외 상황의 인수가[eqn: ``rm bold "nil"`]이 아닐 때에는 처리하지 못한다. 이 경우에는 오른쪽과 같이[eqn: {rm bold +raise}`]를 사용하여 예외 상황을 다시 발생시키면서, 다시 발생한 예외 상황이[eqn: ``{rm bold E}`]뿐임을 나타낸다.

이 장에서는 본 논문에서 다루는 대상 언어인 L 언어를 정의하였다. 다음 장에서는 L 언어를 이용하여 프로그램의 함수 흐름을 예측하는 방법에 대해서 알아본다.

3. SML 프로그램의 함수 흐름도 예측

이 장에서는 예외 상황 분석 전에 꼭 필요한, 프로그램 내의 함수 흐름도를 예측하는 방법  에 대해서 설명한다. 또 타입 정보를 이용해서 프로그램의 흐름을 예측할 때, 정확도를 높이기 위해 하게 되는 몇 가지 일들에 대해서 알아본다.

프로그램의 흐름을 분석하는 것은 데이타의 흐름 분석과 함수의 흐름 분석의 두 가지로 나누어질 수 있다. FORTRAN과 같은 간단한 프로그래밍 언어는 두 가지 흐름을 분리해서 분석하는 방법을 주로 사용한다. 반면에, 함수가 인수로 전달되거나 결과 값으로 전달받을 수 있는 - 함수가 데이타의 일종인 - 프로그래밍 언어에서는 데이타의 흐름 분석과 같이 두 가지 분석을 동시에 하게 된다.

3.1 프로그램의 함수 흐름도 예측

본 논문에서는 프로그램의 흐름 분석과 예외 상황 분석을 분리하는 방법을 제안한다. 예외 상황 분석을 하기 전에 먼저 SML 프로그램의 흐름을 타입 정보를 이용하여 예측하는 것이다.

함수를 호출하는 모든[eqn: {rm bold {''}}``e_1~`` e_2 {rm bold ''}`]에 대해서, [eqn: e_1]이 어떤 함수인지를 아는 것이 프로그램의 흐름을 알아내는 것이다. 만일, [eqn: e_1]이 어떤 함수인지를 모를 경우에는 (예를 들어, [eqn: e_1]이 정의된 함수 이름도 아니고[eqn: rm bold {''`` fn~x~Rarrow~cdots``''}``]와 같은 직접 적혀진 함수(immediate function)도 아닐 경우), [eqn: e_1]의 타입과 같아질 수 있는(unifiable[17]) 타입을 가진 함수가 호출되는 것으로 한다.

이 방법을 이용하면 분석의 정확도가 문제가 될 수 있지만, SML 프로그램 내의 함수는 굉장히 다양한 타입을 갖는 경향이 있기 때문에, 이 방법은 유용하게 사용될 수 있다. 그림 3.1은 몇몇 SML 프로그램에 대해서 함수의 타입에 관련된 사항들을 조사한 것으로, 프로그램 내의 함수들이 매우 다양한 타입을 갖고 있음을 알 수 있다.

그림 3.1

한 가지 유의할 점은 프로그램 내의 각 함수 타입에 대해서, 그 타입과 같아질 수 있는(unifiable) 타입의 갯수가 많은 경우가 있다는 것이다. 예를 들어, compiler.sml의 경우에는 이러한 함수 타입의 평균 갯수가 10.68이다. 이렇게 큰 값을 갖게 되는 이유는 프로그램 내의 몇몇 함수의 타입이 □[eqn: alpha~` ->`` beta``]□  이기 때문이다. 이러한 경우에는 프로그램 분석의 정확도가 떨어질 수 있다. 특히 상위 개념의 함수(higher-order function)에 대한 분석은 정확도가 많이 떨어지게 되므로, 본 논문에서는 더 자세한 정보를 제공하는 방법을 제안하고 있다. 다음 절에서는 이러한 방법에 대해서 알아보기로 한다.

SML에서 [eqn: alpha~` ->`` beta``]는 임의의 타입의 인수를 받아서 임의의 타입의 결과를 만드는 함수의 타입이다. 그러므로 프로그램 내의 모든 함수들이 이 타입과 같아질 수 있다.

3.2 상위 개념의 함수에 대한 흐름 분석

이 절에서는 타입 정보를 이용해서 프로그램의 흐름을 예측할 때, 정확도를 높이기 위해서 사용하는 몇 가지 방법들에 대해서 설명한다.

3.2.1 상위 개념 함수의 흐름 분석에 대한 문제점

지금까지 설명한 방법은 실제로 프로그램의 흐름을 분석하는 것이 아니라 타입 정보를 이용해서 프로그램의 흐름을 예측하기 때문에, 프로그램의 흐름을 분석하는 비용이 매우 작지만, 그 정확도는 요약 해석(abstract interpretation)에 비해 떨어질 수 있다. 특히, 여러 가지 타입을 갖는 상위 개념의 함수들(polymorphic higher-order function)을 분석할 때에는 정확도가 많이 떨어지게 된다.

다음과 같은[eqn: ``rm bold map`] 함수

[eqn: rm bold {fun~map~(f,~"nil")~=~"nil"~|~map~(f,~a::b)~=~(f~a)~::b}]

를 예로 들면,[eqn: ``rm bold map`]의 인수인 함수[eqn: ``rm bold f``]는 [eqn: alpha~` ->`` beta``]의 타입을 갖는다. [eqn: alpha~` ->`` beta``]의 타입은 모든 함수의 타입과 같아질 수(unifiable) 있으므로, 지금까지 제안한 방법에서는 프로그램 내의 모든 함수가[eqn: ``rm bold map`]의 인수로 전달된다고 가정하게 된다.

또 다른 예로 다음의 함수와 그 함수가 호출되는 경우를 본다.

[eqn: {rm bold {fun~``f~x~`=~`fn~y~Rarrow~}}e``]

[eqn: {rm bold {(`(``f~}}~e{rm bold {)}}~``e'{rm bold {)}}`]

바깥쪽의 함수 호출에 대해서 살펴보면[eqn: {rm bold {fn~y~``Rarrow~}}e``]가 호출되는 것이 분명한데도 불구하고, 지금까지의 방법은[eqn: {rm bold {(``f~``}}e{rm bold )}`]의 타입과 같아질 수(unifiable) 있는 타입을 가진 함수들이 모두 호출된다고 가정한다. 따라서,[eqn: {rm bold {(``f~``}}e{rm bold )}`]의 타입이 [eqn: alpha~` ->`` beta``]이면, 모든 함수가 호출될 수 있다고 가정하게 된다.

이러한 경우에는 실제로 프로그램에서 호출되는 함수를 쉽게 알 수 있는데도 불구하고 너무나 많은 다른 함수를 모아오게 된다. 따라서 프로그램 분석의 정학도가 떨어지게 된다. 다음 절에서는 이러한 문제를 해결하는 방법들에 대해서 알아본다.

3.2.2 인수로 전달된 함수의 호출

지금까지는 상위 개념의 함수 [eqn: f``]로 전달되는 함수들을 모으기 위해서 [eqn: f``]의 인수의 타입과 같아질 수 있는(unifiable) 함수들을 모두 모아왔다. 그러나, 3.2.1절에서 예를 통해 살펴본 것처럼, 여러 가지 타입을 갖는 함수 타입에 대해서는 필요 없이 너무나 많은 함수를 모아오게 된다.

본 논문에서 제안하는 방법은[eqn: ~f``]로 전달되는 함수가 무엇인지를 알고자 할 때,[eqn: ~f``]가 호출될 수 있는 장소(call site)를 모두 찾아가서, 그 곳에서[eqn: ~f``]로 전달되는 함수들을 모아오는 것이다. 즉, 프로그램 내의 모든 함수 호출 표현식들 중에서 함수[eqn: ~f``]가 호출될 수 있는 장소를 모두 찾은 후에, 그 곳에서 함수[eqn: ~f``]로 전달되는 함수들을 모두 찾아오는 것이다.

그러므로, 함수 [eqn: f``]의 인수로 전달된 함수 [eqn: g]를 호출할 경우에는 함수 [eqn: g]의 타입과 같아질 수 있는 타입을 가진 모든 함수를 모아오지 않는다. 그 대신에 함수 [eqn: f``]가 호출될 때 인수로 전달되는 실제 함수들을 찾아오게 된다.

3.2.3 커리 형태로 된 함수

다음의 예와 같은 커리 형태로 된 함수[eqn: ``rm bold f``]

[eqn: {rm bold {(``fn~x~``Rarrow~(``fn~y~``Rarrow~}}e{rm bold {))}}`]

가 다음과 같이 호출된다면,

[eqn: rm bold {((``f~``0`)~1`)}]

바깥쪽의 함수 호출이[eqn: {rm bold {(``fn~y~``Rarrow~}}e{rm bold {)}}`]를 호출한다는 것을 분명히 알 수 있다.

그러므로, [eqn: e_1]이 커리 형태로 된 함수[eqn: ``rm bold f``]를 호출하는 표현[eqn: {rm bold {(``f}}~``e{rm bold)}]라면,[eqn: {rm bold (``}e_1~ `e_2{rm bold )}]에 대해서 프로그램 흐름 분석을 할 때,[eqn: {rm bold {(``f}}~``e{rm bold)}]의 타입과 같아질 수 있는(unifiable) 타입을 가진 모든 함수를 모아오지 않는다. 그 대신에 커리 형태로 된 함수[eqn: ``rm bold f``]가 정의된 곳을 보고, 분명히 호출되는 함수인[eqn: {rm bold {(``fn~y~``Rarrow~}}e{rm bold {)}}`]를 찾아온다.

3.3 안전한 함수 흐름도 테이블 [eqn: bold Lam``]

3.1절에서 설명한 것처럼, 본 논문에서 제안하는 함수 흐름 예측 방법은 함수를 호출하는 모든[eqn: {rm bold {''}}``e_1~`` e_2 {rm bold ''}`]에 대해서, [eqn: e_1]의 타입과 같아질 수 있는(unifiable) 타입의 모든 함수를 모아오는 것이다. 이러한 함수 테이블은 실제로 [eqn: e_1]이 나타내는 함수들을 모두 포함해야 한다. 그런 의미에서 □안전한□ 함수 테이블을 다음과 같이 정의하기로 한다. 이 테이블은 L 프로그램(2장)을 대상으로 한다.

정의 3.1 ([eqn: bold {type` (e)`}]) 타입 [eqn: tau``]를 갖는 프로그램 [eqn: e`]에 대해서, [eqn: e`] 안에 있는 표현 [eqn: e']의 타입 [eqn: type_e (e')`]이 [eqn: tau']이라는 것은 (iff) 프로그램 [eqn: e`]의 타입 [eqn: tau``]를 유추하는 중에 [eqn: e']의 타입으로 [eqn: tau']이 유추되었다는 뜻이다. [eqn: type_e (e')`]의 첨자 [eqn: e`]가 없는 경우는 [eqn: e`]가 어떤 프로그램을 나타내는지 확실하게 알 수 있을 때 사용한다.

정리 3.1 (안전한 함수 흐름도 테이블[eqn: ~bold Lam`]) 주어진 프로그램 [eqn: e`]에 대해, [eqn: e`] 안의 함수 호출식에서 함수에 해당하는 표현식들의 집합을 [eqn: FtnExpr``]이라 하고, [eqn: e`] 안에 있는 함수들의 멱집합을 2LambdaExpr라 한다.

[eqn: Lam{it :}`` FtnExpr~ ->~]2LambdaExpr

을 다음의 방정식들을 만족하는 가장 큰 테이블이라고 정의한다:

[eqn: Lam`(lambda` x_tau . e`)`]	=	[eqn: \{`` lambda` x_tau . e``\}]	상수 함수
[eqn: Lam`(f``)`]	=	[eqn: \{`` lambda x_tau . e``]| 프로그램 내에 있는 fix[eqn: ~f~`lambda x_tau . e``\}]	이름이 붙여진 함수
[eqn: Lam`(x`)`]	=	[eqn: union`` \{``Lam` (e_2`)~|~e_1 ~e_2~ in~CallSites`(lambda`x_tau . e`)`\}]	함수를 나타내는 변수
[eqn: Lam`(e_1 ~e_2`)`]	=	[eqn: union`` \{``Lam` (e`)~|~lambda`x_tau . e~ in~Lam`(e_1` )`\}]	호출 결과 값인 함수
[eqn: Lam`(e`)`]	=	[eqn: \{`` lambda` x_tau . e`'``|``type(e)~ = ~type(lambda` x_tau . e') \}]	다른 표현식

[eqn: CallSites`(lambda` x_tau . e`)``=`` \{``]프로그램 내에 있는 [eqn: e_1 ~e_2~`` |~lambda` x_tau . e~in~Lam`(e_1 `)` \}]

□상수 함수□와 □이름이 붙여진 함수□는 프로그램 안에서 어떤 함수인지 쉽게 알 수 있는 함수이다. 반면에, □다른 표현식□은 프로그램 안에서 어떤 함수인지를 모르는 경우이므로 같은 타입을 갖는 함수들을 모두 모아오게 된다. □함수를 나타내는 변수□의 경우에는 3.2.2절에서 설명한 것처럼, 그 변수에 함수 값이 전달되는 곳을 찾아가서 실제로 전달받는 함수를 모아온다.

이렇게 정의한 [eqn: Lam`]의 안전성은 4장에서 정의하는 제약식 시스템 [eqn: ♤_1]과 연계하여 증명하였다. (정리 4.2)

이상으로 3장에서는 적은 비용으로 SML 프로그램의 함수 흐름도를 예측할 수 있는 방법에 대해서 알아보았다. 또한 프로그램 흐름을 예측할 때 정확도를 높이기 위해서 다루는 몇 가지 일에 대해서 알아보았다. 다음 장에서는 타입 정보를 이용하여 예측해낸 프로그램 흐름을 기반으로 하여 예외 상황을 분석하는 방법에 대하여 설명하고 그 안전성을 증명한다.

4. 예외 상황 분석 제약식의 도출

이 장에서는 집합 제약식(set constraints)를 이용한 예외 상황 분석 방법에 대해서 설명한다.

4.1 개요

3장에서 구한 프로그램 흐름도를 이용해서 프로그램 실행 중에 발생할 수 있는 예외 상황들의 집합을 집합 제약식들로 표현하고, 그 제약식들의 해를 구하면 예외 상황 분석의 결과가 된다. 본 논문에서는 예외 상황에 대한 관계를 각 함수마다 두 가지 집합 제약식으로 표현한다.

첫 번째 집합 제약식은 함수 [eqn: f``]를 실행하는 동안에 발생해서 소멸하지 않을 가능성이 있는 예외 상황들의 집합인데, [eqn: P_f``]로 표시한다. 예를 들어, 다음 함수[eqn: ``rm bold f``]

[eqn: rm bold {fun~``f(g)~=~g(0)``+``1}]

의 [eqn: P_f``]는[eqn: ``rm bold f``]에 전달될 수 있는 함수 [eqn: h``] 각각에 대한 [eqn: P_h``]의 합인 [eqn: union_{h}][eqn: P_h``]이 된다. 이 때,[eqn: ``rm bold g`]의 타입이[eqn: rm bold {"int"~rarrow~"int"}`]이므로,[eqn: rm bold {"int"~rarrow~"int"}`]와 같아질 수 있는(unifiable) 타입을 가진 모든 함수들이[eqn: ``rm bold f``]로 전달된다고 가정한다.

또 다른 예로, 다음 함수[eqn: ``rm bold f``]

[eqn: rm bold {fun~``f(x)~=~raise~x}]

의 [eqn: P_f``]는[eqn: ``rm bold f``]로 전달되는 예외 상황들의 집합이다.

두 번째 집합 제약식은 함수 [eqn: f``]를 실행하는 동안에 발생 가능한 예외 상황들의 집합이고, [eqn: X_f``]로 표시한다. 위의 예에서 함수[eqn: ``rm bold f``]에 대한 [eqn: X_f``]는[eqn: ``rm bold f``]를 호출하는 함수 [eqn: h``] 각각에 대한 [eqn: X_h``]의 합인 [eqn: union_{h}][eqn: X_h``]이 된다. 왜냐하면,[eqn: ``rm bold f``]를 호출하는 함수 [eqn: h``]는 [eqn: h``]를 실행하는 동안에 발생 가능한 예외 상황들을[eqn: ``rm bold f``]로 전달할 수 있기 때문이다. 이러한 함수 [eqn: h``]를 다 포함하는 집합은 인수의 타입이 예외 상황 타입인 함수를 호출하는 함수들의 집합이다. 예를 들어, 다음의 함수[eqn: ``rm bold h``]는 함수[eqn: ``rm bold f``]를 호출한다고 가정한다.

[eqn: rm bold {fun~``h(g)~=~cdots``~g`(`Error`)~``cdots}]

이렇게 각 함수마다 두 가지 집합 제약식을 만든 후에 이 제약식들의 집합을 푸는 것이 본 논문에서 제안하는 예외 상황 분석 방법이다. 전체 프로그램에서 제일 상위에 있는 함수(top-level function)를 [eqn: f``]라고 할 때, [eqn: f``]에 대한 [eqn: P_f``]의 해가 바로 전체 프로그램에서 발생돼서 소멸되지 않을 수 있는 예외 상황들이 된다.

4.2 집합 제약 시스템(set constraint system)

본 논문에서 제안하는 예외 상황 분석은 집합 제약식[16,17]을 이용하여서, 다음과 같은 세 가지 집합 제약 시스템을 통해 설명하기로 한다. [eqn: ♤_1](그림 4.1)은 각 표현식마다 그 식의 값에 대한 제약식과 그 식을 계산하는 중에 처리되지 않을 예외 상황에 대한 제약식을 만들어 낸다. [eqn: ♤_2](그림 4.3)은 [eqn: ♤_1]을 간단히 하여, 각 표현식의 예외 상황 값에 대해서만 제약식을 만든다. [eqn: ♤_3](그림 4.6)은 [eqn: ♤_2]를 더 간단히 하여, 각 표현식에 대해서가 아니라 각 함수에 대해서 제약식을 만든다.

실제로 본 논문에서 다루게 되는 예외 상황 분석은 [eqn: ♤_3]이고, 다른 두 가지 시스템들은 제안하고 있는 예외 상황 분석이 안전하다는 것을 증명하는 데에 사용된다.

예외 상황 분석의 입력으로 들어가는 L 프로그램은 모두 타입이 잘 정해져 있고(well-typed), L 프로그램 내의 모든 변수들은 유일하게 이름이 정해진다고 가정한다.

집합 제약식 방법에서 사용하는 표기법으로는 다음과 같은 것들이 있다. □제약식들의 모임□ [eqn: C`] 안에 있는 각각의 제약식 [eqn: X`` SUPSETEQ ``se``](집합 변수 [eqn: X`]와 집합 표현식 [eqn: se``])에 대하여 [eqn: se``]가 의미하는 집합 [eqn: I`(se)``]가 정의되어 있고 [eqn: I`(X`)`` supseteq ``I`(se)``]을 만족하면, [eqn: I``]는 제약식들 [eqn: C`]의 모델(해)라고 한다. [eqn: C`]의 가장 작은 모델(least model)을 [eqn: lm`(C`)``]라고 적기로 한다. 집합 제약식에서 사용되고 있는 연산자가 모두 단조적이고(monotonic) 모든 제약식의 왼쪽이 변수 하나이기 때문에, 모든 시스템([eqn: ♤_1, ♤_2, ♤_3])이 만들어내는 제약식들의 가장 작은 모델은 항상 존재한다는 것이 보장된다 [16].

4.2.1 구체적인 제약식(concrete constraint system) 만들기[eqn: ``bold ♤_1]

프로그램 안에 있는 각각의 표현식 [eqn: e``]에 대하여, [eqn: V_e``supseteq``se``]와 [eqn: P_e`` supseteq``se``]라고 하는 두 가지의 집합 제약식들을 만든다. [eqn: V_e``]는 [eqn: e``]가 가질 수 있는 값들의 집합을 나타내고, [eqn: P_e``]는 [eqn: e``]를 계산하는 도중에 발생돼서 처리되지 않는 예외 상황들의 집합을 나타낸다. 제약식 [eqn: V_e``supseteq``se``]의 뜻은 □표현식 [eqn: e``]가 [eqn: se``]의 값을 포함한 값들을 가질 수 있다.□라는 것이고, [eqn: P_e`` supseteq``se``]의 뜻은 □표현식 [eqn: e``]가 [eqn: se``]를 계산하는 도중에 발생돼서 처리되지 않는 예외 상황들을 포함한 예외 상황들을 갖는다.□라는 것이다.

그림 4.1

그림 4.1은 집합과 집합 표현식의 의미, 제약식을 만들어내는 규칙 등을 나타내고 있다. 제약식을 만들어내는 규칙에서 [eqn: V``]와 [eqn: P``]는 표현식이나 숫자로 이름 붙여진다. 다음의 예를 보면,

[eqn: [RS_{♤_1}]]  [eqn: {♤_1~~ e_1 :~ C_1} over {♤_1~~ {rm bold raise}~e_1 :~ \{ P_e`` supseteq`` V_1 ` { scale 70 union } `` P_1 \} ` { scale 70 union } `` C_1}]

[eqn: C_1]은 [eqn: V_{e_1}]과 [eqn: P_{e_1}]에 대한 제약식을 갖는데, 이 두 집합 변수들은 간단하게 각각 □[eqn: V_1]□과 □[eqn: P_1]□으로 적는다. 집합 변수 □[eqn: V_e`]□와 □[eqn: P_e`]□의 첨자인 □[eqn: e`]□는 위의 규칙이 적용되고 있는 표현식인[eqn: ``(rm bold raise~ it e_1`` )`]을 나타내고 있다.

[eqn: var``(x)``]는 [eqn: x``]를 인수로 갖는 함수가 호출될 때 [eqn: x``]에 전달되는 값들을 나타내고:

[eqn: I``(var`(x`)) = \{ v~ |~ ''e_1~ e_2 ''~ in~ e,~ lambda` x_tau . CDOT ` in`` I``(V_1 ), ~v~ in`` I``(V_2 ) \},]

[eqn: app_V`` (V_1 )`]은 [eqn: V_1`]에 있는 함수들의 결과 값을 나타낸다:

[eqn: I``(app_V `(V_1` ))~ =`` \{ v~ |~ lambda` x_tau . e~ in`` I``(V_1` ), ~v~ in`` I``(V_e` ) \}.]

마찬가지로, 첨자가 [eqn: P``]인 [eqn: app_P` (V_1 )``]은 [eqn: V_1`]에 있는 함수들을 수행하는 도중에 발생되고 처리되지 않는 예외 상황들을 나타낸다.

각각의 규칙은 [18]에 나와있는 규칙을 확장한 것이다. 즉, 각 표현식에 대하여 발생되어서 처리되지 않는 예외 상황들에 대한 제약식을 덧붙인 것이다. 처리 함수[eqn: {rm bold {''``` handle}}`` ~e_1 ``~lambda x_tau .e_2 {rm bold ''}`]에 대한 규칙인 [[eqn: HNDL_{♤_1}]]에서 제약식 [eqn: V_x~ supseteq``P_1``]은, 처리되는 표현 [eqn: e_1``]으로부터 발생되어 처리되지 않는 예외 상황들이 처리 함수[eqn: {rm bold {''}}``lambda` x_tau . e_2` {rm bold ''}`]의 인수로 전달된다는 것을 의미한다.

정리 4.1 ([eqn: bold ♤_1]의 타입 보존성(typefulness)) 자유 변수가 없는 표현식 [eqn: e``]에 대해서 [eqn: ♤_1 ~e`:``C_1]이라고 하면, [eqn: C_1`]의 가장 작은 모델인 [eqn: lm`(C_1` )``]은 타입을 유지(preserve)한다:

[eqn: FORALL e_i~ in`` e.~ lm`(C_1 `) (V_i )~ subseteq~ Val_{type`(e_i `)}] ([eqn: type`(e_i `)`]의 값들의 집합).

그림 4.2

[eqn: ♤_1]의 타입 보존성은 다음 절에서 설명하는 제약식 시스템 [eqn: ♤_2]와의 일관성(consistency)를 위해서 중요한 성질이다.

[eqn: ♤_1]이 틀리지 않다는 것(즉, 어떤 프로그램에 대한 [eqn: ♤_1]-제약식의 가장 작은 모델이 실제 그 프로그램의 값들과 발생되어 처리되지 않는 예외 상황들을 모두 포함한다는 것)은 본 논문에서 증명하지는 않았다. 이 증명은 [18]에 나와있는 증명 방법과 비슷하게 이루어진다.

4.2.2 예외 상황 제약식 만들기[eqn: `` bold ♤-_2]

이 절에서는 각 표현식이 갖는 값들에 대한 것이 아니라 단지 예외 상황의 이름들 [eqn: subseteq ~Exn``` =`` \{kappa_1,`` cdots,`` kappa_N \}]과 발생된 예외 상황들[eqn: `subseteq ~Exn``]만을 다루어서, [eqn: ♤_1]을 간단하게 만든 새로운 시스템[eqn: ♤_2](그림 4.3)에 대하여 설명한다. 즉, 함수 값들에 대한 제약식은 만들어내지 않고, 그 대신 각각의 함수 호출 표현식[eqn: {rm bold {''}}``e_1~`` e_2 {rm bold ''}`]에 대하여 [eqn: e_1`]이 나타낼 수 있는 함수들을 모두 모아오는 방법을 제안한다. 이러한 함수 테이블은 정리 3.1에서 정의한 [eqn: Lam`]을 사용한다.

그림 4.3

프로그램 안에 있는 각각의 표현식 [eqn: e``]에 대하여, [eqn: X_e`` supseteq`` se``]와 [eqn: P_e``supseteq``se``]라고 하는 두 가지의 집합 제약식들을 만든다. [eqn: X_e`]([eqn: Exn`]의 부분 집합)는 [eqn: e``]의 값을 이루는 예외 상황들의 집합을 나타내고,  [eqn: P_e``]([eqn: Packet`]의 부분 집합)는 [eqn: e``]를 계산하는 도중에 발생돼서 처리되지 않는 예외 상황들의 집합을 나타낸다.

예외 상황 값은 하나 이상의 예외 상황 이름을 가질 수 있다. 예를 들어, [eqn: kappa_1 (kappa_2 (1))]은 [eqn: kappa_1]과 [eqn: kappa_2]를 갖는다.

집합 변수의 이름을 붙이는 방법은 4.1절([eqn: ♤_1])에서와 같은 방법을 사용한다.

[eqn: rm bold -raise`]에 대한 규칙을 살펴보면:

[eqn: [-RS_{♤_2}]] [eqn: { ♤_2~~ e_1`:~ C_1} over {♤_2~~ {rm bold -raise}~e_1~ kappa_1``` cdots``` kappa_n `` :~ \{` P_e``` supseteq``` (`X_1~ "\"_{e_1}`` \{` kappa_1 , `cdots, `kappa_n \})`` {scale 70 union}`` P_1` \}`` {scale 70 union}`` C_1}]

제약식 [eqn: P_e``supseteq``P_1``]은 [eqn: e_1`]으로부터 발생되어 처리되지 않는 예외 상황들을 모아오고, 제약식 [eqn: P_e``supseteq``X_1``"\"_e`\{`kappa_1, ` cdots, ` kappa_n \}`]은 발생된 예외 상황들 중에서[eqn: ~kappa_i]들을 제외한 것을 모아온다. [eqn: "\"_e``]의 의미는 다음과 같다.

[eqn: I``(X_1`` "\"_e`` \{` kappa_1,` cdots,` kappa_n \} )`` =`` CASES {``I`(X_1 ) & ``type(e) = tau'`` exn`` {scale 70 wedge}``` isExn(tau')~일~ 경우 # & # ``I`(X_1 )``"\"``\{` kappa_1,` cdots,` kappa_n \} & ``그렇지~ 않을~ 경우}]

예외 상황 표현식의 타입이 예외 상황을 인수로 가질 때는[eqn: ~kappa_i]들을 제외하지 않는다. 이것은 예외 상황 분석의 안전성을 위해서 중요한 점이다. 다음과 같이 예외 상황 [eqn: kappa_2 (1)]을

인수로 갖는 예외 상황 [eqn: e`]를 [eqn: rm bold -raise`]하는 경우로 예를 들어 본다. (즉, [eqn: kappa_1 (kappa_2 (1))`]을 [eqn: e`]라고 하자.)

[eqn: rm bold -raise`] [eqn: kappa_1 (kappa_2 (1))~~ kappa_2]

만약에 [eqn: X_e``=``\{`kappa_1 ,``kappa_2 \}`]에서[eqn: ~kappa_2]를 제외했다면, 나중에 나오는 처리 함수에 의해서 [eqn: kappa_1 (kappa_2 (1))`]을 처리할 때 디컨스트럭트해서[eqn: ~kappa_2]를 다시 발생시킬 수 있음에도 불구하고 빠뜨리게 되는 것이다. 그러므로 집합-뺄셈 연산자인 [eqn: "\"_e`]는 [eqn: e`]가 인수로 예외 상황을 갖지 않을 경우에만 적용된다. (교집합 연산자인 [eqn: cap_e`]도 같은 이유로 해서 예외 상황을 인수로 갖는 예외 상황에는 적용하지 않는다.)

함수 호출에 사용되는 집합 표현식 [eqn: app(e_1 )`]은 [eqn: ♤_1]에서와 비슷하게 사용되는데, 호출되는 함수가 [eqn: Lam{it :}`` FtnExpr~ ->~]2LambdaExpr라는 테이블을 사용하여 얻어진다는 점이 다르다.

정의 4.1 [eqn: Lam`]이 [eqn: ♤_1]에 대해서 안전하다는 것은 (iff) 프로그램 [eqn: e`] 안에 있고 함수을 갖는 각각의 표현식 [eqn: e'`]에 대해서[eqn: ``♤_1~ e`:``C`]이면[eqn: ``Lam`(e')``supseteq``lm`(C)`(V_e' )`]이라는 것을 뜻한다.

정리 4.2 ([eqn: bold Lam`]의 안전성(correctness)) [eqn: Lam`](3.1)은 [eqn: ♤_1]에 대해서 안전하다.

그림 4.4

[eqn: Lam`]이 [eqn: ♤_1]에 대해서 안전하면 [eqn: ♤_2]는 [eqn: ♤_1]의 안전한 근사값(approximation)이다:

정리 4.3 ([eqn: bold ♤_2]의 안전성(correctness)) 자유 변수가 없는 표현식 [eqn: e`]에 대해서,[eqn: ``♤_1~ e`:``C_1`] 이고[eqn: ``♤_2~ e`:``C_2`]이며, 각각의 가장 작은 모델이 [eqn: I_1``=``lm`(C_1 )]과 [eqn: I_2``=``lm`(C_2 )]라고 가정한다. 만약에 [eqn: Lam`]이 [eqn: ♤_1]에 대해서 안전하다면, [eqn: e`] 안에 있는 각각의 표현식 [eqn: e_i`]에 대해서:

[eqn: I_2`(X_i )``supseteq``|`I_1` (V_i )`|] 이고 [eqn: I_2`(P_i )``supseteq``|`I_1` (P_i )`|] 이다.

여기에서 [eqn: |V```|]는 [eqn: V``] 안에 있는 예외 상황들을 이루는 예외 상황 이름들의 집합이다.

[eqn: |V```| {scale 70 {def} atop {=}} \{ `kappa``|``kappa~ v~in V`` \}~ union~ | \{v``|``kappa~v~in V`` \}` |]

그림 4.5

4.2.3 함수의 예외 상황 제약식 만들기[eqn: ``bold ♤_3]

마지막으로, [eqn: ♤_2]를 더 간단하게 하여 새로운 시스템 [eqn: ♤_3](그림 4.6)를 만든다. 새로운 시스템에서는 각 표현식에 대해서 제약식이 만들어지는 것이 아니라 각 함수에 대해서 만들어진다. 따라서 정확도(accuracy)가 줄어들기는 하지만, 풀어야 할 제약식의 갯수가 매우 많이 줄어들게 된다. 입력 프로그램에 대한 [eqn: ♤_3]-제약식의 가장 작은 모델이 본 논문에서 제안하고 있는 예외 상황 분석의 결과이다.

그림 4.6

[eqn: ♤_3]에서는 집합 변수들의 이름이 프로그램 내에 있는 함수와 처리되는 표현식들에 의해서 붙여진다. 모든 함수와 처리되는 표현식들은 유일하게 이름이 붙여진다고 가정하고, 각 함수에는 이름을 첨자로 붙여준다:[eqn: {rm bold {''```}}lambda_f~ x_tau .e{rm bold ''}`]. 마찬가지로 예외 상황 처리 표현식 [eqn: {rm bold {''``` handle}}`` ~e_g ``~lambda_h`` x_tau .e_2 {rm bold ''}`]의 처리되는 표현식에도[eqn: {rm bold {''```}}e_g{rm bold ''}`]처럼 이름을 붙여준다.

프로그램 안에 있는 각각의 함수 (또는 처리되는 표현식) [eqn: f``]에 대하여, [eqn: X_f``supseteq``se``]와 [eqn: P_f``supseteq``se``]라고 하는 두 가지의 집합 제약식들을 만든다. [eqn: X_f``]는 [eqn: f``] 안에서 □사용 가능한□ 예외 상황들의 집합이고, [eqn: P_f``]는 [eqn: f``]의 수행 중에 발생되어 처리되지 않는 예외 상황들의 집합이다.

함수 호출 표현식에 대한 규칙을 보면:

[eqn: [APP_{♤_3}]] [eqn: { f~ ♤_3~~ e_1`:`` C_1~~~~~~~~~ f~ ♤_3~~ e_2`:`` C_2`} over {f~♤_3~~ e_1~`` e_2`` :~ \{`` X_f~`` supseteq`` app_X`` (e_1 , `X_f` ),~ P_f~`` supseteq`` app_P`` (e_1 , `X_f` ) \}` {scale 70 union}`` C_1 ` {scale 70 union}`` C_2}]

[eqn: {rm bold {''```}}f~``♤_3 ~e`{rm bold ''}`]의 왼쪽에 있는 [eqn: f``]는 표현식 [eqn: e`]가 [eqn: f``] 안에서 나타난다는 것을 표현하고 있다. 따라서 [eqn: f``] 안에[eqn: ~e_1~` e_2`]라는 함수 호출식이 있다면, [eqn: f``] 안에서 사용 가능한 예외 상황들 [eqn: X_f``]는 이 호출식에서 결과 값으로 전달하는 예외 상황들인 [eqn: app_X` (e_1 ,` X_f` )`]을 포함해야 한다. 또한 [eqn: P_f``]는 이 호출식을 수행하는 동안 발생되어 처리되지 않는 예외 상황들인 [eqn: app_P` (e_1 ,` X_f` )`]을 포함해야 한다.

변수에 대한 규칙 [[eqn: VAR_{♤_3}]]을 보면, 제약식들이 함수에 대하여 만들어지기 때문에 변수[eqn: ~x`]에 대한 제약식은 두 가지 함수에 의해서 표현되어야 함을 알 수 있다: 하나는 변수[eqn: ~x`]가 예외 상황을 제공하는 함수[eqn: ~f``]이고, 다른 하나는[eqn: ~x`]에게 예외 상황을 제공하는 함수[eqn: ~g``]이다.[eqn: ~f``]는[eqn: {rm bold {''```}}♤_3 ~x`{rm bold ''}`]의 왼쪽에 나타나는 함수이고,[eqn: ~g``]는[eqn: ~x`]를 인수로 갖는 함수[eqn: (Owner`(x))`]이다. 각각의 경우[eqn: ~x`]에 대한 제약식이 만들어지는데, 하나는[eqn: ~x`]를 만났을 때 만들어지고:

[eqn: [VAR_{♤_3}]] [eqn: ~f~♤_3~~ x``:~ \{ X_f~` supseteq~ X_{Owner`(x)} \}]

다른 하나는[eqn: ~x`]의 주인인 [eqn: Owner`(x)`({scale 70 {let} atop {=}}~g~)]가 호출될 때 [eqn: app_X`(e_1 , `X_f `)`]의 세 번째 조건인 [eqn: I`(X_g `)``supseteq``I`(X_f `)]에 의해서 만들어진다:

[eqn: I`(app_X` (e_1 ,` X_f` ))`` =`` \{` kappa`` |`` lambda_g`` x_tau . e~ in~ Lam`(e_1 ),~ kappa~ in~ I`(X_g ),~ I`(X_g )`` supseteq`` I(X_f` )) \}]

[eqn: ♤_3]은 [eqn: ♤_2]의 안전한 근사값이다:

정리 4.4 ([eqn: bold ♤_3]의 안전성) 자유 변수가 없는 표현식 [eqn: e``]에 대해서, [eqn: ♤_2 ~e` :``C_2``]이고 [eqn: {rm bold main}`` ♤_3 ~e`:``C_3``]이며, 각각의 가장 작은 모델이 [eqn: I_2`` =`` lm`(C_2 )`]와 [eqn: I_3`` =`` lm`(C_3 )`]라고 가정한다. 만약에[eqn: {rm bold main}`` ♤_3 ~e`:``C_3``]를 계산하는 동안에 [eqn: g~♤_3~ e'`: C`'``]이 나타난다면,

[eqn: I_3` (X_g `)``supseteq``I_2` (X_e' )] 이고 [eqn: I_3` (P_g `)``supseteq``I_2` (P_e' )] 이다.

그림 4.7

4.2.4 정확도에 대하여

[eqn: ♤_2]와 [eqn: ♤_3]의 제약식 규칙들은 안전성을 해치지 않으면서 좀 더 정확하게 만들어질 수 있다.

먼저, [eqn: ♤_2]의 규칙을 변화시켜서 예외 상황 타입을 갖는 표현식들만 예외 상황을 갖도록 만들 수 있다. 즉, 새롭게 바꾼 규칙 [[eqn: DCON_{♤_2}]]는 다음과 같다.

[eqn: [DCON_{♤_2}]] [eqn: { ♤_2~~ e_1`:~ C_1} over {♤_2~~ {rm bold decon}~ e_1` :~ \{ X_e`` supseteq`` (X_1` |` isExn`(type`(e))),~ P_e`` supseteq`` P_1 \} ``{scale 70 union}`` C_1 }]

여기에서 [eqn: I`(X`|`cond``)`]는 [eqn: cond`]가 참(true)이면 [eqn: I`(X`)`]이고 거짓(false)이면[eqn: ~EMPTYSET]이다. 새로운 시스템 [eqn: ♤_2]가 [eqn: ♤_1]에 대하여 안전한 근사값이라는 것(정리 4.4)도 증명될 수 있다. 또한 [eqn: ♤_2]의 타입 보존성도 증명될 수 있다: 프로그램 [eqn: e`]에 대한 새로운 [eqn: ♤_2]-제약식의 가장 작은 모델을 [eqn: I_2`]라고 가정하면, [eqn: FORALL` e_i~` in`` e.` LNOT`` isExn`(type`(e_i` ))`]이면 [eqn: I_2` (X_i` ) = emptyset`]이다.

다음으로, [eqn: ♤_3]을 다음과 같이 바꾸어서 정확도를 높일 수 있다. 한 가지는 함수[eqn: ~f``]의 인수[eqn: ~x``]가 예외 상황 타입을 가질 때에만[eqn: ~f``]가[eqn: ~x``]를 통해서 예외 상황을 전달받도록 하는 것이다. 다른 한 가지는 함수[eqn: ~f``]의 결과 값의 타입이 예외 상황 타입일 경우에만[eqn: ~f``]를 호출한 함수에게[eqn: ~X_f``]를 전달하도록 하는 것이다. 이러한 것들을 추가한 규칙은 다음과 같다.

[eqn: I`(app_X`(e_1 ,{it X}`))]	[eqn: =]	[eqn: \{`kappa``|``lambda_f``x_tau . e~in```Lam`(e_1 ),~ kappa``in`` I`(X_f`|`isExn`(type`(e))),] [eqn: ~~~~I`(X_f )``supseteq``I`(X`|`isExn`(tau)) \}]
[eqn: I`(app_P`(e_1 ,{it X}`))]	[eqn: =]	[eqn: \{`kappa``|``lambda_f``x_tau . e~in```Lam`(e_1 ),~ kappa```in```I`(P_f`),~I`(X_f )```supseteq``` I`(X`|`isExn`(tau)) \}]
[eqn: I`(var`(x`))]	[eqn: =]	[eqn: I`(X_{Owner`(x`)}`|`isExn(type`(x`)))]
[eqn: X_f``]	[eqn: supseteq`]	[eqn: app_X` (cdots) {scale 70 union}``(X_g`|`isExn(type`(e_g`)))~~~~~~~~~~~ rm \in~ [HNDL_{♤_3}]]

새로운 시스템 [eqn: ♤_3]이 맞다는 것도 [eqn: ♤_2]의 타입 보존성을 사용하여 증명할 수 있다. 이러한 성질들은 앞에 나와있는 증명들과 비슷한 방법으로 증명할 수 있다. 실제로 예외 상황 분석의 구현에서는 새로운 시스템 [eqn: ♤_3]의 규칙을 사용한다.

4.3 [eqn: bold ♤_3]을 Standard ML에 적용

L 언어에서 제공하는 모든 함수는 오로지 하나의 타입만을 가지고 있지만, 실제로 SML은 여러 가지 타입으로 구체화될 수 있는(polymorphic) 타입을 가지고 있고 예외 상황과 함수 외에도 다른 여러 가지 타입을 갖기 때문에, [eqn: ♤_3]을 SML 프로그램에 적용하기 위해서는 두 함수 [eqn: isExn`](그림 4.3)과 [eqn: Lam`](정리 3.1)의 정의를 바꾸어주어야 한다.

여러 가지 타입으로 구체화될 수 있는 타입 때문에, [eqn: isExn`]은 보존력(conservative)이 있어야 한다. 이러한 [eqn: isExn`]의 새로운 정의는 다음과 같다.

[eqn: isExn`(iota{scale 80 vee}~ tau``` ->`` tau'`)]	[eqn: =]	false	상수 또는 함수 타입
[eqn: isExn`(alpha {scale 80 vee}~ tau~ exn`)]	[eqn: =]	true	일반적 또는 예외 상황 타입
[eqn: isExn`(tau~ ref```)]	[eqn: =]	[eqn: isExn`(tau`)]	레퍼런스(reference) 타입
[eqn: isExn`(u`)]	[eqn: =]	[eqn: EXIST `kappa`` in`` Con`(u).`isExn`(Arg`(kappa`))]	사용자 정의 데이터 타입 u

마지막 규칙은 데이타 컨스트럭터 [eqn: kappa`` in`` Con`(u`)]가 예외 상황을 인수로 받는 경우를 위한 것이다.

[eqn: Lam`]의 새로운 정의를 만들기 전에 먼저, 여러 가지 타입으로 구체화될 수 있는 타입(polymorphic type)의 프로그램들을 하나의 타입을 갖는 프로그램으로 변환시킨다. 즉 여러 가지 타입으로 구체화될 수 있는 타입의 함수가 사용된 곳을 찾아가서, 각각의 구체화된 타입으로 대체시키는 것이다.

그러므로, 어떤 함수 표현식의 타입과 같은 타입으로 구체화될 수 있는 타입을 갖는 함수는 그 함수 표현식이 호출되는 곳에서 호출될 수 있다. 그러므로 [eqn: Lam`]의 마지막 규칙은 두 타입이 서로 같은지를 검사하는 것이 아니라, 서로 같은 타입이 될 수 있는지 (type unifiability)를 검사해야 한다.

[eqn: Lam`(e)`` =`` \{`lambda x.e'~|``type_SML`(e)]는 [eqn: type_SML `(lambda x.e')]과 같아질 수 있다.[eqn: \}`]

[eqn: type_SML`(e)`]의 정의는 다음과 같다.

정의 4.2 ([eqn: bold {type_SML`(e)`}]) 타입 [eqn: tau``]를 갖는 SML 프로그램 [eqn: e`]에 대해서, [eqn: e`]안에 있는 표현식 [eqn: e'`]의 타입 [eqn: type_SML`(e')`]이 [eqn: tau'']이라는 것은 (iff) 1. 프로그램[eqn: ~e`]의 타입 [eqn: tau``]를 유추하는 중에 [eqn: e'`]의 타입으로 [eqn: tau']이 유추되었고, 2. [eqn: tau'] 안에 있는 모든 타입 변수들의 이름을 유일하게 붙인 결과가 [eqn: tau'']이라는 뜻이다.

이 장에서는 본 논문에서 제안하고 있는 예외 상황 분석 방법으로, 각 함수에 대한 집합 제약식을 만드는 방법에 대해서 알아보았다. 다음 장에서는 지금까지 설명한 방법들을 구현한 결과에 대해서 알아본다.

5. 예외 상황 분석기의 구현

그림 5.1

본 논문에서는 SML/NJ 108.13[21]의 컴파일러 소스 코드를 이용하여 예외 상황 분석기를 구현하였다. 먼저, SML/NJ 108.13 컴파일러의 내부 표현인[eqn: rm bold absyn]을 입력으로 받아서 프로그램 내의 함수 흐름을 분석하여 테이블로 구현한다. 다음으로 그 테이블을 이용해서 각 함수에 해당하는 제약식([eqn: P_f``]와[eqn: ~X_f`])을 만든다. 이 제약식은 Z1[22,23]이라고 하는 도구를 이용해서 풀 수가 있다. 이 과정은 그림 5.1과 같다.

각 함수에 대한 [eqn: P_f``]와[eqn: ~X_f`]의 제약식을 만든 후에, 그 제약식의 해는 전통적인 반복 부동점 방법(iterative fixpoint method)에 의해서 구해진다. 본 논문에서는 예외 상황 분석을 해서 만들어진 제약식을 해결하는 데 Z1을 사용하였다. Z1은 재귀적으로 만들어진

제약식의 집합을 입력받아서, 그 제약식의 가장 작은 해를 구하는 프로그램을

출력한다.

이 장에서는 본 논문에서 제안한 예외 상황 분석 방법의 구현에 대해서 설명하였다. 다음 장에서는 본 논문의 결론을 맺는다.

6. 결론 및 토의

SML에서는 프로그래머가 예외 상황의 발생과 소멸을 간편하고 자유롭게 표현할 수 있으므로 프로그램 내에서 매우 유용하게 사용되고 있다.

그러나 예외 상황은 프로그래머가 주의 깊게 사용하지 않을 경우에는 프로그램의 안전에 문제로 작용할 수가 있다. 프로그램 실행 중에 발생한 예외 상황이 처리되지 않으면 프로그램이 갑작스럽게 중단되기 때문이다.

본 논문에서는 프로그램 실행 중에 발생해서 처리되지 않을 수 있는 예외 상황들을 프로그램을 실행하기 전에 예측해내는 분석 방법을 제안한다. 이 방법은 SML/NJ 컴파일러가 타입 유추를 통해 제공하는 타입 정보를 이용해서, 프로그램의 함수 흐름을 분석하여 함수 흐름도를 만들어낸다. 이 함수 흐름도를 이용하여 예외 상황 분석에 대한 제약식을 만들어내고, 이 제약식의 가장 작은 해를 구하면 이 분석의 결과가 된다. 본 논문에서 제안하고 있는 분석 방법이 틀리지 않다는 것을 집합 제약식을 이용하여 증명하였다.

이 분석 방법을 구현하여 실제 프로그램에 실험해 본 결과, 적절한 비용 대 성능비를 가지고 있는 것으로 밝혀졌다. 예를 들어 ML-lex 프로그램을 분석하는 데 약 1.36초가 걸렸다. 정확도에 대해서는, 10개의 예외 상황 중에서 실제로 발생해서 소멸되지 않는 3개의 예외 상황만을 정확하게 찾아낸다.

이 분석 방법을 완전히 구현하여 SML/NJ 컴파일러에 장착되도록 하기 위해서는 다음과 같은 일들이 필요하다. 먼저, SML의 모듈 시스템으로 확장시켜서 전체 프로그램이 없어도 프로그램의 일부분을 분석할 수 있게 하는 것이다. 다음으로, 구현 방법을 개선하여 실험 결과의 성능 향상을 얻는 것이다.

참고 문헌

[1]	Niklaus Wirth. A plea for lean software. IEEE Computer, 28(2):64-68, February 1995.
[2]	T. Andrews. Designing linguistic interface to an object database or what do C++, SQL, and hell have in common? In Proceedings of the 4th International Workshop on Database Programming Languages - Object Models and Languages. Springer-Verlag, 1993.
[3]	Guy L. Steele, Jr. Principled design of programming languages. Invited presentation of ACM '94 Conference on Programming Language Design and Implementation, 1994.
[4]	Andrew W. Appel. A critique of Standard ML. Journal of Functional Programming, 3(4):391-430, 1993.
[5]	Dennis M. Ritchie. The development of the C language. In ACM SIGPLAN Notices, 28(3), History of Programming Languages Conference (HOPL-II), pages 201-208. ACM SIGPLAN, 1993.
[6]	Robin Milner, Mads Tofte, and Robert Harper. The Definition of Standard ML. MIT Press, 1990.
[7]	Robin Milner and Mads Tofte. Commentary on Standard ML. MIT Press, 1991.
[8]	David B. Macqueen and Andrew W. Appel. Standard ML of New Jersey. Technical memorandum, AT&T Bell Labs., 1993.
[9]	Jeffrey D. Ullman. Elements of ML Programming. Prentice-Hall, 1994.
[10]	Luis Damas and Robin Milner. Principal type-scheme for functional programs. In Proceedings of the ACM Symposium on Principles of Programming Languages, 1982.
[11]	Juan Carlos Guzm□n and Asc□nder Su□rez. A type system for exceptions. In Proceedings of the ACM SIGPLAN Workshop on ML and its Applications, June 1994.
[12]	Jean-Piere Talpin and Pierre Jouvelot. Polymorphic type, region and effect inference. Journal of Functional Programming, 2(3):245-271, July 1992.
[13]	Manuel Fahndrich and Alex Aiken, May 1996. (personal communication).
[14]	Kwangkeun Yi. Compile-time detection of uncaught exceptions for Standard ML programs. In Lecture Notes in Computer Science, volume 864. Proceedings of the first international static analysis symposium edition, 1994. http://compiler.kaist.ac.kr/~kwang/paper/94-sas-yi.ps.
[15]	Patrick Cousot and Radhia Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Conference Record of the 4th ACM Symposium on Principles of Programming Languages, 1977.

[16]	Kwangkeun Yi, Sukyoung Ryu, and Ky-Hyun Pyun. Estimating uncaught exceptions in standard ml programs from type-based equations. pages 455-460. Proceedings of the 20th annual international computer software and applications conference edition, May 1996.
[17]	J. A. Robinson. A machine-oriented logic based on the resolution principle. Journal of the ACM, 12(1):23-41, 1965.
[18]	Nevin Heintze. Set Based Program Analysis. PhD thesis, Carnegie Mellon University, October 1992.
[19]	Alex Aiken and Nevin Heintze. Constraint-based program analysis. POPL'95 Tutorial, January 1995.
[20]	Nevin Heintze. Set based analysis of ml programs. Technical Report CMU-CS-93-193, Carnegie Mellon University, July 1993.
[21]	Patrick Cousot and Radhia Cousot. Compositional and inductive semantic definitions in fixpoint, equational, constraint, closure-condition, rule-based and game-theoretic form. In Lecture Notes in Computer Science, volume 939, pages 293-308. Proceedings of the 7th international conference on computer aided verification edition, 1995.
[22]	Joseph E. Stoy. Denotational Semantics: the Scott-Strachey Approach to Programming Language Theory. MIT Press, 1977.
[23]	http://compiler.kaist.ac.kr/~cookcu/sml/mirror/.
[24]	Kwangkeun Yi and Williams Ludwell Harrison III. Automatic generation and management of interprocedural program analyses. In Proceedings of the Annual ACM Symposium on Principles of Programming Languages, pages 246-259, January 1993. http://compiler.kaist.ac.kr/~kwang/paper/popl93.ps.