서 론

실행시간 전문화를 위한 집합기반분석의 준비

(Preparing Set-Based Analysis for Run-time Specialization)

어 현 준     이 광 근

(Hyunjun Eo) (Kwangkeun Yi)

요 약 정적 분석을 사용하여 프로그램의 입력에 의존하는 성질을 예측하는 방법을 제안한다. 제안된 방법은 입력에 무관한 성질을 예측하도록 설계된 정적 분석을 입력에 의존하는 성질을 예측하는 분석으로 변환한다. 이 방법은 실행 중에 프로그램의 성질을 알아내기 위해서 실행중인 프로그램을 관찰하는 코드가 필요 없고 계측된 자료를 모으는 과정도 필요 없다.

정적 분석의 가장 마지막 부분을 프로그램의 실행 시간으로 미루는 것이 이 논문의 핵심 아이디어다. 먼저 정적 분석을 분석하여, 프로그램의 입력에 민감하여 프로그램의 실행시간으로 연기되어야 하는 부분을 찾아낸다. 그 후, 값을 자르는 분석을 사용하여 이 부분을 재구성하여 프로그램의 입력에 대한 간단한 멤버쉽 테스트에 의해 분석이 풀어질 수 있도록 한다. 이런 재구성 과정을 통해 준비된 분석들은 프로그램의 입력이 나타나기만 하면 순간적으로, 동시에 풀려질 수 있다.

모든 과정은 엄밀하게 정의되고 증명되었다.

Abstract We present a technique of using static analysis for estimating program's input-dependent properties. A static analysis that is originally designed for estimating the input-independent properties of programs is transformed into one that can safely estimate the input-dependent properties at the programs' input occurrence. No profile is collected and no probing codes inside the running program are needed.

Our idea is to defer the finish of the static analysis to the program's run-time. By analyzing the static analysis, we identify the parts of the analysis that are sensitive to the program's inputs, hence need to be deferred to the program's run-time. Then by using an analysis named static value-slicing, we short-cut some of the dynamic parts so that they are solved by simple membership tests for the program's input. This re-formulation accelerates the analysis; once the program's input occurs the prepared dynamic parts can immediately and simultaneously start to resolve.

Every step of our technique is formally defined and proven correct.

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

1.1 동기

입력에 무관한 프로그램의 성질들은 최적화된 코드를 생성하기 위해 필요하다. 그러나 만약, 자주 사용되는 입력에 맞게 프로그램을 맞추고 싶다면, 입력에 의존하는 프로그램의 성질들도 필요하게 된다.

입력에 의존하는 성질들을 얻는 방법으로 가장 일반적인 것은 프로파일(profile)이다. 프로파일 기반 최적화 기법들은 프로파일된 결과들의 통계를 사용하여 가장 많이 사용된 입력에 대해 최적화된 목적 코드를 생성하게 된다.

그러나, 프로파일 기반 분석들은 몇 가지 단점을 가지고 있다. 프로파일 자료로부터 얻어진 프로그램의 성질들은 몇 가지 최적화 기법들에 적용하기에는 부족하다. 일반적으로 프로파일된 통계 자료는 프로그램의 흐름이 특정 경로를 얼마나 자주 따라 갔나를 세는 것이다. 이런 정보는 분기 예측(branch prediction)에 민감한 최적화 기법들에는 유용하다. 그러나 병렬화와 같은 다른 최적화 방법들은 프로그램 변수들이 어떻게 읽혀지고 쓰여졌는가에 대한 정보를 필요로 하고, 이를 관찰하기 위해서는 프로그램의 어떤 경로가 몇 번 수행되었는지를 세는 것 보다 더 많은 정보를 관찰할 필요가 있다. 게다가, 그런 정교한 실행시간 성질들을 수집하기 위해서는 프로그램의 실행에 훨씬 더 많은 부담(overhead)을 가지게 된다. 현재의 경로를 세는 프로파일은 15%-30%[1, 2]의 실행시간 부담이 있다. 프로그램의 내부에서 프로그램을 계측하는 코드가 더 복잡해지게 되면, 프로파일 부담과 정확성 사이의 균형을 맞추는 일은 더 어려워진다.

프로파일을 하지 않고 입력에 의존하는 프로그램의 성질들을 추정하는 일반적인 기술이 필요하다. 이런 상황은 글로벌 컴퓨팅 환경, 그리고 웹 컴퓨팅 환경에서 더욱 요구되어진다. 다수의 코드 소비자(사용자)가 네트웍 너머의 코드 제공자(컴파일러)와 떨어져 있는 상황을 생각해 보자. 코드 제공자는 소스 프로그램을 컴파일하고, 컴파일된 코드를 네트웍의 다른쪽 끝에 있는 소비자에게 전달한다. 이 경우 입력에 의존하는 최적화들은 각각의 소비자들에게 위임된다. (만약 위임하지 않는 다면, 코드 제공자는 각각의 소비자들의 입맛에 맞는 코드를 만들기 위해서 궁지에 몰리게 될 것이다.) 소비자들은 소스 프로그램에 접근할 수 없기 때문에, 전달된 목적 코드에 대한 최적화는 제한될 수밖에 없다. 반면에, 코드 제공자는 각각의 소비자들의 입력 패턴에 맞추는 적극적인 최적화를 제공하기를 원한다. 코드 제공자가 원하는 적극적인 최적화는 소스 레벨에서의 정교한 프로그램 분석을 필요로 한다.

따라서, 다음의 시나리오가 예상된다. 코드 제공자는 입력에 의존하는 소스 프로그램의 성질을 소비자 싸이트(site)에서 예측할 수 있는 분석을 준비한다. 코드 제공자는 또한 추정된 소스 프로그램의 실행시간 성질로부터 최적화된 코드를 어떻게 생성할 지에 관한 정보를 가지고 있다. 코드 제공자는 소비자에게 컴파일된 목적 코드와 함께 이 두 가지 정보 - □소스 프로그램에 대한 준비된 분석 A□, □목적 코드에 대한 최적화 계획 O□ - 를 전달한다 (그림 1). 코드 소비자는 전달된 코드를 수행한다. 입력이 발생하면 코드의 수행과는 무관하게, 준비된 분석 A는 소스 프로그램의 동적 성질들을 추정한다. A에 의해 분석된 결과는 최적화 계획 O를 활성화 시켜서 입력에 맞게 최적화된 목적 코드를 생성하게 한다. 다음에 비슷한 입력이 발생하게 되면, 소비자는 원래의 코드 대신에 최적화된 코드를 수행한다.

1.2 개관

이 논문은 프로그램의 입력에 의존하는 성질을 추정하는 분석인 □준비된 분석 A□를 디자인하기 위한 방법을 제시한다. 이 방법은 정적 분석의 틀을 기반으로 한다. 프로그램과 무관한 성질들을 추정하도록 고안된 정적 분석은 프로그램의 입력이 나타났을때 입력에 의존하는 성질들을 안전하게 추정할 수 있는 분석으로 변환된다. 프로파일은 필요없고, 실행중에 프로그램의 상태를 조사하기 위한 코드도 필요없다.

아이디어는 단순히 정적 분석의 마지막을 프로그램의 실행시간으로 연기하는 것이다. 정적 분석을 분석하여, 프로그램의 입력에 민감한 부분들을 찾아낸다. 그리고 나서, 값을 자르는 분석을 통하여 이런 부분들이 입력에 대한 간단한 멤버쉽(membership) 테스트만으로 풀려질 수 있도록 단축시킨다. 이러한 재구성은 프로그램의 입력이 나타나기만 하면 준비된 분석이 순간적으로, 동시에 풀려질 수 있도록 준비한다.

예를 들어, 입력 [eqn: alpha]에 의존하는 다음 식(expression)의 값을 추정하는 분석을 생각해보자.

if e = 0 then 1 else 2

식의 값 [eqn: X``]는 다음과 같은 조건부 집합 관계식이다.

[eqn: X_e`][eqn: supseteq][eqn: 0] [eqn: Rightarrow] [eqn: X][eqn: supseteq][eqn: 1]

[eqn: X_e`][eqn: supseteq] {[eqn: n][eqn: |][eqn: n][eqn: not = 0] } [eqn: Rightarrow] [eqn: X][eqn: supseteq][eqn: 2].

조건식 [eqn: e]가 입력에 의존하는 식이라고 가정하자.

조건식의 값은 컴파일 시간에 알 수가 없기 때문에, 컴파일러는 if식의 값이 {[eqn: 1,2] }라는 결론을 내야 한다. 실행시간에는 [eqn: X_e`]의 값을 알 수 있으므로 더 정확한 결과를 결정할 수 있다. 다음과 같이 [eqn: X_e`][eqn: supseteq] {[eqn: 0] }와 [eqn: X_e`][eqn: supseteq] {[eqn: n]|[eqn: n][eqn: not=0] }를 입력[eqn: alpha]의 [eqn: V``]와 [eqn: W```]에 대한 멤버쉽 테스트로 재구성하면, 분석 결과를 더 빠르게 얻을 수 있다.

[eqn: alpha][eqn: in][eqn: V``] [eqn: Rightarrow] [eqn: X][eqn: supseteq] {[eqn: 1] }

[eqn: alpha][eqn: in][eqn: W```] [eqn: Rightarrow] [eqn: X][eqn: supseteq] {[eqn: 2] }

else [eqn: Rightarrow] [eqn: X][eqn: supseteq] {[eqn: 1,`` 2] }.

실행시간에 입력 [eqn: nu``]이 발생하면, 이 조건들은 [eqn: X_e`]가 계산되어질 때까지의 지연 없이 바로 참이나 거짓으로 결정된다. 따라서 입력 [eqn: nu``]에 따른 식의 값 [eqn: X``]가 빠르게 추정될 수 있다. [eqn: V``]와 [eqn: W```]는 (또 다른 정적 분석에 의해) 컴파일 시간에 추정되기 때문에 모든 값을 커버할 필요는 없다. 몇몇 입력은 [eqn: V``][eqn: cup][eqn: W```]에 포함되지 않을 수 있고, 이런 경우는 정적 분석의 결과와 같은 정확도의 분석 결과를 낸다.

1.3 논문의 구조

2절에서는 소스 언어 L을 소개한다. 3절은 입력 변수를 가지는 L 프로그램에 대한 정적 분석을 소개한다. 이 분석으로부터, 입력에 의존하는 성질을 추정하는 동적 분석을 정의한다. 4절과 5절에서는 동적 분석의 부담을 컴파일 시간으로 옮기는 방법을 제시한다. 4절에서는 정적 분석에서 입력에 의존하는 부분을 식별하고, 입력에 무관한 부분은 컴파일 시간에 풀면서 입력에 의존하는 부분은 실행시간으로 연기하는 방법을 제시하고, 5절에서는 입력에 의존하는 부분들을 단축하는 방법을 제시한다. 우리가 제시한 분석을 적용한 예를 6절에서 보여주고, 7에서는 관련 연구들에 대해서 논한다. 8절에서 결론을 맺는다.

2. 소스 언어 L

우리가 대상으로 하는 언어는 core ML[3]과 같이 값에 의한 호출(call-by-value)을 하는 고차(higher-order)언어 이다. 고차 언어란, 함수를 다른 값들과 구분하지 않고 다른 함수의 인수나 결과값으로 사용하는 언어이다. 언어에서 사용하는 식은 변수, 함수 호출식, 자료 생성(data construction), 자료값에서 인수의 추출(deconstrution) 또는 경우에 따른 분기(case)이다(그림 2). 각각의 모든 식에 꼬리표(label)를 붙일 수 있다. 값은 함수이거나 자료(data)이다. 자료 값 [eqn: kappa(v`)`]는 식 □con[eqn: kappa][eqn: e`]□에 의해, 자료 생성자 [eqn: kappa]와 식 [eqn: e``]의 값 [eqn: v``]로부터 만들어진다. 인수 값 [eqn: v``]는 [eqn: e``]의 값이 [eqn: kappa(v`)`]일 때 □decon[eqn: kappa][eqn: e`]□로 부터 얻을 수 있다. □case[eqn: e_1][eqn: kappa][eqn: e_2][eqn: e_3]□는 [eqn: e_1]의 값에 때라 [eqn: e_2]나 [eqn: e_3]로 분기한다.

L의 의미(semantics, 그림 2)는 계산 문맥(evaluation context)[4, 5] 방법을 사용하여 정의하였다. 이 계산 문맥은 값에 의한 호출을 따르는 변형(reduction) 방법을 정의한다. 문맥 □의 구멍이 식 [eqn: e`]로 채워질 때, □[eqn: [e`]`]로 표기한다. 변형 규칙은 전통적인 변형 규칙을 따른다. unlabel 규칙이 꼬리표를 떼어 내는 것을 제외하면 모든 규칙들은 꼬리표를 유지한다. 치환 연산 [eqn: [v`/x]`e``]는 [eqn: e``]에 나타나는 모든 자유 변수(free variable) [eqn: x``]를 [eqn: v``]로 치환한다. 치환 연산은 [eqn: x``]의 꼬리표들을 유지한다. 예를 들어, [eqn: [v/`x]`x_l```=```v_l`] 이다.

3. 출발점 : 집합 기반 분석

이 절에서는 집합 기반 분석의 틀[6, 7, 8, 9] 위에서 출발점이 될 정적 분석을 정의하고, 다음절에서 이 정적 분석을 이용하여 프로그램의 입력에 의존하는 성질을 분석하는 분석을 이끌어 낼 것이다.

집합 기반 분석은 집합 관계식 모으기와 풀기의 두 단계로 이루어진다. 첫번째 단계는 프로그램 식들 사이의 자료 흐름을 기술하는 관계식들을 이끌어 내는 것이고, 두번째 단계는 그런 관계식들을 만족하는 값의 집합을 찾아가는 단계이다. 결과는 집합 변수로부터 그러한 값의 집합으로의 테이블이다. 값의 집합의 크기는 무한할 수 있지만, 그것을 유한하게 기술할 수 있는 방법인 정규 트리 문법(regular tree grammar)이 존재한다.

식[eqn: e_l``]과 프로그램의 변수[eqn: x``]는 집합 변수[eqn: X_l`]과[eqn: X_x`]을 갖는다. 각각은 식의 값과 변수에 결합된(bound) 값을 나타낸다. 집합 관계식은 [eqn: X][eqn: supseteq][eqn: se``]의 형태를 갖는다. [eqn: X``]는 집합 변수이고, [eqn: se``]는 집합식이다. 이 관계식은 집합 [eqn: X``]가 집합 [eqn: se``]를 포함한다는 의미를 가진다. 집합식 [eqn: se``]는 일곱 가지가 있다. 각각은 프로그램 식들과 대응된다(그림 3). 집합식의 의미는 대응되는 프로그램 식으로부터 자연스럽게 이끌어진다. 예를 들어, [eqn: kappa```X_1``]는 [eqn: v``]가 [eqn: X_1`]의 원소일 때 [eqn: kappa(v`)``]들의 집합을 의미한다. [eqn: app(X_1, X_2`)``]는 인수를 [eqn: X_2`]로하여 함수 [eqn: X_1`]를 호출한 호출식으로부터 반환된 값의 집합을 나타낸다. [eqn: case(X_1 , kappa , X_2 , X_3`)``]는 [eqn: X_1`]의 값에 [eqn: kappa(v`)``]가 있으면 [eqn: X_2`]의 값들을, [eqn: X_1`]의 값에 [eqn: kappa'(v`)``]가 있으면 [eqn: X_3`]의 값들을 나타낸다. 집합식의 의미는 집합식들로부터 값의 집합으로의 매핑인 해석 [eqn: I``]로 엄밀하게 정의된다(그림 3). 모든 [eqn: X``supseteq``se````in````C``]에 대해 [eqn: I(X`)``supseteq``I(se`)``]이면, 해석 [eqn: I``]를 관계식 집합 [eqn: C``]의 모델이라고 부른다.

정적 분석은 집합 관계식들의 최소 모델로 정의될 수 있다. 이 논문에서 제안한 집합 관계식은 모든 연산들이 단조적(monotonic)이고 각 관계식의 왼쪽이 변수로만 이루어지기 때문에 모든 관계식들을 만족하는 최소모델이 존재함을 보장한다[6].

3.1 초기 관계식들을 모으기

그림 3은 프로그램 □로부터 초기 관계식 [eqn: C``]를 모으기 위한 규칙들을 보여준다. 이 규칙들은 프로그램을 한번만 훑어봄으로써 초기 관계식을 모을 수 있다.

[eqn: wp``□``C`]

각 식으로부터 만들어지는 관계식들은 하위식들로부터 얻어진 관계식들과, 그 식 자체에 대한 관계식을 합친 것이다. 예를 들어, 함수 호출식 [eqn: e_1][eqn: e_2`]에 대해 만들어지는 관계식들은 두개의 하위식 [eqn: e_1], [eqn: e_2`]로부터 만들어진 두 관계식들 [eqn: C_1], [eqn: C_2`]와 [eqn: X_l][eqn: supseteq][eqn: app( X_1, X_2`)``]를 합친 것이다. [eqn: X_l][eqn: supseteq][eqn: app( X_1, X_2`)``]의 의미는 [eqn: X_l`]이 가질 수 있는 값은 [eqn: X_2`]([eqn: e_2`]에 대한 집합 변수)를 인수로 한 [eqn: X_1`]([eqn: e_1`]에 대한 집합 변수)이 가지는 함수의 결과값을 포함한다는 의미이다.

3.2 관계식들을 풀기

관계식을 푸는 단계는 초기 관계식 집합 [eqn: C``]를 그림 4의 규칙에 따라서 더 이상 풀 것이 없을 때까지 푸는 것이다. 직관적으로, 그림 4의 규칙들은 프로그램의 모든 가능한 자료 흐름 경로를 따라서 값을 전파시킨다. 각 전파 규칙들은 복합(compound) 집합식을 더 작은 형태로 분해시킨다. 이 과정은 식들 사이로 값이 흐르는 단계를 요약(approximate)한 것이다. 호출식에 대한 규칙을 생각해 보자. [eqn: X][eqn: supseteq][eqn: app( X_1,` X_2`)] :

[eqn: {X`` supseteq`` app( X_1,` X_2`) ~~~~ X_1`` supseteq`` lambda`x.e_3} over {X`` supseteq`` X_3 ~~~~ X_x`` supseteq`` X_2}]

이 규칙은 호출될 함수가 [eqn: lambda x.e_3`]일 경우 [eqn: X][eqn: supseteq][eqn: X_3`]를 생성한다. 그리고, 실인수 [eqn: X_2`]가 형식인수 [eqn: x`]에 결합되는 것을 흉내내기 위해 [eqn: X_x][eqn: supseteq][eqn: X_2`]를 추가한다. ([eqn: X_1``supseteq``lambda x.e_3`]와 같이 복합 집합식을 분해하는 방아쇠 역할을 하는 관계식을 □점화 관계식□이라고 부른다.) 다른 규칙들은 집합식에 대응하는 의미들로부터 쉽게 이끌어진다.

규칙 [eqn: R`]들을 사용하여 [eqn: c`]가 [eqn: A`]로 부터 유도될 수 있으면 [eqn: A``vdash_R`` c`]라고 쓰고, 규칙 [eqn: R`]에 대한 [eqn: A`]의 닫힌집합(closure) {[eqn: c```|```A`vdash_R`c``]}을 [eqn: R^* (A`)`]라고 쓴다.

이 닫힌집합은 다음과 같은 최소 고정점(least fixpoint)으로 정의될 수도 있다. lfp (□X.A□{c | X □R c }).

집합 관계식의 집합 [eqn: C`]에 대해, [eqn: Vars(C`)`]는 [eqn: C`]에 있는 집합 변수들의 집합을, [eqn: C(X`)`]는 {[eqn: X``supseteq``se][eqn: |][eqn: X``supseteq``se][eqn: in][eqn: C``]}를 나타낸다.

[eqn: S^* (C`)`]에 있는 관계식 집합 사이에서, 완전히 분해된 관계식 집합 [eqn: atom(S^* (C`)`)`]는 [eqn: C`]의 최소 모델을 이룬다. 그런 관계식들을 □핵(atomic)□이라 부른다. 핵 관계식(atomic constraint)은 관계식의 오른쪽 [eqn: ae`](atomic expression)가 다음의 값 집합일 때 [eqn: X``supseteq``ae`]의 형태이다.

[eqn: ae````::=````lambda`x.e``````|``````kappa`X``````|``````top`.]

핵 관계식의 집합 [eqn: G][eqn: =`]{[eqn: X_1``supseteq``ae_1`],[eqn: `...`],[eqn: X_n`` supseteq``ae_n`]}는 [eqn: G`]의 문법적 해석(정규 트리 문법, 집합 변수는 비단말(non-terminal)) [eqn: X_1``::=``ae_1,``...``,X_n``::=``ae_n`]에 의해 생성되는 문장(sentence)들의 집합을 의미한다.  □G□는 그런 문장들의 집합이다.

정리1. [eqn: wp`]에 자유 변수가 없고, 집합 관계식 [eqn: C`]가 [eqn: wp``□``C`]에 의해 도출되었다고 하면, [eqn: C`]의 최소 모델은 [eqn: \{`X``mapsto``□atom( S^* (C`)(X`))□``|``X``in``Vars(C`)`\}] 이다.

증명. [6, 7] □

정의1.([eqn: sba`]) 자유변수가 없는 프로그램 [eqn: wp`]에 대한 집합 관계식 [eqn: C`]가 [eqn: wp``□``C`]에 의해 도출되었다고 하면, [eqn: sba(wp`)(l`)``□``□atom(S^* (C`)(X_l`))`□]. 집합 기반 분석 [eqn: sba(wp`)`]는 프로그램 값들을 안전하게 예측한 것(safe approximation)이다.

정리2. ([eqn: sba`]의 안전성) 자유변수가 없는 프로그램 [eqn: wp`]의 관계식이 [eqn: wp``□``C`]라 하자. 만약 [eqn: wp``mapsto^*``□[v_l`]`]이라면 [eqn: v``in``sba(wp`)(l`)`].

증명. [6, 7]의 증명 방법을 따라서 증명가능. [7]의 집합 기반 동적 의미 구조를 정리 1을 증명하기 위한 중간 단계로 사용한다. □

3.3 입력(자유 변수)이 있을 경우의 분석

지금까지 우리는 분석될 프로그램이 입력(자유) 변수를 가지고 있지 않다고 가정했다. 이제부터는 모든 프로그램 [eqn: wp`]이 하나의 입력 변수 [eqn: alpha`]를 가진다고 가정하겠다.

3.3.1 정적 분석: 입력에 무관한 불변 성질의 예측

입력 변수 [eqn: alpha`]를 가지는 프로그램 [eqn: wp`]에 대한 초기 관계식들의 집합 [eqn: C`(wp``□``C`)]는 [eqn: X_alpha`]에 대해서는 아무런 관계식을 가지고 있지 않다. 따라서, [eqn: X_alpha`]를 사용하는 집합 관계식들은 풀려질 수 없다.

그러나, [eqn: C`]를 사용하여 입력에 무관한 성질(불변 성질)들을 추정하는 정적 분석을 얻는 것은 쉽다. 입력 변수 [eqn: alpha`]에 대한 또 다른 관계식 [eqn: X_alpha``supseteq``top`]로부터 푸는 과정 [eqn: S^* (□)`]를 시작한다. [eqn: top`]은 전체 값들의 집합 [eqn: Val`]을 나타낸다. 분석 과정은 다음과 같다.

let [eqn: wp``□``C`]             초기 관계식 (컴파일시간)

in  [eqn: S^* (C``cup``{X_alpha``supseteq``top`}`)]  관계식 풀기 (컴파일시간)

입력에 대해서는 아무런 정보도 없다(전체 집합)고 가정했기 때문에, 위의 분석은 입력에는 무관한 성질을 예측하게 된다.

정의2. ([eqn: sba_top`]) 프로그램 [eqn: wp`]가 입력 [eqn: alpha`]를 가지고, 그에 대한 초기 관계식이 [eqn: wp``□``C`]에 의해 도출되었다고 하자. [eqn: sba_top (wp`)(l`)``□``□atom( S^* (C``cup`\{ X_alpha``supseteq``top`\})(X_l`))□].

정리3. ([eqn: sba_top`]의 안전성) 모든 [eqn: nu``in``Val`]에 대해, [eqn: [nu/ alpha`]`wp``mapsto^*``□[v_l ]`]이면 [eqn: v`` in`` sba_top` ( wp`)(l`)`]이다.

증명. [eqn: ´nu`` in`` Val`], [eqn: sba([ nu/ alpha`] wp`)(l`)`` subseteq``sba_top (wp`)(l`)`]이기 때문에 정리 2에 의해 증명 가능. [eqn: sba`]와 [eqn: sba_top`]는 같은 규칙을 사용하고, 이 규칙은 단조(monotonic)적이다. [eqn: sba([ nu/ alpha`] wp`)`]는 [eqn: X_alpha`` supseteq`` nu`]를 가지는 반면, [eqn: sba_top`( wp`)`]는 더 큰 [eqn: X_{ alpha}`` supseteq`` top`]를 가지는 것을 제외하고는 두 개의 초기 관계식이 같기 때문에 증명 가능하다. □

3.3.2 동적 분석: 입력에 따라 변하는 성질들의 예측

입력에 의존하는 성질을 분석을 하기 위해서는, 푸는 단계을 실행시간으로 미루어야 한다. 실행시간에는 입력에 대한 관계식 [eqn: X_{ alpha}`` supseteq`` top`]에서 [eqn: top`]을 실제 입력값 [eqn: nu`]으로 대체할 수 있다:

let  [eqn: wp`` □`` C`]            초기 관계식 (컴파일 시간)

in  [eqn: ``S^* (C`` cup` X_alpha`` supseteq`` nu`)]   관계식 풀기 (실행 시간)

위의 과정은 입력값 [eqn: nu`]에 특화된 성질을 예측한다.

정의 3. ([eqn: sba_nu`]) 프로그램 [eqn: wp`]이 입력 [eqn: alpha`]를 가지고, 초기 관계식이 [eqn: wp`` □`` C`]에 의해 도출되었다고 하면, [eqn: sba_nu ( wp`)(l`)`` □`` □ atom( S^* (C`` cup` X_alpha`` supseteq`` nu`)( X_l`))□].

정리 4. ([eqn: sba_nu`]의 안전성) [eqn: [ nu/ alpha`]` wp`` mapsto^* ``□[v_l`]`] 이면 [eqn: v`` in`` sba_nu ( wp`)(l`)`]이다.

증명. [eqn: sba_nu ( wp`)`` = ``sba([ nu/ alpha`] wp`)`]이기 때문에, 정리 2에 의해 증명 가능.□

다음절에서는 이 동적 분석을 바탕으로 동적 관계식을 미루고, 이 부분을 단축시킨 분석을 유도한다. 유도된 분석은 프로그램의 입력이 나타나면 안전하면서도 빠르게 결과를 낼 것이다.

4. 파생 분석 I: 동적 관계식을 미루자

동적 분석 [eqn: S^* (C`` cup` X_alpha`` supseteq`` nu`)`]을 계산하는 과정 중 많은 부분이 컴파일 시간에 수행될 수 있다. 관계식  [eqn: X_{ alpha}`` supseteq`` nu`]이 프로그램의 실행시간이 되어야 제공된다고 해도, 컴파일 시간에 [eqn: C`]중에서 입력에 무관한 관계식들은 풀고 나머지를 실행시간으로 미룰 수 있다.

프로그램의 입력에 의존하는 관계식 [eqn: X`` supseteq ``se_□`]은 집합 식 [eqn: se_□`]가 입력에 의존한다(아래첨자 □)고 표시된 것을 제외하고는 보통의 관계식들과 같은 형태를 가진다. 입력에 의존하는 집합 식 [eqn: se_□`]는 컴파일 시간에는 분해될 수 없다. 입력 의존적 집합식은 다음의 네 가지가 있다.

[eqn: matrix {{ se_□}& {::=}& {X_{ alpha}~ |~ kappa_□^{-1} ~|~ app_□`( X_1`, X_2`) ~|}# {}& {}& {case_□`( X_1`, kappa`, X_2`, X_3`)~~~~~~~}}]

입력 변수에 대한 집합 변수 [eqn: X_{ alpha}`]는 입력에 의존적이다. 복합 집합식들은 점화 관계식이 입력에 의존적이면 입력에 의존적이다.

입력에 의존적이 동적 관계식들을 식별하는 것은 간단하다. 관계식에 푸는 규칙 S를 적용할 때, 우리는 집합 관계식 [eqn: X`` supseteq`` X_{ alpha}`]와 같이 입력 집합 변수를 오른쪽에 가지는 관계식들로부터 출발하여 입력에 대한 의존성도 함께 전파하게 된다. [eqn: S`]에 있는 푸는 규칙들은 점화 관계식이 주어지면, 복합 집합 관계식들을 더 작은 것으로 분해한다는 것에 주목하자. 따라서, 점화 관계식이 입력에 의존적이면 복합 집합 관계식도 입력 의존적이 된다. 예를 들어, 다음의 규칙을 생각해 보자.

[eqn: {X`` supseteq`` app( X_1`, X_2`) ~~~~ X_1`` supseteq`` lambda`x.e} over {X`` supseteq`` X_e ~~~~ X_x`` supseteq`` X_2}].

점화 관계식 [eqn: X_1`` supseteq`` lambda`x.e`] 는 [eqn: X`` supseteq`` app( X_1`, X_2`)`]가 분해되게 해 준다. 만약 이 점화 관계식이 입력에 의존적이라면 우리는 다음과 같이 [eqn: app( X_1, X_2`)`]도 입력에 의존적이라고 표시할 수 있다.

[eqn: {X`` supseteq`` app( X_1`, X_2`) ~~~~ X_1`` supseteq`` se_□} over {X`` supseteq`` app_□ ( X_1`, X_2`)}].

다른 경우들도 비슷하게 정의된다.

그림 5는 입력에 의존하는 관계식들을 식별하는 규칙을 나타낸다. 각각의 규칙은 [eqn: S`]에서 대응되는 규칙들과 나란히 놓여져 있다. 마지막 규칙은 입력에 대한 의존성을 전달하는 규칙이다.

모든 과정은 다음과 같이 정의된다:

let [eqn: wp`` □`` C`]             초기 관계식 (컴파일시간)

[eqn: C'`` =`` (S`` cup` D)^* (C`)`] 부분적으로 풀기([eqn: S`]),

연기하기([eqn: D`]) (컴파일시간)

in  [eqn: S_□^* (| C'`|`` cup` X_alpha`` supseteq`` nu`)`] 연기된 관계식 풀기

(실행시간)

먼저, 프로그램 [eqn: wp`]로부터 초기 관계식 집합 [eqn: C`]를 모은다(그림 3의 [eqn: wp`` □`` C`]). 그리고 나서, 입력에 무관한 관계식들을 풀기 위해 규칙 [eqn: S`]를 [eqn: C`]에 적용하고, 동시에 규칙 [eqn: D`]를 적용하여 입력에 의존하는 관계식들을 식별하여 미룬다. 이 두 과정은 컴파일 시간에 수행될 수 있다. 결과로 만들어진 관계식 집합 [eqn: C'`]은 실행시간에 입력값 [eqn: nu`]과 함꼐 풀어지게 된다. 실행시간에 우리는 규칙 [eqn: S_□`]를 적용한다. 규칙 [eqn: S_□`]는 [eqn: □`]로 표시된 입력 의존적 집합식들을 다룬다는 것 외에는 규칙 [eqn: S`]와 같다. 관계식 집합 [eqn: | C'`|`]는 [eqn: C'`]에 있는 관계식들 중 완전히 풀려진 것 또는 연기된 관계식들을 모은 집합이다.

[eqn: MATRIX { {| C'`| }& {= }& {\{ X`` supseteq`` ae`` |`` X`` supseteq`` ae`` in`` C'`\} }# { }& {cup }& {\{ X`` supseteq`` se_□`` |`` X`` supseteq`` se_□`` in`` C'` \} } }]

정의 4. (연기된 분석 [eqn: dsba`]) 프로그램 [eqn: wp`]가 입력 [eqn: alpha`]를 가지고, 초기관계식이 [eqn: wp`` □`` C`]에 의해 도출되었으며, [eqn: nu`]은 실행시간에 주어진 입력이라고 하자. [eqn: C'`` =`` (S ``cup`` D`)^* (C`)`]이고,  [eqn: C''`` =`` S_□^* (| C'`|`` cup` X_alpha`` supseteq`` nu`)`]일때, 연기된 분석  [eqn: dsba_ nu ( wp`)(l`)`` □`` □atom( C''( X_l`)`)□]이다.

정리 5. ([eqn: dsba`]의 안전성) [eqn: [ nu/ alpha]` wp`` mapsto^* ``□[v_l`]`]이면 [eqn: v`` in`` dsba_nu ( wp`)(l`)`]이다.

증명. [eqn: dsba_nu ( wp`)`` =`` sba_nu ( wp`)`]이므로 증명 가능. 두 과정의 다른 점은 [eqn: dsba_nu ( wp`)`]는 입력에 의존하는 관계식들을 미루어 실행시간에 푼다는 것 뿐이다. 여기서, 실행시간에 푸는 규칙은 [eqn: sba_nu ( wp`)`]에서 사용하는 규칙과 정확하게 일치하며, 연기된 관계식들의 의미도 앞에서와 같다. 따라서, 연기된 집합 기반 분석의 결과도 [eqn: sba_nu ( wp`)`]의 결과와 일치한다. □

연기된 관계식 [eqn: | C'`|`]를 풀기위한 실행시간 과정 [eqn: S_□^* (| C'`|`` cup` X_alpha`` supseteq`` nu`)`]에도 약간의 실행시간 지연이 남아 있다. 연기된 관계식의 점화 관계식은 그 점화 관계식의 점화 관계식이 풀어져야 풀려질 수 있고, 점화 관계식의 점화 관계식은 점화 관계식의 점화 관계식의 점화 관계식이 풀어져야 풀려질 수 있다. 이렇게 [eqn: X_alpha`` supseteq`` nu`]으로부터 점화 관계식이 풀려질 때까지 값이 전파된 후에야 풀고자 하는 관계식을 풀 수 있는 것이다.

다음절에서는 이런 지연을 피하기 위한 관계식 변환에 대해 설명한다.

5. 파생 분석 II: 값을 자르는 분석을 통해 동적 관계식을 준비하자

만약 점화 관계식이 [eqn: se_□`]의 하위구조에 관한 것이 아니라 프로그램의 입력에 관한 것이라면, 연기된 관계식  [eqn: X`` supseteq`` se_□`]을 푸는 시간은 단축될 수 있을 것이다. 예를 들어, 다음의 [eqn: X`` supseteq`` case_□ ( X_1, kappa, X_2, X_3`)]를 푸는 규칙을 생각해 보자.

[eqn: {X`` supseteq`` case_□ ( X_1`, kappa`, X_2`, X_3`) ~~~~ X_1`` supseteq`` kappa` Y} over {X`` supseteq`` X_2}]

점화식 [eqn: X_1`` supseteq`` kappa` Y`]는 프로그램내의 식 [eqn: X_1`]에 대한 것이기 때문에, [eqn: X_1`]이 [eqn: kappa ` Y`]로 풀려질 때까지 기다려야 한다.

변환 규칙의 점화 관계식을 다음과 같이 입력에 대한 조건으로 바꾸면 이런 지연이 없어진다. □만약, 프로그램의 입력이 [eqn: V`]에 포함되면 case식 [eqn: X`]는 [eqn: X_2`]의 값을 가진다.□ [eqn: V`]에 관한 조건은 다음과 같다. [eqn: V`]에 속한 모든 프로그램의 입력에 대해 [eqn: e_1`]은 [eqn: kappa`]로 시작되는 값으로 계산되어진다.

□값을 자르는 분석□은 그러한 집합 [eqn: V`]를 예측한다. 값을 자르는 분석이란 다음의 질문에 대한 답을 얻기 위한 정적분석이다: 프로그램내의 한 식의 값이 집합 [eqn: V`]에 포함되기 위한 프로그램의 입력의 조건은 무엇인가?

5.1 값을 자르는 분석

일반적으로, 자르는 분석(slicing) [10]이라 하면 기준이 되는 식에 관련된 프로그램의 부분(프로그램의 식 또는 변수)들을 고르는 방법이다.

값을 자르는 분석은 프로그램의 일부분을 자르는 것이 아니라, 프로그램내의 식이 가질 수 있는 값을 자르는 분석이다. 자르는 기준인 [eqn: e`` subseteq`` V`]는 식 [eqn: e`]의 값이 [eqn: V`]에 속하기 위한 조건이다. 자른 결과인

[eqn: SVS_wp (e`` subseteq`` V`)`]

는 프로그램 [eqn: wp`]의 식들로부터 그 값의 집합으로의 매핑이다. 각 값의 집합들은 프로그램이 [eqn: e`]의 값을 [eqn: V`]에 속하게끔 만들어주기 위해 필요한 값들이다. 더 엄밀하게 말하면, 자른 결과 [eqn: SVS_wp (e``subseteq``V`)( alpha`)`]에 속한 모든 입력에 대해서 프로그램이 [eqn: e`]의 값을 계산해 낸다면, 그 값은 [eqn: V`]에 속해야 한다.

예 1 다음의 프로그램 [eqn: wp`]을 생각해보자.

datatype t = A | B | C

case x of

A => B

| _ => x

입력 x가 A또는 B일 때, 프로그램은 B를, 입력이 C일때는 C를 결과로 낸다. 자르는 기준이 [eqn: wp`` subseteq`]B일 때, 값을 자르는 분석 [eqn: SVS_wp (wp``subseteq``]{B}[eqn: )(]x[eqn: )]는 A, B의 부분집합이 되어야 한다. 만약, 기준이 [eqn: wp`` subseteq`]{C}라면,  [eqn: SVS_wp (wp`` subseteq] {C})(x) [eqn: subseteq] {C}가 되어야 한다.□

이 논문에서 우리는 값을 자르는 분석을 집합 관계식의 틀 위에서 정의하려고 한다. 집합 관계식은 다음의 형태를 가진다.

[eqn: se_l`` subseteq`` se_r]

이것의 의미는 집합 [eqn: se_l`]는 집합 [eqn: se_r`]에 포함되어야 한다는 것이다.

그림 7은 관계식의 정의이다. 관계식 시스템은 초기 관계식을 이끌어 내기 위한 세 개의 규칙들과 슬라이싱 전달 규칙 [eqn: B`]로 이루어진다. 이 세 개의 규칙들은 한꺼번에 적용하는 것이 아니라 따로 따로 적용하게 된다.

□backward□의 의미에서 B로 이름지었다.

규칙 [eqn: B`]는 관계식의 의미에서부터 직관적으로 만들어진다. 초기 관계식을 이끌어내기 위한 규칙 ( [eqn: □_i`])도 역시 직관적이다:

□[eqn: (]con [eqn: kappa] [eqn: e_1` )_l`]이 1[eqn: X_l`]로 잘려진다면, 하위식 [eqn: e_1`]을 다음과 같이 잘라야 한다: [eqn: kappa` X_1`` subseteq`` X_l`]. decon의 경우에도 마찬가지이다.

□ 호출식 [eqn: (e_1``e_2`)_l`]이 [eqn: X_l`]로 잘려진다면, [eqn: e_1`], [eqn: e_2`]와 호출된 함수에 대한 세 개의 집합을 잘라야 한다: 함수 식 [eqn: e_1`]에 대한 집합은 [eqn: e_1`]에서 호출 가능한 함수들의 집합인 [eqn: Lam_wp (e_1`)`]로 잘라져야 한다. [eqn: lambda`x.e_3`` in`` Lam_wp (e_1`)`]에 속한 모든 함수들에 대해, 인수 식 [eqn: e_2`]는 [eqn: x`]의 값으로 잘려져야 하고, 호출된 함수는 호출식 [eqn: X_l`]로 잘라져야 한다.

[eqn: Lam_wp`]은 모든 입력에 대해서 각각의 식 [eqn: e`]에서 호출되어질 수 있는 함수들을 안전하게 모은 테이블이다. 그림 6의 규칙 [eqn: L`]에 의해 테이블이 결정된다:

[eqn: Lam_wp (e`)`` =`` \{ lambda`x.e'``|`` e`` rightarrow`` lambda`x.e'`` in`` L_wp^* (wp`)].

[eqn: e`` rightarrow`` lambda` x.e'`]는 [eqn: e`]가 함수 [eqn: lambda` x.e'`]으로 계산되어질 수 있음을 의미한다. [eqn: Lam_wp`]테이블의 안전성은 쉽게 증명될 수 있다.

□[eqn: (]case [eqn: e_1] [eqn: kappa] [eqn: e_2] [eqn: e_3][eqn: )_l`]이 [eqn: X_l`]로 잘려진다면, 자르는 방법은 세 가지가 있을 수 있다. 이 규칙들은 [eqn: e_2`]만 수행될 경우, [eqn: e_3`]만 수행될 경우, [eqn: e_2`], [eqn: e_3`]가 모두 수행될 경우의 세 가지 가능한 수행 흐름에 따라 달라진다. 각각의 상황에 따라서 자르는 규칙을 서로 다르게 정의할 필요가 있다. 첫 번째 상황에 대해서는, [eqn: e_1`]이 [eqn: kappa`` top`]( [eqn: top`]은 전체 집합을 의미)으로, [eqn: e_2`]는 [eqn: X_l`](case식)으로 잘라야 한다. 첫 번째 상황에 대해서는, [eqn: e_1`]이 [eqn: overline{ kappa}` top`]([eqn: kappa`]로 시작하지 않는 값)으로, [eqn: e_3`]는 [eqn: X_l`](case식)으로 잘라야 한다. 세 번째 상황에 대해서는, [eqn: e_1`]에 대해서는 아무 것도 자르지 않아야 하고, [eqn: e_2`], [eqn: e_3`] 모두 [eqn: X_l`]로 잘라야 한다.

값을 자르는 분석 [eqn: SVS_wp (e`` subseteq`` V`)`]의 과정을 다음과 같이 정의한다:

프로그램에 n개의 case식이 있으면, 3n개의 초기 관계식을 만들어 내야하지만, 비용과 정확성의 균형을 위해서 3개의 초기 관계식만을 만들어 낸다.

let  [eqn: wp`` □_i`` C_i`, {rm for} i=1,2,3]   세 개의 초기관계식

in  [eqn: bigvee_{i=1}^3` B^* (C_i`` cup` \{ X_e`` subseteq`` V `\}`)` MATRIX { {```` 세개의 자른 결과들의}# {논리합 ````````````````````````````````````````````} }]

규칙 [eqn: B`]에 닫힌 핵 관계식 [eqn: B`]는 [eqn: C_i`` cup` \{ X_e`` subseteq`` V` \}`]의 최대 모델 ([eqn: gm`])이다. 우리가 제안한 관계식 시스템은 코데피니트(co-definite) 관계식이기 때문에, 최대 모델이 항상 존재한다[11].

정리 6. 프로그램 [eqn: wp`]가 입력변수 [eqn: alpha`]를 가지고, [eqn: e`]는 [eqn: wp`]의 하위식이며, [eqn: V`]는 값의 집합이고, [eqn: wp`` □_i`` C_i`]에 의해 초기 관계식들이 만들어진다고 하면,  [eqn: □atom( B^* (C_i`` cup` \{ X_e`` subseteq`` V` \}))□`]는 [eqn: C_i`` cup` \{ X_e`` subseteq`` V` \}]의 최대 모델(greates model)이다.

증명. [eqn: C'`` =`` C_i`` cup` \{ X_e`` subseteq`` V` \}`]라 하자. 먼저 [eqn: gm(C'`)`` =`` gm(B^* ( C'`))`] 임을 [eqn: B`]가 [eqn: gm(C'`)`]을 유지하는 관계식들만 추가한다는 것을 이용해서 보일 수 있다. 그 후 [eqn: gm(B^* (C'`))`` =`` gm(atom(B^* (C'`)))`] 임을 보인다. A.1 절에서 자세하게 증명하였다.□

핵 관계식은 관계식 집합식 [eqn: ae`]가 핵 집합식인 [eqn: X`` subseteq`` ae`]다.

값을 자르는 분석은 세개의 관계식들에 대한 최대 모델들의 집합이다:

정의 5. (값을 자르는 분석 [eqn: SVS_wp (e`` subseteq`` V`)`]) 프로그램 [eqn: wp`]가 입력 변수 [eqn: alpha`], 하위 식 [eqn: e`]를 가지고, [eqn: i``=``1`,2`,3`]에 대해 [eqn: wp`` □_i`` C_i`]를 통해서 초기 관계식 [eqn: C_i`]를 이끌어 냈다고 하면, 값을 자르는 분석은 다음과 같이 정의된다.

[eqn: SVS_wp (e`` subseteq`` V)] □

[eqn: \{ □atom( B^* (C_i`` cup` \{ X_e`` subseteq`` V` \}))□`` |`` I`=`1,2,3 \}].

다음절에서, 우리는 [eqn: SVS_wp (e`` subseteq`` V)(alpha`)`]를 [eqn: \{v`` |`` v`` in`` Sigma( alpha`),``` Sigma`` in`` SVS_wp (e`` subseteq`` V`) \}`]의 의미로 사용한다.

이렇게 정의된 값을 자르는 분석은 우리가 예상한 다음의 성질을 만족한다:

정리 7. ([eqn: SVS_wp (e`` subseteq`` V`)`]의 정확성) 프로그램 [eqn: wp`]의 입력 변수가 [eqn: alpha`], 하위식 [eqn: e`` in`` wp`]라 하자. [eqn: Sigma`` in`` SVS_wp (e`` subseteq`` V`)`]이면 [eqn: □`nu`` in`` Sigma( alpha`)([ nu/ alpha`] wp`` mapsto^*`` □[v_e`]`` Rightarrow`` v`` in`` V`)`]이다.

증명. 집합 기반 동적 의미구조 [6, 7] [eqn: Sigma`` vdash`` e``□ `` v`] 를 중간 단계로 사용하여 증명한다. 먼저, [eqn: Sigma`` vdash`` e`` □`` v`` Rightarrow`` v`` in`` Sigma(e`)`]이고, [eqn: Sigma`]가 [eqn: [ nu/ alpha`] wp`]에 대해 안전한 집합 환경이며,  [eqn: Sigma(e`)`` supseteq`` V`]임을 증명한다. 그 후, [eqn: [ nu/ alpha`]` wp`` mapsto^*`` □[v_e`]`]가  [eqn: Sigma`` vdash`` e`` □`` v`]를 의미하고, 따라서 [eqn: v`` in`` Sigma(e`)`]를 의미하게 되고, 결국 [eqn: v`` in`` V`]를 의미하게 됨을 보인다. A.1 절에서 자세한 증명을 하였다. □

5.2 동적 관계식의 단축

값을 자르는 분석을 이용하여, 입력에 의존적인 관계식을 간단한 원소 테스트를 통해서 풀 수 있다. 즉, 프로그램의 수행 중 입력이 주어지면, 그 입력이 어떤 집합의 원소인지 아닌 지의 테스트만 통해서 동적 관계식들이 즉각적으로 동시에 풀려질 수 있다.

경우식에 대한 동적 관계식  [eqn: X`` supseteq`` case_□`( X_1`, kappa`, X_2`, X_3`)`]을 생각해 보자. 점화 관계식은 [eqn: X_1`` supseteq`` kappa` Y`]이거나 [eqn: X_1`` supseteq`` kappa'` Y`( kappa'`` not=`` kappa`)`]이다. [eqn: V_1`]에 속한 입력은 [eqn: X_1`]을 [eqn: kappa`]로 시작하는 값으로 만들어 주고, [eqn: V_2`]에 속한 입력은 [eqn: X_1`]을 [eqn: kappa'`]으로 시작하는 값으로 만들어 준다고 가정하자. 이런 집합 [eqn: V_1`], [eqn: V_2`]는 값을 자르는 분석의 결과가 될 수 있다:

[eqn: V_1 = SVS_wp`(X_1`` supseteq`` kappa` top`)( alpha`)````````]

[eqn: V_2 = SVS_wp`(X_1`` supseteq`` overline{ kappa}` top`)( alpha`)`.]

이 두 집합을 이용하여, 동적 분석 [eqn: X`` supseteq case_□`( X_1`, kappa`, X_2`, X_3`)`]은 다음과 같은 세 가지의 관계식으로 수정되어 진다.

[eqn: X`` supseteq`` if_□` (V_1`, X_2`)`,]

[eqn: X`` supseteq`` if_□` (V_2`, X_3`)`,]

[eqn: X`` supseteq`` if_□` ( overline{V_1`` cup` V_2}`, X_2`` cup` X_3`)]

집합식 [eqn: if_□` (V`, X`)`]는 프로그램의 입력이 [eqn: V`]의 원소일 때만, 집합 [eqn: X`]가 된다. 마지막에 있는 [eqn: if_□`]관계식은 입력이 [eqn: V_1`], [eqn: V_2`]에 모두 속하지 않는 경우에 사용된다.

[eqn: X`` supseteq`` if_□` (V`, X`)`]에 대한 점화관계식은 프로그램의 입력 [eqn: nu`]에 대한 간단한 멤버쉽 테스트 [eqn: nu`` in`` V`]이다:

[eqn: {X`` supseteq`` if_□ (V`, X_1`) ~~~~ nu`` in`` V} over {X`` supseteq`` X_1}]

정규 트리 문법 [eqn: V`]에 대한 테스트 [eqn: nu`` in`` V`]는 다항식(polynomial) 시간이 걸린다[12]: [eqn: nu`]의 크기[eqn: times][eqn: V`]에 있는 비단말(non-terminal)[eqn: times]함수(자료 생성자)의 인자 수(arity)의 합.

case식에 대한 입력에 의존적인 관계식을 정의하는 규칙은 다음과 같이 바뀐다.

[eqn: {X`` supseteq`` case(X_1` ,kappa`,X_2` ,X_3` ) ~~~~ X_1`` supseteq`` se_□} over {X`` supseteq`` case_□ (X_1` ,kappa` ,X_2` ,X_3` )}]

[eqn: Rightarrow]

[eqn: {matrix {{X`` supseteq`` case(X_1` ,kappa`, X_2` ,X_3` ) ~~~~ X_1 supseteq se_□}# {V_1`` = `` SVS_wp (X_1`` subseteq`` kappa` top`)(alpha)}# {V_2`` = `` SVS_wp (X_1`` subseteq`` overline{kappa}` top`)(alpha)}}} over {matrix {{X`` supseteq`` if_□ (V_1` , X_2`) ~~~~ X`` supseteq `` if_□ (V_2` ,X_3`)}# {X`` supseteq`` if_□ (overline{V_1`` cup` V_2} ,X_2`` cup` X_3` )}}}]

그림 8은 입력에 의존하는 관계식을 규명하고, 준비하고, 연기하는 규칙 [eqn: P`]와, 준비된 규칙을 실행시간에 푸는 규칙 [eqn: S_P`]이다.

분석을 준비하는 과정은 다음과 같이 정의된다.

let [eqn: wp`` □`` C`]             관계식의 도출(컴파일시간)

[eqn: C'`` =`` (S`` cup` P`)^* (C`)`] 동적 관계식을 준비하기

(컴파일시간)

in [eqn: S_P^* (| C'`|`` cup` \{ X_{ alpha}`` supseteq ``nu`)`] 준비된 관계식을 풀기

(실행시간)

먼저, 프로그램의 초기 관계식 [eqn: C`]를 그림 3의 [eqn: □`]규칙을 이용해서 모은 후, [eqn: S`]규칙을 [eqn: C`]에 적용하여 입력에 무관한 관계식을 풀고, 동시에 규칙 [eqn: P`]를 적용하여 입력에 의존하는 관계식을 규명하고, 준비한다. 결과로 나온 관계식의 집합 [eqn: C'`]은 실행시간에 프로그램의 입력 [eqn: nu`]에 의해 풀어지게 된다. 앞에서와 같이, [eqn: | C'`|`]는 [eqn: C'`]의 관계식들 중 핵 관계식으로 풀려진 것 또는 동적 관계식으로 준비된 관계식들의 집합이다.

정의 6. (준비된 분석 [eqn: psba`]) 프로그램 [eqn: wp`]의 입력 변수가 [eqn: alpha`], 도출된 초기 관계식이 [eqn: wp`` □`` C`], 입력 값이 [eqn: nu`]라 하자. 준비된 분석은 [eqn: C'`` =`` (S`` cup` P`)^* (C`)]이고, [eqn: C''`` =`` S_P^* (|C'`|`` cup` \{ X_alpha`` supseteq`` nu`\})`]일 때, [eqn: psba_nu ( wp`)(l`)]□[eqn: □atom( C''( X_l `))□]로 정의된다.

준비된 분석은 입력에 의존하는 성질을 안전하게 예측한다:

정리 8. ([eqn: psba`]의 안전성) [eqn: [ nu/ alpha`]` wp`` mapsto^*`` □[v_l`]`]이면  [eqn: v`` in`` psba_nu ( wp`)(l`)]이다.

증명. [eqn: psba`]가 [eqn: sba_nu`]의 안전한 예측이라는 것을 보임으로써 [eqn: psba`]의 안전성을 증명한다. [eqn: sba_nu ( wp`)`]와 [eqn: psba_nu ( wp`)`]의 닫힌 집합(closure)에 해당하는 두 개의 연속(continuous) 함수 [eqn: F_nu`]와 [eqn: P_nu`]를 정의한다[13]. 그 후, [eqn: P_nu`]의 최소 고정점(least fixpoint)이 [eqn: F_nu`]의 최소 고정점보다 크거나 같다는 것을 보인다. A.2 절에 자세한 증명을 하였다. □

6. 예

[14]에서 사용되었던 그림 9의 패킷 필터 프로그램을 생각해 보자. 이 프로그램은 다음과 같은 자료구조를 가지는 패킷을 입력으로 받아, 패킷의 ip 소스가 FOO이면 true를 반환한다.

예로 든 프로그램은 값의 쌍(pair)와 쌍에서의 첫번째(#1), 두번째(#2) 값을 고르는 식을 가지고 있다. 이 논문에서는 위의 두 식에 대해서는 분석 규칙을 생략하였다. 전체 시스템이 코데피니트(co-definite)한 것을 깨지 않고, 슬라이싱 전달 규칙을 추가할 수 있다.

[eqn: packet``` ::=`` langle ethertype`, langle` ip`, arp` rangle rangle]

[eqn: `ip`` ::=`` langle ipsrc`, ipdst` rangle]

[eqn: arp`` ::=`` langle arpsrc`, arpdst` rangle]

(*)로 마크된 casea식에 대한 분석을 생각해 보자. [eqn: wp`` □`` C`]로부터 만든 casea의 초기 관계식은 다음과 같다.

[eqn: X_{{rm case}_a}`` supseteq`` case( X_{rm ipsrc}`, {rm FOO}`, X_{rm TRUE}`, X_e`)]

변수 ipsrc가 입력 [eqn: alpha`]의 하위구조에 결합(bind)되므로, [eqn: X_{rm ipsrc}`]는 입력에 의존한다.

값을 자르는 분석을 이용하여, 점화 관계식 [eqn: X_{rm ipsrc}`` supseteq`` {rm FOO}` Y`]와 [eqn: X_{rm ipsrc}`` supseteq`` kappa` Y`( kappa`` neq`` {rm FOO}`)`]를 단축시켜, 프로그램의 입력에 대한 멤버쉽(membership) 테스트가 되도록 만들 수 있다.

[eqn: SVS_wp (X_{rm ipsrc}`` subseteq`` {rm FOO}` top)]

[eqn: SVS_wp (X_{rm ipsrc}`` subseteq`` overline{rm FOO}` top)]

그림 10은 [eqn: SVS_wp (X_{rm ipsrc}`` subseteq`` {rm FOO}` top)( alpha`)]를 푸는 과정을 보여준다. 입력 [eqn: X_{ alpha}`]에 대한 결과는

[eqn: X_{ alpha}`` subseteq`` langle {rm IP}, langle langle {rm FOO}, {rm FOO} rangle, top rangle rangle] 또는

[eqn: X_{ alpha}`` subseteq`` langle topr, langle langle {rm FOO}, top rangle, top rangle rangle]

이다. 따라서, 점화 관계식 [eqn: X_{rm ipsrc}`` supseteq`` {rm FOO}` Y`]를 멤버쉽 테스트 [eqn: alpha`` in`` langle top, langle langle {rm FOO}, top rangle, top rangle rangle`]로 대체할 수 있다. 즉, 실행 중에, 입력이 위의 테스트를 통과하면 준비된 관계식

[eqn: X_{{rm case}_a}`` supseteq`` if_□` ( langle top, langle langle {rm FOO}, top rangle, top rangle rangle, X_{rm TRUE})],

는

[eqn: X_{{rm case}_a}`` supseteq`` X_{rm TRUE}]

로 풀려진다.

7. 관련 연구

자료 흐름 분석을 전문화하는 다른 연구들은 우리 연구에 비해 다음의 세 가지 한계를 가진다: 프로그램의 흐름을 미리 알고 있어야 한다. 실행시간에 빠르게 풀기 위한 컴파일 시간 준비(값을 자르는 분석을 통한)가 없다. 전문화 과정의 정확성이 수학적으로 정의되고 증명되지 않았다. Sharma등의 방법[15]은 여러 가지의 자료 흐름들을 모으게끔 만드는 지점을 찾아내어, 그 점에 대한 분석을 실행시간으로 미룬다. 실행 시간에 연기된 점으로 여러 개의 자료 흐름 엣지들 중 하나가 선택되고, 정적 자료 흐름 분석에 비해 정확한 결과를 내게된다. 이 방법은 프로그램의 함수 흐름 그래프(control flow graph)를 미리 알고 있다고 가정하기 대문에 함수가 다른 값과 같이 사용될 수 있는 고차(higher-order) 언어에서는 사용할 수 없다. 또, 실행 시간 전문화를 위해서 실행중인 프로그램의 흐름이 연기된 점까지 도달하기를 기다려야 한다. 이런 지연을 줄이기 위해서 컴파일 시간에 어떤 준비도 하지 않는다. Moon등의 포트란 프로그램에 대한 동적 의존 분석(dynamic dependence analysis)[16]도 같은 한계를 가진다.

Ammons와 Larus는 자료 흐름 분석의 정확성을 향상시키기 위해서 계측된 자료(profiled data)를 사용한다[17]. 프로그램의 함수 흐름 그래프에서 자주 수행되는 경로를 분리하여 자료 흐름 분석을 함으로써 정확성을 향상시켰다. 이 방법은 계측 자료를 모아서 자주 수행되는 경로를 찾아내고, 그 경로에 대한 자료 흐름 분석을 분리시키고, 전체 프로그램에 대해 안전한 분석을 재구성하기 위한 부담이 있다. 이러한 과정은 코드 제공자/소비자 모델에서 볼 때, 코드 제공자측에서 하는 것이 아니라, 사용자측에서 하게 되므로 큰 부담이 될 수 있다. 우리 방법은 실행과정을 관찰하여 자료를 계측하지 않기 때문에 이런 부담이 없다.

실행시간 코드 생성 기법[18, 19, 20, 21]은 입력에 의해 만들어지는 동적 성질을 찾아내는 것이 아니라, 실행시간에 목적 코드를 최적화 하는데 초점을 두고 있다. 이 방법은 실행시간에 특정 입력에 대한 프로그램의 동적 성질을 분석하지 않는다. 모든 분석은 컴파일시간에 이루어진다. 기본적으로 프로그램의 어떤 부분이 전문화될 것인지에 대한 프로그래머의 주석(annotation)을 바탕으로 한 결합 시간 분석(binding-time analysis)이다. 실행시간에 여러 개의 입력중 일부분을 알게 되면, 부분 계산(partial evaluation)[22]에 바탕을 둔 코드 전문화 과정에 의해 부분 입력에 최적화 된 코드를 생성하게 된다.

Flanagan과 Felleisen의 부품별(componential) 집합 기반 분석[5]은 우리 방법과 전혀 다른 관점에서 적용될 수 있다. 이 방법은 우리 분석을 분리해서, 부품별로 준비하여 모듈별 실행시간 전문화 기법을 만드는 데 적용될 수 있을 것이다. 이 방법에서 사용된 관계식의 단순화 알고리즘은 관계식을 푸는 과정에서 새로운 관계식이 무한하게 생성되는 경우 이를 제한하는 방법이다. 본 논문에서 사용된 분석은 생성되는 관계식의 수가 프로그램의 크기에 의해 제한되기 때문에 이 과정이 필요 없다. 만약 시작점으로 사용된 정적 분석이 위의 클래스에 들어간다면 부품별 집합 기반 분석에서 제시된 단순화 과정을 적용할 수 있을 것이다.

값을 자르는 분석은 자르는 기준에 해당하는 사용자의 주석(annotation)을 사용하는 하위타입 또는 정제된 타입 유추[23, 24, 25]로 볼 수 있다. 다른 점은 하위 타입이나 정제된 타입 시스템에서 사용하는 타입 계층(hierarchy)이 우리가 사용하는 정규 트리 문법의 도메인보다 더 작다는 것이다. Reps와 Turnidge의 문맥 분석(context analysis)[26]과 Liu의 의존성 분석[27]은 고정된 아주 작은 래티스를 사용한다. Bourdoncle의 Syntox 시스템[28]은 값을 자르는 분석의 한 종류이다. Syntox에서 사용된 값을 자르는 분석이 파스칼 프로그램의 디버깅에 사용할 수 있음을 보였다. 그러나, 우리 방법은 임의의 자료형을 지원하는 반면, Syntox의 값은 정수의 범위(range)로 제한되어 있다. Biswas가 제안한 필요할 때 푸는(demand-driven) 집합 기반 분석[29]은 전체 프로그램의 값을 계산하는데 영향을 준 하위 식들을 찾는 방법이다. 이 방법은 프로그램의 식을 자를 뿐, 식의 값을 자르지는 않는다.

8. 결론

본 논문에서 우리는 정적 분석을 사용하여 프로그램의 입력에 의존하는 성질을 예측하는 방법을 제안하였다. 우리가 제안한 방법은 입력에 무관한 성질을 예측하도록 설계된 정적 분석을 입력에 의존하는 성질을 예측하는 분석으로 변환할 수 있다. 이 방법은 실행 중에 프로그램의 성질을 알아내기 위해서 실행중인 프로그램을 관찰하는 코드나 계측 과정을 필요로 하지 않는다.

정적 분석의 가장 마지막 부분을 프로그램의 실행 시간으로 미루는 것이 이 논문의 핵심 아이디어다. 먼저 정적 분석을 분석하여, 프로그램의 입력에 민감하여 프로그램의 실행시간으로 연기되어야 하는 분석의 부분을 찾아낸다. 그 후, 값을 자르는 분석을 이용하여 이 부분을 재구성하여 프로그램의 입력에 대한 간단한 멤버쉽 테스트에 의해 분석이 풀어질 수 있도록 한다. 이런 재구성과정을 통해 준비된 분석들은 프로그램의 입력이 나타나기만 하면 순간적으로, 동시에 풀려질 수 있다.

이 방법의 장점은 1) 집합 기반 분석이 주어지면 그에 해당하는 어떤 입력에 기반한 성질도 분석할 수 있다. 따라서, 단순히 실행 횟수만을 계측하는 전통적인 계측 방법에 비해 더 일반적인 분석 방법이다. 2) 수행중인 프로그램에 대해 실행시간 부담(overhead)이 없다. 3) 함수 값이 다른 값과 구별 없이 사용되는 고차 언어(higher-order language)에 적용할 수 있다. 4) 엄밀히 정의되었고, 정확하게 증명되었다.

참고 문헌

[1]	Thomas Ball and James R. Larus. Optimally profiling and tracing program. ACM Transactions on Programming Languages and Systems, 16(4):1319-1360, July 1994.

[2]	Thomas Ball, Peter Mataga, and  Mooly Sagiv. Edge profiling versus path profiling: the showdown. In Proceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, January 1998.

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

[4]	Martin S. Feather. A survery and classification of some program transformation approaches and techniques. In L.G.L.T. Meertens, editor, Program Specification and Transformation, pages 165-195. Elsevier Science Publishers, 1987.

[5]	Cormac Flanagan and Matthias Felleisen. Componential set-based analysis. In Proceedings of the SIGPLAN conference on Programming Language Design and Implementation, 1997.

[6]	Nevin Heintze. Set Based Program Analysis. PhD thesis, Carnegie Mellon University, October 1992.

[7]	Nevin Heintze. Set based analysis of ML Programs. Technical Report CMU-CS-93-193, Carnegie Mellon University, July 1993.

[8]	Nevin Heintze and David McAllester. Linear-time subtransitive control flow analysis. In Proceedings of the SIGPLAN Conference on Programming Language Design and Implementation, pages 261-272, June 1997.

[9]	Alex Aiken and Nevin Heintze. Constraint-based program analysis. Tutorial Notes of the ACM Symposium on Principles of Programming Languages, January 1995.

[10]	Frank Tip. A survey of program slicing techniques. Technical Report CS-R9438, Centrum voor Wiskunde en Informatica, 1994

[11]	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.

[12]	Hubert Comon, Max Dauchet, Remi Gilleron, Florent Jacquemard, Denis Lugiez, Sophie Tison, and Marc Tommasi. Tree automata techniques and applications, April 1999.

[13]	Patrik 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. Springer-Verlag, proceedings of the 7th international conference on computer-aided verification edition, 1995.

[14]	Steven McCanne and Van Jacobson. The BSD packet filter: A new architecture for user-level packet capture. In Proceedings of the Winter 1993 USENIX Conference, pages 259-269. USENIX Association, January 1993.

[15]	Shamik Sharma, Anurag Acharya, and Joel Saltz. Deferred data-flow analysis. Technical Report TRCS98-38, University of California, Santa Barbara, December 1998.

[16]	Sungdo Moon, Mary W. Hall, and Brian R. Murphy. Predicated array data-flow analysis for run-time parallelization. In Proceedings of the ACM International Conference on Supercomputing, July 1998.

[17]	Glenn Ammons and James Larus. Improving data-flow analysis with path profiles. In Proceedings of the SIGPLAN Conference on Programming Language Design and Implementation, June 1998.

[18]	Charles Consel and Fran□ois No□l. A general approach for run-time specialization and its application to C. In Proceedings of The ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, January 1996.

[19]	Mark Leone and Peter Lee. Optimizing ML with run-time speicialzation. Technical Report CMU-CS-95-205, Carnegie Mellon University, December 1995.

[20]	Jeol Auslander, matthai philipose, Craig Chambers, Susan J. Eggers, and Brian N. Bershad. Fast, effective dynamic compilation. In Proceedings of SIGPLAN conference on Programming Language Design Implementation, June 1998

[21]	Brian Grant, Markus Mock, Matthai Philipose, Craig Chambers, and Susan J. Eggers. Annotation-directed run-time specialization in C. In Proceedings of The ACM Symposium on Partial Evaluation and Program Manipulations.

[22]	Charles Consel and Olivier Danvy. Tutorial notes on partial evaluation. In the Twentieth ACM Symposium on Principles of Programming Languages, January 1993.

[23]	You-Chin Fuh and Prate다 Mishra. Type inference with subtypes. Theoretical Computer Science, 73:155-175, 1990.

[24]	Tim Freeman and Frank Pfenning. Refinement types for ML. In Proceedings of the SIGPLAN Conference on Programming Language Design and Implementation, pages 268-277, 1991.

[25]	Mario Coppo, Ferruccio Damiani, and Paola Giannini. Refinement types for program analysis. In Lecture Notes in Computer Science, volume 1145. Springer-Verlag, 1996.

[26]	Thomas Reps and Todd Turnidge. Program specialization via program slicing. In Lecture Notes in Computer Science, volume 1110, pages 409-429. Springer-Verlag, 1996

[27]	Yanhong A. Liu. Dependence analysis for recursive data. In Proceedings of the IEEE International Conference on Computer Language, pages 206-215, May 1998.

[28]	Fran□ois Bourdoncle. Abstract debugging of higher-order imperative Languages. In Proceedings of the SIGPLAN conference on Programming Language Design and Implementation, 1993.

[29]	Sandip K. Biswas. A demand-driven set-based analysis. In Proceedings of The ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 372-385, 1997.

A. 증명

A.1 SVS의 정확성

다음의 두 보조정리는 정리 6을 증명하기 위해 사용되고, 정리 6은 다시 정리 7을 증명하는 데 사용된다.

보조정리 1. [eqn: C`` =`` B^* (C_0`)`], [eqn: D`` =`` atom(C`)`], [eqn: I_C`` =`` gm(C`)], [eqn: I_D`` =`` gm(D`)`]라 하면,

[eqn: v`` not in`` I_D (X`)`` ∃`` v`` not in`` I_D (a`)`]  for some [eqn: X`` subseteq`` a`] in [eqn: C]

이다.

증명. [eqn: v`` not in`` gm(C`)(X`)`]라 하면, [eqn: C`]는 [eqn: X`` subseteq`` se`]형태를 가지고 [eqn: v`` not in`` gm(C`)(se`)`]인 [eqn: X`]의 상한(upper bound)을 가진다. 따라서, [eqn: v`` not in`` I_D (X`)`` ∃`` v`` not in`` I_D (a`)`], [eqn: X`` subseteq`` a`] in [eqn: D`]이다. 이것은 어떤 [eqn: X`` subseteq`` a`` in`` C`]에 대해서, [eqn: v`` not in`` I_D (X`)`` ∃`` v`` not in`` I_D (a`)`]임을 의미한다.□

보조정리 2. [eqn: C`` =`` B^* (C_0`)`], [eqn: D`` =`` atom(C`)`], [eqn: I_C`` =`` gm(C`)`], [eqn: I_D`` =`` gm(D`)`]라 하면,

[eqn: I_D ``subseteq`` I_ C]

이다.

증명. [eqn: I_D`]가 [eqn: C`]의 모델, 즉 [eqn: v`` not in`` I_D (se`)`` Rightarrow`` v`` not in`` I_D (X`)`]임을 증명한다.

□ [eqn: X`` subseteq`` ae`]이 [eqn: C`]에 속할 경우

[eqn: Rightarrow] [eqn: X`` subseteq`` ae`]이 [eqn: D`]에 속하므로 참이다.

□ [eqn: X`` subseteq`` Y`]이 [eqn: C`]에 속하고, [eqn: v`` not in`` I_D (Y`)`]인 경우

[eqn: Rightarrow] [eqn: C`]에 속한 [eqn: v`` not in`` I_D (ae`)`]에 대해 [eqn: Y`` subseteq`` ae`]

(보조정리 1에 의해)

[eqn: Rightarrow] [eqn: X`` subseteq`` Y`]이고 [eqn: Y`` subseteq`` a`]이 [eqn: C`]에 속하므로,

[eqn: X`` subseteq`` ae`]가 [eqn: C`]에 속한다.

[eqn: Rightarrow] [eqn: X`` subseteq`` ae`]가 [eqn: D`]에 속한다.

[eqn: Rightarrow] [eqn: v`` not in`` I_D (X`)`] □

정리 6. 프로그램 [eqn: wp`]가 입력변수 [eqn: alpha`]를 가지고, [eqn: e`]는 [eqn: wp`]의 하위식이며, [eqn: V`]는 값의 집합이고, [eqn: wp`` □_i`` C_i`]에 의해 초기 관계식들이 만들어진다고 하면,  [eqn: □atom( B^* (C_i`` cup` \{ X_e`` subseteq`` V` \}))□`]는 [eqn: C_i`` cup` \{ X_e`` subseteq`` V` \}]의 최대 모델(greates model)이다.

증명. [eqn: C'`` =`` C_i`` cup` \{ X_e`` subseteq`` V` \}`]라 하자. 먼저, [eqn: gm(C`')`` =`` gm(B^* (C'`))`]임을 규칙 [eqn: B`]가 [eqn: gm(C'`)`]를 유지하는 관계식들만 추가한다는 것을 이용해서 보일 수 있다.

[eqn: {rm [TRANS]} ~~{X`` subseteq`` Y ~~~~ Y`` subseteq`` ae} over {X`` subseteq`` ae}]

[eqn: X`` subseteq`` Y`]와 [eqn: Y`` subseteq`` ae`]는 [eqn: I(X`)`` supseteq`` I(ae`)`]임을 의미하고, [eqn: X`` subseteq`` ae`]도 역시 이를 의미한다.

[eqn: {rm [TRANS-CON_1 ]} ~~{kappa` X`` subseteq`` Y ~~~~ Y`` subseteq`` kappa` Z} over {X`` subseteq`` Z}]

[eqn: kappa` X`` subseteq`` Y`]는 [eqn: I(X`)`` subseteq`` \{v ~|~ kappa` v`` in`` I(Y`)` \}`]를 의미하고,  [eqn: Y`` subseteq`` kappa` Z`]는 [eqn: I(Y`)`` subseteq`` \{kappa` v ~|~ v`` in`` I(Z`)` \}`]를 의미한다.  따라서, [eqn: kappa` X`` subseteq`` Y`]와 [eqn: Y`` subseteq`` kappa` Z`]는 [eqn: I(X`)`` subseteq`` I(Z`)`]를 의미하고, [eqn: X`` subseteq`` Z`]도 역시 이를 의미한다.

[eqn: {rm [TRANS-CON_2 ]}~~{kappa` X`` subseteq`` Y ~~~~ Y`` subseteq`` kappa` top} over {X`` subseteq`` top}]

[eqn: kappa` X`` subseteq`` Y`]는 [eqn: I(X`)`` subseteq`` \{v ~|~ kappa` v`` in`` I(Y`)` \}`]를 의미하고,  [eqn: Y`` subseteq`` kappa` top`]은 [eqn: I(Y`)`` subseteq`` \{kappa` v ~|~ v`` in`` Val` \}`]을 의미한다.  따라서, [eqn: kappa` X`` subseteq`` Y`]와 [eqn: Y`` subseteq`` kappa` top`]은 [eqn: I(X`)`` subseteq`` Val`]을 의미하고, [eqn: X`` subseteq`` top`]도 역시 이를 의미한다.

[eqn: {rm [TRANS-CON_3 ]} ~~{kappa` X`` subseteq`` Y ~~~~ Y`` subseteq`` overline{kappa'}` top} over {X`` subseteq`` top}]

[eqn: kappa` X`` subseteq`` Y`]는 [eqn: I(X`)`` subseteq`` \{v ~|~ kappa` v`` in`` I(Y`)` \}`]를 의미하고,  [eqn: Y`` subseteq`` overline{ kappa'}` top`]은 [eqn: I(Y`)`` subseteq`` \{kappa''` v ~|~ kappa''`` neq`` kappa'`, v`` in`` Val` \}`]을 의미한다. [eqn: kappa`` neq`` kappa'`]이기 때문에, [eqn: kappa` X`` subseteq`` Y`]와 [eqn: Y`` subseteq`` overline{kappa'}` top`]은 [eqn: I(X`)`` subseteq`` Val`]을 의미하고, [eqn: X`` subseteq`` top`]도 역시 이를 의미한다.

[eqn: {rm [TRANS-CON_4 ]} ~~{kappa` X`` subseteq`` Y ~~~~ Y`` subseteq`` top} over {X`` subseteq`` top}]

[eqn: kappa` X`` subseteq`` Y`]는 [eqn: I(X`)`` subseteq`` \{v ~|~ kappa` v`` in`` I(Y`)` \}`]를 의미하고,  [eqn: Y`` subseteq`` top`]은 [eqn: I(Y`)`` subseteq`` \{v ~|~ v`` in`` Val` \}`]을 의미한다. [eqn: \{v ~|~ kappa` v`` in`` Val`\} ``=`` Val`]이기 때문에, [eqn: kappa` X`` subseteq`` Y`]와 [eqn: Y`` subseteq`` top`]은 [eqn: I(X`)`` subseteq`` Val`]을 의미하고, [eqn: X`` subseteq`` top`]도 역시 이를 의미한다.

이제, [eqn: gm(B^* (C_i`))`` =`` gm(atom(B^* (C_i` )))`]을 증명해야 한다. [eqn: atom(B^* (C_i` ))`` subseteq`` B^* (C_i` )`]이므로, [eqn: gm(B^* (C_i` ))`` subseteq`` gm(atom(B^* (C_i` )))`]이고, 보조정리 2에 의해서, [eqn: gm(atom(B^* (C_i `)))`` subseteq`` gm(B^* (C_i` ))`]이 증명된다. □

다음의 보조정리는 정리 7을 증명하기 위해 사용된다.

보조정리 3. [eqn: wp`` □_i`` C_i`]이고, [eqn: I`]가 [eqn: C_i`` cup` \{X_0`` supseteq`` V_0` \}`]의 최소 모델이라고 하자. 모든 [eqn: e`` in`` wp`]에 대해, [eqn: I`` vdash`` e`` □`` v`]는 [eqn: v`` in`` I(X_e`)`]임을 의미하고, [eqn: nu`` in`` I(alpha`)`]일 때, [eqn: I`]는 [eqn: [ nu/ alpha`]` wp`]에 대해 안전한 집합 환경이다.

증명. [eqn: I`` vdash`` e`` □`` v`]의 집합 기반 의미 구조의 증명 트리 크기에 대한 귀납법을 사용해서 증명.

□ 증명 트리 크기가 1일 때

[eqn: {rm [VAR]}`` e``=``x]

[eqn: I(x`)`` vdash`` x``□`` v`` Rightarrow`` v`` in`` I(X_x` )` (의미~ 구조에~ 의해)]

[eqn: {rm [LAM]}`` e`` =`` lambda`x.e']

[eqn: I`` vdash`` lambda`x.e'`` □`` lambda`x.e' ``Rightarrow`` lambda`x.e'`` in`` I(X_e` )]

([eqn: I`]와 [eqn: □_i`]의 정의에 의해)

□ 증명 트리 크기가 1 이상일 때

[eqn: {rm [CON]}`` e`` =] con[eqn: kappa`` e`]

[eqn: I(X_e` )`` =`` V``]

[eqn: Rightarrow~~ I(X_1` )`` =`` \{v ~|~ kappa` v`` in`` V`\}]

([eqn: I`]와 [eqn: □_i`]의 정의에 의해)

[eqn: Rightarrow~~ (I`` vdash`` e_1`` □`` v'`` Rightarrow`` v'`` in`` \{v ~|~ kappa` v`` in`` V` \})]

(귀납 가설에 의해)}

[eqn: Rightarrow~~ (I`` vdash]con[eqn: kappa``e_1 ``□`` v`` Rightarrow`` v`` in`` V`)]

(의미 구조에 의해)

[eqn: {rm [DECON]}`` e`` =] decon[eqn: kappa``e_1]

[eqn: I(X_e` )`` =`` V``]

[eqn: Rightarrow~~ I(X_1` )`` = \{ kappa` v ~|~ v`` in`` V` \}]

([eqn: I`]와 [eqn: □_i`]의 정의에 의해)

[eqn: Rightarrow~~ (I`` vdash`` e_1`` □`` v'`` Rightarrow`` v'`` in`` \{kappa` v ~|~ v`` in`` V` \})]

(귀납 가설에 의해)}

[eqn: Rightarrow~~ (I`` vdash]decon[eqn: kappa``e_1 ``□`` v`` Rightarrow`` v`` in`` V`)]

(의미 구조에 의해)

[eqn: {rm [APP]}`` e`` =`` e_1`` e_2]

[eqn: I(X_e` )`` =`` V``]

[eqn: Rightarrow~~ I(X_{e'})`` subseteq`` V``]

[eqn: I(X_1` )`` subseteq`` Lam_wp (e_1` )]

[eqn: I(X_2` )`` subseteq`` I(X_x` )]

([eqn: I`]와 [eqn: □_i`]의 정의에 의해)

[eqn: Rightarrow~~ (I`` vdash`` e_1`` □`` lambda`x.e'`` Rightarrow`` lambda`x.e'`` in`` Lam_ wp (e_1` )]

[eqn: (I`` vdash`` e'`` □`` v`` Rightarrow`` v`` in`` V`)]

[eqn: I(x`)`` ni`` v'`, if`` I`` vdash`` e_2`` □`` v']

(귀납 가설에 의해)                [eqn: cdots] (*)

[eqn: Rightarrow~~ (I`` vdash`` e_1`` e_2`` □`` v`` Rightarrow`` v`` in`` V`)]

(의미 구조에 의해)

[eqn: {rm [CASE]}`` e`` =] case[eqn: {e_1}``{ kappa}``{e_2}``{e_3}]

[eqn: I(X_e` )`` =`` V``]

[eqn: 1)~~ Rightarrow~~ I(X_1` )`` subseteq`` kappa` top]

[eqn: I(X_2` )`` subseteq`` V``]

([eqn: I`]와 [eqn: □_i`]의 정의에 의해)

[eqn: Rightarrow~~ I`` vdash`` e_1`` □`` v_1`` Rightarrow`` v_1`` in`` kappa` top]

[eqn: I`` vdash`` e_2`` □`` v_2`` Rightarrow`` v_2`` in`` V``]

(귀납 가설에 의해)

[eqn: Rightarrow~~ I`` vdash]case[eqn: {e_1}``{kappa}``{e_2}``{e_3}`` □`` v~ Rightarrow~ v`` in`` V``]

(의미구조에 의해)

[eqn: 2)~~ Rightarrow~~ I(X_1` )`` subseteq`` overline{ kappa}` top]

[eqn: I(X_3` )`` subseteq`` V``]

([eqn: I`]와 [eqn: □_i`]의 정의에 의해)

[eqn: Rightarrow~~ I`` vdash`` e_1`` □`` v_1`` Rightarrow`` v_1`` in`` overline{kappa}` top]

[eqn: I`` vdash`` e_3`` □`` v_3`` Rightarrow`` v_3`` in`` V``]

(귀납 가설에 의해)

[eqn: Rightarrow~~ I`` vdash]case[eqn: {e_1}``{kappa}``{e_2}``{e_3}`` □`` v~ Rightarrow~ v`` in`` V``]

(의미구조에 의해)

[eqn: 3)~~ Rightarrow~~ I(X_2` )`` subseteq`` V``]

[eqn: I(X_3` )`` subseteq`` V``]

([eqn: I`]와 [eqn: □_i`]의 정의에 의해)

[eqn: Rightarrow~~ I`` vdash`` e_2`` □`` v_2~ Rightarrow~ v_2`` in`` V``]

[eqn: I`` vdash`` e_3`` □`` v_3~ Rightarrow~ v_3`` in`` V``]

(귀납 가설에 의해)

[eqn: Rightarrow~~ I`` vdash]case[eqn: {e_1}``{kappa}``{e_2}``{e_3}`` □`` v~ Rightarrow~ v`` in`` V``]

(의미 구조에 의해)

집합 환경이 모든 닫힌 식 [eqn: e_0`]의 수행 중에 일어날 수 있는 결합을 가진다면, 그 집합 환경은 [eqn: e_0`]에 대해 안전하다고 한다[20]. [eqn: Lam_wp (e_1` )`` ni`` lambda`x.e'], [eqn: I(alpha`)`` ni`` nu`]일 때 모든 호출식 [eqn: {e_1}``{e_2}]에 대해, [eqn: I(X_x` )`` subseteq`` I(X_2` )]이므로, (*)는 [eqn: I`]가 [eqn: [ nu/ alpha`]` wp`]에 대해 안전하다는 것을 보여준다. □

정리 7. ([eqn: SVS_wp (e`` subseteq`` V`)`]의 안전성) 프로그램 [eqn: wp`]의 입력 변수가 [eqn: alpha`], 하위식 [eqn: e`` in`` wp`]라 하자. [eqn: Sigma`` in`` SVS_wp (e`` subseteq`` V`)`]이면 [eqn: □`nu`` in`` Sigma`( alpha`)([ nu/ alpha`] wp`` mapsto^*`` □[v_e`]`` Rightarrow`` v`` in`` V`)`]이다.

증명. 정리 6에 의해, [eqn: Sigma`]는 [eqn: C_i`` cup` \{X_e`` subseteq`` V` \}`]의 최대 모델이다. 따라서, 보조정리 3에 의해, [eqn: Sigma`` vdash`` e`` □`` v~ Rightarrow~ v`` in`` Sigma(e`)`]이고, [eqn: Sigma`]는 [eqn: [nu/ alpha`]` wp`]에 대해 안전한 집합 환경이다. 또, [eqn: Sigma`]가 [eqn: C_i`` cup` \{X_e`` subseteq`` V` \}`]의 최대 모델이므로, [eqn: Sigma`(e`)`` subseteq`` V`]이다.

따라서, [eqn: [ nu/ alpha`]` wp`` mapsto^*`` □[v_e `]]

[eqn: Rightarrow~~ Sigma`` vdash`` e`` □`` v``]

([eqn: Sigma`]는 [eqn: [nu/ alpha`]` wp`]에 대해 안전하므로)

[eqn: Rightarrow~~ v`` in`` Sigma`(e`)]

(보조정리 3에 의해)

[eqn: Rightarrow~~ v`` in`` V``]

([eqn: Sigma`]는 최대 모델이므로)

□

A.2 psba의 안전성

정리 8. ([eqn: psba`]의 안전성) [eqn: [ nu/ alpha`]` wp`` mapsto^*`` □[v_l`]`]이면  [eqn: v`` in`` psba_nu ( wp`)(l`)]이다.

증명. [eqn: psba`]가 [eqn: sba_nu`]의 안전한 예측(approximation)이라는 것을 보임으로써 [eqn: psba`]의 안전성을 증명한다. 먼저, [eqn: sba_nu ( wp`)`]와 [eqn: psba_nu ( wp`)`]의 닫힌 집합(closure)에 해당하는 두 개의 연속(continuous) 함수 [eqn: F_nu`]와 [eqn: P_nu`]를 정의한다[13]. 그리고 나서, [eqn: P_nu`]의 최소 고정점(least fixpoint)이 [eqn: F_nu`]의 최소 고정점보다 크거나 같음을 증명한다.

프로그램 [eqn: wp`]의 초기 관계식 [eqn: C`]가 [eqn: wp``□``C`]에 의해 도출되어졌다고 하면, [eqn: sba_nu (wp`)`]는 [eqn: F_nu` :` (Vars(C`)`` rightarrow`` 2^{Val}`)`` rightarrow`` ( Vars(C`)`` rightarrow`` 2^{Val}`)`]의 최소 고정점 [eqn: lfp`` F_nu`]와 같다[13].

또 다른 연속 함수 [eqn: P_nu` : (Vars(C`)`` rightarrow`` 2^{Val}`)`` rightarrow`` (Vars(C`)`` rightarrow`` 2^{Val}`)`]를 [eqn: psba_ nu ( wp`)`]이 [eqn: P_nu`]의 최소 고정점 [eqn: lfp`` P_nu`]와 같아 지도록 정의한다. 식 [eqn: overline{e}`]는 그 식의 집합 관계식이 입력과 무관하다는 것을 나타내고, [eqn: underline{e}`]는 그 식의 집합 관계식이 입력에 의존적인 [eqn: X_e`` supseteq`` se_□`]이라는 것을 나타낸다. 아무런 줄도 그어지지 않은 식은 입력에 의존적인지, 무관한지를 구별할 필요가 없는 식임을 의미한다. case[eqn: {e_1}``{kappa}``{e_2}``{e_3}`]의 [eqn: e_1`]을 제외하고는, [eqn: P_nu (varphi`)( overline{e}`)`]이 [eqn: P_nu (varphi`)(underline{e}`)`]와 정확하게 일치한다.

[eqn: Q (varphi`, rho`)`]가

[eqn: (□`e`` in`` wp`. varphi(X_e` )`` supseteq`` rho( X_e` ))]

[eqn: wedge`` (varphi`` subseteq`` lfp`` P_nu` )`` wedge`` (rho`` subseteq`` lfp`` F_nu` )]

일 때, [eqn: Q(lfp`` P_nu` , lfp`` F_nu` )`]를 고정점 귀납법(fixpoint induction)을 사용해서 증명한다.

[eqn: Q( emptyset`, emptyset`)`]는 당연히 참이다.

이제, 귀납 가설이 [eqn: Q( varphi`, rho`)`]일 때, [eqn: Q(P_nu (varphi`)`, F_nu (rho`))`]가 성립함을 보이면 된다. 즉, [eqn: P_nu (varphi`)(X_e` )`` supseteq`` F_nu (rho`)(X_e` )`]를 보이면 된다.

[eqn: {rm [CON]}~ e`` =] con[eqn: {kappa}``{e_1}].

[eqn: P_nu (varphi`)(X_e` )`` =`` \{ kappa` v ~|~ v`` in`` varphi(X_1` )` \}]

(정의에 의해)}

[eqn: supseteq`` \{ kappa` v ~|~ v`` in`` rho(X_1` )]

(귀납 가설에 의해)

[eqn: =`` F_nu (rho`)(X_e` )]

(정의에 의해)

[eqn: {rm [CASE]}`]를 제외한 다른 경우들은 모두 비슷하게 증명되어진다.

[eqn: {rm [CASE]}~ e`` =`` case{underline{e_1}}``{kappa}``{e_2}``{e_3}].

[eqn: P_nu (varphi`)(X_e` )]

[eqn: matrix {=}& {\{v ~|~ v`` in`` varphi(X_2` ), nu`` not in`` SVS_wp (X_1`` subseteq`` overline{kappa}` top`)(alpha`)` \}}# {}& {cup` \{v ~|~ v`` in`` varphi(X_3` ), nu`` not in`` SVS_wp (X_1`` subseteq`` kappa` top`)(alpha`)` \}} }]

(정의에 의해)

[eqn: matrix {=}& {\{v ~|~ v`` in`` varphi(X_2` ), kappa` v'`` not in`` (lfp`` F_nu )(X_1 )` \}}# {}& {cup` \{v ~|~ v`` in`` varphi(X_3` ), kappa'` v''` not in`` (lfp`` F_nu )(X_1 ),kappa' neq kappa` \}} }]

(*)

[eqn: matrix {=}& {\{v ~|~ v`` in`` varphi(X_2` ), kappa` v'`` not in`` rho(X_1`) \}}# {}& {cup` \{v ~|~ v`` in`` varphi(X_3` ), kappa'` v'`` not in`` rho(X_1`), kappa'neq kappa` \}} }]

(귀납 가설에 의해)

[eqn: =~ F_nu (rho`)(X_e` )]

(정의에 의해)

정리 4와 정리 7에 의해 [eqn: v`` in`` sba_nu (X`)`` wedge`` v`` not in`` V``] [eqn: Rightarrow]  [eqn: nu`` not in`` SVS_wp (X`` subseteq`` V`)( alpha`)`]이므로, (*)는 사실이다. □