2023년 11월 14일 (화) 03:19에 Ahn9807님의 편집

2023-11-14T03:19:52Z

← 이전 판		2023년 11월 14일 (화) 03:19 판
1번째 줄:		1번째 줄:
	[[분류: ~~프로그램 분석~~]]		[[분류: Abstract interpretation]]

	== 개요 ==		== 개요 ==

Ahn9807: 새 문서: 분류: 프로그램 분석 == 개요 == Widening은 fix point iterations에서 lattice가 infinite이거나, search space가 너무 크면 수렴에 무한히 (오랜)시간이 걸리는 문제를 해결하기 위해서, step을 한번에 크게 가져가는 것을 말한다. widening operation은 $\bigtriangledown : D^{\sharp} \times D^{\sharp} \rightarrow D^{\sharp}$ 라는 기호로 표기한다. 여기서 다음 조건을 만족시키는 finite chain Y를...

2023-11-14T03:08:54Z

새 문서: 분류: 프로그램 분석 == 개요 == Widening은 fix point iterations에서 lattice가 infinite이거나, search space가 너무 크면 수렴에 무한히 (오랜)시간이 걸리는 문제를 해결하기 위해서, step을 한번에 크게 가져가는 것을 말한다. widening operation은 <math>\bigtriangledown : D^{\sharp} \times D^{\sharp} \rightarrow D^{\sharp}</math> 라는 기호로 표기한다. 여기서 다음 조건을 만족시키는 finite chain Y를...

새 문서

[[분류: 프로그램 분석]]

== 개요 ==
Widening은 fix point iterations에서 lattice가 infinite이거나, search space가 너무 크면 수렴에 무한히 (오랜)시간이 걸리는 문제를 해결하기 위해서, step을 한번에 크게 가져가는 것을 말한다.

widening operation은
<math>\bigtriangledown : D^{\sharp} \times D^{\sharp} \rightarrow D^{\sharp}</math>
라는 기호로 표기한다.

여기서 다음 조건을 만족시키는 finite chain Y를 다음과 같이 정의 가능하다.

<math>\bigsqcup_{i \geq 0}F^i(\bot) \sqsubseteq Y_{lim}</math>

여기서 Y는 <math>\bigtriangledown</math>를 통해서 다음과 같이 정의된다.

<math>Y_0 = \bot</math><br>
<math>Y_{i+1} = \begin{cases} Y_i & \mbox{if } F(Y_i) \sqsubseteq Y_i \\ Y_i \bigtriangledown F(Y_i) & \mbox{otherwise} \end{cases}</math>

''쉽게 설명 하자면'', widening operator는 무조건 finite해야 하며 (당연히 유한 시간안에 operation을 끝내야 함으로), 또한 Y의 upper bound는 무조건 원래 수렴하는 step보다는 크다.

== 예시 ==
<syntaxhighlight lang=c>
x = 0;
while (*) {
x++;
}
</syntaxhighlight>
<math>\bigtriangledown : D^{\sharp} \times D^{\sharp} \rightarrow D^{\sharp}</math>
를 다음과 같이 정의하면 <br>
<math>[a,b] \bigtriangledown \bot = [a,b]</math>

<math>\bot \bigtriangledown [c,d] = [c,d]</math>

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

처음 시작에서는 [0, 0]으로 range doamin이 시작하지만 다음 [0, 1]에서 widening되어서 [0, infty]로 widening된 결과를 가진다.

== 같이 보기 ==
# [[Narrowing]]

Widening - 편집 역사

2023년 11월 14일 (화) 03:19에 Ahn9807님의 편집