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

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

일단 내용상

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

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

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

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

▶ 다른 경우에도 다음 조건을 만족하는 이진 연산자 ∇: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 에 의해 공식화 되었습니다.