https://en.wikipedia.org/wiki/Abstract_interpretation 해석 하는 방법

Question

https://en.wikipedia.org/wiki/Abstract_interpretation 여기에서
n other cases, it is still possible to obtain such an x′ through a (pair-)widening operator,[4] defined as a binary operator ∇:L×L→L which satisfies the following conditions:

1. For all x

   and y

   , we have x≤x∇y

   and y≤x∇y

   , and

2. For any ascending sequence (yn′)n≥0

   , the sequence defined by x0′:=⊥

   and xn+1′:=xn′∇yn′

   is ultimately stationary. We can then take yn′=f′(xn′)

   기호, 설명 다 이해가 안되는데 어떻게 하면 이해할 수 있는지 궁금합니다

   .

Answer 1

안녕하세요. 서종현 전문가입니다.

위키피디아 추상 해석 설명은 수학적 기호와 개념이 복잡해 이해하기 어려우실수 있습니다.

1. 추상 해석은 프로그램의 동작을 정확하게 실행하지않고 간락화된 (추상화된)값 범위로 분석하는 기법입니다.

2. 여기서 ∇(폭넓힘 연산자, widening operator)는 두 추상 값 x,y를 받아서 더 큰 추상값을 반환하는 함수입니다. 조건은 x≤x∇y와 y≤x∇y를 만족해야 하고, 계속 반복해도 값이 어느 시점에서 변하지 않는 (안정되는)것을 보장합니다.

3. 식에서 x_0' =⊥는 시작값(가장 작거나 없는 상태)이고, x_n +1' = x_n'∇y_n'는 이전 결과에 새로운 값을 폭넓힘 연산으로 합치는 과정입니다.

4. 이 과정을 통해 점점 커지는 값들의 무한한 상승을 막고 최종적으로 안정화된 값을 얻을 수있습니다.

이해에는 수학 기초(부분순서,연산자 함수 이해)가 필요하므로, 먼저 순서 관계(≤),함수정의,시퀀스(수열)개념부터 익히시는 것이 좋습니다.

단계별로 기호 하나씩 찾아보고, 간단한 예제로 차근차근 풀어보시면 도움이 됩니다. 이해가 어렵다면 관련 수학 기초서나 추상 해석 입문 자료를 함께 참고하시길 추천드립니다.

Answer 2

안녕하세요. 김상규 전문가입니다.

일단 내용상

위키피디아 의 요약 해석 관련해서

확장 연산자에 관련된 내용을 설명한 부분인데요.

일단 기호 들을 다 설명해드릴 방법은 없습니다.

다만 올려주신 내용의 해석된 내용을 보면

▶ 다른 경우에도 다음 조건을 만족하는 이진 연산자 ∇:L×L→L로 정의된 (pair-)widening 연산자[4]를 통해 이러한

x'를 얻을 수 있습니다:

모든 x에 대하여

그리고 y

we have x≤x∇y

그리고 y≤x ∇

,그리고.

오름차순 (yn')n≥0의 경우

, x0':= ⊥로 정의된 시퀀스

and xn+1′:=xn′∇yn′

는 궁극적으로 정지 상태입니다. 그러면 yn'=f'(xn')를 취할 수 있습니다 ◀

〓〓〓〓〓〓〓〓〓〓〓〓〓〓〓〓〓〓〓〓〓〓〓〓〓〓〓〓〓〓〓

올려주신 말들을 이해하기 위해서 필요한 부분은

확장연산자를 통해 해석가능하다는 부분에서

컴퓨터 과학 내에서 추상적 해석을 알아야하는데

특히 격자와 같은순서집합에 대한 단조함수를 기반으로 하는

컴퓨터 프로그램 의미론에 대한 이론입니다.

모든 계산을 하지않고도 의미론에 대한 정보를 얻는

컴퓨터 프로그램의 부분적 실행으로 볼 수 있는데요

이런 분석의 두가지 용도로는

• 컴파일러 내부에서 프로그램을 분석하여 특정 최적화 또는 변환이 적용가능한지 결정

• 디버깅이나 버그 클래스에 대한 프로그램 인증을 위해 사용

으로 볼 수 있습니다.

위에서

이진 연산자 ∇:L×L→L 라는 부분을 볼 때

순서집합 L 의 기호가 사용되는 것으로 보아

추상화 함수를 쓰는 것으로 볼 수 있으며

결국 추상화 해석을 알아야만 해석이 가능하겠습니다

그 안에서 L 은 순서 집합, L`는 추상집합이라 정의하고

이 두집합 요소를 하나에서 다른 하나로 매핑하는 전체함수를 정의하여

서로 관련이 있습니다.

프로그램 의미론에서 일반적으로

고정점의 추상화는

구체적인 의미론 는 단조함수인데

이것은 knaster - Tarski정리에 따르면 존재하는데..

다른경우에는 쌍 학대 연산자를 통해

이진연산자로 정의되고

거기에서 위에 나열하신 ∇:L×L→L 조건을 만족한다고 나옵니다.

결국 컴퓨터 과학 분야에서

추상적해석을 공부하지 않으신다면

저 위의 내요은 전혀 이해하기 힘드실 듯 합니다.

추상적해석은

1970년대 후반

프랑스 컴퓨터 과학자 부부인

patric cousot / Radhia Cousot 에 의해 공식화 되었습니다.