문서 편집 권한이 없습니다. 다음 이유를 확인해주세요: 요청한 명령은 다음 권한을 가진 사용자에게 제한됩니다: 사용자. 문서의 원본을 보거나 복사할 수 있습니다. [[분류: 프로그램 분석]] == 개요 == [[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><br> <math>Z_{i+1} = Z_i \bigtriangleup F(Z_i)</math> == 예시 == <syntaxhighlight lang=c> x = 0; while (x < 10) { x++; } </syntaxhighlight> <math>\bigtriangleup : D^{\sharp} \times D^{\sharp} \rightarrow D^{\sharp}</math> 를 다음과 같이 정의하면 <br> <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]으로 좁혀진다. Narrowing 문서로 돌아갑니다.