Narrowing

개요

Widening과 같은 경우에는 Overshooting을 통해서 finite한 시간안에 Least fixed point를 찾도록 해주지만, 너무 Overshooting되어서 precise한 결과를 가져오지 못하는 한계가 있다. 이를 해결하기 위해서 Narrowing을 통해서 Widening된 해답을 Optimal solution을 향해서 좁혀나가는 것을 의미한다.

Narrowing operation은 [math]\bigtriangleup : D^{\sharp} \times D^{\sharp} \rightarrow D^{\sharp}[/math] 라는 기호로 표기한다.

여기서 finite chain Z를 다음의 조건을 반드시 만족시켜야 한다.

[math]\bigsqcup_{i \geq 0}F^i(\bot) \sqsubseteq Z_{lim}[/math]

이를 만족시키는 Z는 [math]\bigtriangleup[/math]를 통해서 다음과 같이 정의된다. 식에서 Y는 Widening에서 설명한 finite chain Y이며, 각 widening의 step의 집합을 의미한다.

[math]Z_0 = Y_{lim}[/math]

[math]Z_{i+1} = Z_i \bigtriangleup F(Z_i)[/math]

예시

x = 0;
while (x < 10) {
    x++;
}

[math]\bigtriangleup : D^{\sharp} \times D^{\sharp} \rightarrow D^{\sharp}[/math] 를 다음과 같이 정의하면
[math][a,b] \bigtriangleup \bot = [a,b][/math]

[math]\bot \bigtriangleup [c,d] = [c,d][/math]

[math] [a,b] \bigtriangleup [c,d] = [(c == -\infty? c : a), (b == +\infty? d : b)][/math]

Widening을 통해서 나온 결과는 [0, +infty]인데, [0, + infty] [math]\bigtriangleup[/math] [0, 10] = [0, 10]임으로 최종적으로 x가 while loop에서 가질수 있는 한계는 [0, 10]으로 좁혀진다.