[프로그래밍언어론] 4. Semantics

Static Semantics & Attribute Grammar

프로그래밍 언어의 큰 2가지 축은 Syntax 와 Semantics다.

syntax(문법)은 지금 들어온 코드의 문법이 맞다 틀리다만 판단할 수 있다.

하지만 이 문법만 가지고는 문장의 의미를 알 수 없다.

 

코드를 예로 든다면, 먼저 변수를 선언하고나서 값을 할당해야하는데, 선언하지도 않은 변수에 값을 할당하는 것은 문법적으로는 옳을 수 있어도 문맥상, 의미상으로는 올바르지 않은 코드이다.

 

Static Semantics 는 컴파일하는 순간에 알 수 있으며, 프로그램  실행 중 변하지 않는 시멘틱스 정보다.

Attribute Grammars (AG) 는 static semantics 정보를 최대한 알아내고자 등장했다.

 

AG는 CFG (Context Free Grammar) 에 시멘틱 정보를 추가한 것과 같다.

CFG는 파싱트리로 나타낼 수 있기 때문에 AG를 사용하면 Semantic 정보를 파싱 트리의 각 노드에 추가한다.

 

Attribute Grammar는 논리식을 이용해서 표현한다.

각각의 grammar symbol x 에 대해, x가 갖고 있는 attribute values 의 집합 A(x) 가 존재한다.

 

위 예시를 보자.

BNF 를 보면 X0 를 X1 으로 확장하라는 규칙이 존재한다.

 

이런 규칙을 하나로 모아서 함수에 넣을 수 있다.

논 터미널들은 1개 이상의 규칙을 갖기 때문에 논 터미널에 대한 Attribute 여러개를 하나의 함수로 모을 수 있다는 뜻이다.

이렇게 하나의 함수로 모아진 attribute 를 synthesized attribute 라고 한다.

 

어떤 규칙 Xj 가 X0 ~ Xn  이 결정되는 순간 결정된다고 하자.

그러면 이런 Xj 에 대해 inherited attributes 라고 한다.

 

또 terminal 들은 처음부터 의미가 정해져 있어 intrinsic attributes 라고 한다.

원래 있는 attribute 라는 의미이다.

Example

 

 

위와 같은 BNF 문법이 있다고 해보자.

 

변수 A, B, C 는 선언할 때 반드시 타입을 같이 가져야 한다.

따라서 A, B, C 는 데이터 타입에 대한 actual_type attribute를 가지고 있다. (intrinsic attribute) 

 

actual_type 속성은 <var> 입장에서는 A, B, C 속성을 하나로 모았고, <expr> 입장에서는 <var> + <var> 또는 <var> 속성을 하나로 합성한 것과 같으므로 <var> <expr> 에 대한 synthesized attribute 이다.

 

<expr> 는 예상되는 타입에 대한 attribute인, expected_type 속성을 갖는다.

expected_type 속성은 actual_type 이 결정되어야 결정되는 inherited attribute 이다.

 

위의 syntac, semantic 규칙을 이용하면 <expr> 의 타입을 정할 수 있다.

따라서 semantic rule 로 <expr> 의 actual_type 속성은 <var>[1] 의 actual_type 에 의해 결정된다는 규칙을 만들었다.

 

단, 이 규칙을 적용할 때 전제 조건이 있다.

1. var1의 actual_type 과 var2의 actual_type 이 같아야 한다.

2. expr의 expected_type 은 expr의 actual_type 과 같아야 한다

 

Example 2

 

syntax 규칙에 따르면 <var> 이라는 논터미널은 id 라는 터미널로 전개된다.

semantic 규칙에 따르면 <var>의 actual_type은 <var> 의 string 속성을 보고(look up) 결정한다.

 

---

synthesized attribute 는 파싱트리의 밑에서부터 올라가면서 attribute 들을 모아 그 값을 계산할 수 있다.

inherited attribute 는 파싱트리의 위에서부터 내려가면서 attribute 뜻을 가져와 그 값을 계산할 수 있다.

보통은 합성된 속성과 상속된 속성이 섞여있으므로 바텀-업, 탑-다운을 바꿔 수행하면서 attribute 의 값을 계산해나간다.

 

Example 3

 

<expr>의 expected_type은 부모 속성에 의해 결정되는 inherited 속성이다.

<var> 의 actual_type 은 A, B를 변수 테이블에서 찾아 알아온다.

그리고 <var>[1] 과 <var>[2] 의 actual_type 속성이 같은지 검사한다.

 

만약 두 타입이 같다면 <expr> 의 actual_type 속성을 <var>[1] 의 actual_type 으로 결정한다.

이제 <expr> 의 actual_type 과 expected_type 이 같은지 최종 검사하여 symantic 규칙이 올바른지 검사한다.

 

---

Semantics

위에서는 컴파일 타임에 정할 수 있는 Static Semantcis 에 대해 논의하였다.

하지만 사실 프로그래밍 언어의 시멘틱 의미를 수학적으로 정확하게 맞춰주는 방법은 없다.

유사하게 맞춰주는 방법론이 몇 개 존재할 뿐이다.

하지만 그럼에도 시멘틱은 알아야하고, 표현할 수 있는만큼 수학적으로 표현해야 한다.

이 시멘틱스가 잘 정의되면 프로그래밍 언어를 만들고 설계하는 사람들이 이 기능과 저 기능 사이에 불일치가 있는지 확인할 수도 있다.

 

이제 최대한 semantic 을 알아내고자 하는 3가지 방법을 정리한다.

---

Operation Semantics

수학적으로 정의할 수 있는 시멘틱 중 제일 쉬운 시멘틱

기계에서 문장을 실행(Operate)시켜봄으로써 프로그램의 의미를 확인한다.

(메모리, CPU, 레지스터 등에 값이 잘 들어가 있는지 확인)

 

하지만 순수하게 모든 하드웨어 기능을 묘사하는 인터프리터는 구현하는 비용이 크다.

그래서 소프트웨어로 하드웨어의 동작을 묘사하려고 해도, 정확하게 묘사하는 것은 쉽지 않다.

또 하드웨어에 따라 그 상태가 중간중간 다르게 변할텐데 그 전부를 소프트웨어로 묘사하는 것도 쉽지 않고,

일부 시멘틱 정의는 기계에 종속적일 수도 있다.

 

대안은 컴퓨터를 완전히 시뮬레이션 하는 것이다. (가상 머신)

그래서 소스코드를 기계어로 번역하는 번역기를 만들고, 소스코드를 실행할 컴퓨터에 대한 시뮬레이터를 만든다.

하지만 오퍼레이션 시맨틱을 평가하는 것은 매우 복잡한 일이다.

 

오퍼레이션 시멘틱은 프로그래밍 언어의 매뉴얼, 교과서에 사용되고, 언어를 교육하는데도 사용된다.

Operational Semantics 를 사용하는 단계는 크게 2가지가 있다.

 

Natural Operational Semantics

Structural Operational Semantics

 

Denotational Semantics

재귀 함수 이론에 기반한 시맨틱으로, 가장 추상적인 시맨틱스 묘사 방법이다.

수학적 오브젝트를 만들고 프로그래밍 언어의 구성 요소 하나하나에 수학적 오브젝트와 매칭되는 함수를 만든다.

 

예를 들어 프로그램의 상태 s 를 아래와 가팅 정의한다고 해보자.

 

프로그램의 상태 s는 변수값 v가 바뀔 때마다 변한다.

VARMAP 함수를 사용하면 현재 상태 s의 변수 i 의 값 v를 알 수 있다.

 

 

구체적인 예시를 보면 또 아래와 같은 예시가 있다.

Mdec 라는 함수는 문자열 숫자를 받아서 십진수 수로 바꾸는 함수이다.

만약 인자로 <dec_num> 과 문자가 들어오면 앞에 10을 곱하고 뒤에 들어온 문자를 10진수로 변환한 값을 더해준다.

denotational semantics는 위와 같이 문자로 들어온 수를 실제로 '정수' 라는 의미로 변환하는 과정을 묘사한다.

 

Expression

그렇다면 expression 은 denotational semantics 로 어떻게 표현할까?

수학에서 표현식은 연산자와 피연산자로 구성된다.

쉽게 생각하기 위해 binary operator 만 생각해보자.

 

우선 숫자에 대한 표현식은 위에서 본대로 문자를 그대로 계산해서 십진수 수를 돌려준다.

변수에 대한 표현식은 state 에서 해당 변수의 이름을 통해 값을 조회한다. (VARMAP 함수)

만약 프로그래머가 선언하지 않은 변수를 사용했다면 VARMAP 함수에서 값을 찾지 못했을테니 에러를 내면 된다.

 

이것이 Denotational semantics 이다.

 

 

이걸 이렇게 표현할 수 있다.

굉장히 복잡하고 꼼꼼하게 만들어져있다..

 

Assignment Statements

변수에 새로운 값을 넣어 상태를 바꾸는 것으로 시멘틱스를 정의한다.

 

대충 할당할 수 있으면 VARMAP으로 상태를 업데이트 하고, 아니면 에러를 내라는 의미이다.

 

Loop

 

while 반복문에 대한 denotaional semantics 는 위와 같다.

먼저 불러인 값이 들어있는 B를 Mb 함수를 이용해 상태에 있는지 확인한다.

만약 정의되어있지만 않다면 (undef) 에러를 내고, 아니라면 Mb의 값이 참, 거짓인지 확인한다.

만약 거짓이면 현재 상태에서 변한게 없으니 s를 그대로 돌려주고,

만약 참이면 L  의 상태를 확인해서 Error 를 내거나 L이 실행되어서 만들어진 새로운 상태 sl에 대해 반복한다.

 

위 그림에서 보다시피 반복을 표현하기 위해 재귀 (recursion) 을 사용했음을 알 수 있다.

이게 괜찮은 이유는 반복 (iteration)은 항상 그와 똑같이 동작하는 재귀 (recursion) 동작으로 바꿀 수 있음이 수학적으로 증명되어 있기 때문이다.

---

denotaion semantics 는 이처럼 이 프로그램이 맞는 결과를 내는지 수학적으로 확인하고자 할 때 사용한다.

또 이를 통해 언어를 디자인하는데 쓸 수도 있고, 컴파일러가 만들어낸 코드가 정확한지 확인해서, 컴파일러를 만드는데 도움을 준다.

---

Axiomatic Semantics

이번엔 이산수학에서 사용하는 논리를 이용한 Axiomatic Semantics 에 대해 정리한다.

Axiomatic 은 '공리' 당연한 사실을 말한다.

 

Axiomatic Semantics는 프로그램이 맞나 틀리나 수학적 수식을 이용해서 증명하겠다는 의미다.

(format program verification)

 

Axiom 은 논리식 (assertion) 처럼 생겼다.

assertion 은 3가지 파트로 구성되어 있다.

 

우선 프로그래밍을 실행하기 전에 확인할 조건이 앞에 있고, (pre condition)

가운데에 실행해야 되는 프로그래밍 언어의 문장이 온다.

그리고 문장이 실행된 이후 post condition 이 나온다.

 

프로그래밍 언어에서 pre condition은 약할 수록 좋다.

그래야 프로그래밍 언어의 문장이 실행되기 쉽기 때문이다.

그리고 그래야 post condition 이 실행되기 쉽다.

 

Axiomatic semantics 형태를 예시를 들어보면 아래와 같이 생겼다.

 

P 라고 하는 pre condition 이 있고, statement 이후 Q 라는 post condition 이 나온다.

예를 들어 a = b+1 이라는 문장이 있고, 이 문장이 실행되면, a > 1 이라는 post condition 이 만족된다고 하자.

 

가능한 pre condition 중 하나는 b > 10 이다.

하지만 가능한 pre condition 중 제일 약한 (범위가 넓은) 조건은 b > 0 이다.

 

실제 프로그램을 검증할 때 post condition 은 프로그램의 원하는 결과를 의미한다.

만약 첫번째 statement 에 대한 pre condition 이 프로그램의 실행 사양과 동일하다면 이 프로그램은 잘 짜여진 프로그램이다.

 

Assignment

Axiomatic Semantics 로 assignment statement 는 어떻게 묘사하는지 보자.

 

x = E 라는 statement 에 대해 precondition 은 Qx->E, postcondition 은 Q 이다.

이때 다음과 같은 공식이 존재한다.

 

 

P 가 만족하면 S 가 실행되어 Q 를 만족할 때, 만약 P' 이면 P 이고, Q 면 Q' 이라면

P' 만 만족해도 S 가 실행되어 Q' 까지 만족할 것이라는 것이다.

Sequences

 

또 이런 공식도 존재한다.

P1 이면 S1 이 실행되어 P2 로가고

P2 이면 S2 가 실행되어 P3 으로 가는 경우, P1 이 실행되면 S1, S2가 실행되어 P3 으로 가는 것과 같다.

 

따라서, P1 을 만족하면 S1, S2가 순차적으로 실행되는 것을 의미한다.

 

Selection

if B then S1 else S2 라는 문장은 Axiomatic Semantics 로 이렇게 표현할 수 있다.

 

B 와 P 가 모두 참이면 S1 을 실행하고 Q 가 된다.

만약 B 가 거짓이고 P가 참이라면 S2 가 실행되어 Q 가 된다.

 

B에 의해 S1, S2 가 결정되어 실행되고, Q 라는 동일 조건으로 오게 된다.

 

Loop

 

while 문은 I 와 B 가 모두 참이면 S 를 실행하고 I 라는 조건으로 돌아온다.

이는 I 가 만족하면 while 문을 실행하고, S 가 실행된 결과로는 B 가 거짓이어야 한다는 것을 의미하는 것과 같다.

 

이 I 를 loop invariant 라고 한다.

이 값은 변하지 않는 값을 의미한다.

이 I, loop invariant 가 너무 강한 조건이면 반복문이 실행되기 힘들다.

따라서 이 I 는 약한값이 되는 것이 좋다.

하지만 루프를 종료하는 조건과 I 가 연결될 때는 I가 충분히 강해야 한다.

그래야 반복문이 무한 반복문으로 가지 않고 끝날 수 있기 때문이다.

---

Denotaional Semantics  vs  Axiomatic Semantics

두 방식 모두 쓸모가 있다.

Axiomatics 방식은 프로그램이 정확하다 정확하지 않다를 증명할 때 굉장히 편해진다.

하지만 너무 어렵다..

그래서 우리는 Operational Semantics 를 사용하려고 한다.