[PL] Semantics : Formal Semantics, Operational Semantics, Proof Tree
Compiler / Programming Language
1. 프로그래밍언어의 Semantic
프로그래밍 언어의 semantic은 "프로그램이 어떻게 동작하는 것인가"에 대한 것이다.
📌 Example
e1 + e2는 무엇인가?(+는 현재 ADD 노드일 뿐)
💨calculate e1, calculate e2, sum up the two cacluation results이다.semantic은 Abstract Syntax을 기반으로 정의된다. 따라서 불필요한 디테일은 무시할 수 있다.
프로그래밍 언어의 Semantic은 컴파일러/인터프리터 개발자가 언어의 컴파일러나 인터프리터를 개발하기 위하여 참조된다.
프로그램의 개발자와 프로그램 분석가도 Semantic을 참조할 수 있다.
2. AE의 Semantic 정의하기
각 Syntax에 대해 의미를 부여해 보자!
1) 자연어로 정의하기
(1) [rule Num] : n
➡ Calculate n as integer value n
NUM n을 정수값 n으로 계산한다.(2) [rule Add] : e1 + e2
➡ If calculate result of e1 is n1, calculate result of e2 is n2, then e1 + e2 is n1 +z n2
e1의 계산 결과는 정수값 n1으로, e2의 계산 결과는 정수값 n2로 계산한다. e1 + e2는 n1 +z n2로 계산한다.(3) [rule Sub] : e1 - e2
➡If calculate result of e1 is n1, calculate result of e2 is n2, then e1 - e2 is n1 -z n2
e1의 계산 결과는 정수값 n1으로, e2의 계산 결과는 정수값 n2로 계산한다. e1 + e2는 n1 -z n2로 계산한다.
AE semantic에 근거해서, AE 프로그램의 behavior을 이해할 수 있다.
Example)
(3 - 1) + 2
1.(By Rule Num)
3은 정수 3으로 계산된다.
2.(By Rule Num)
1은 정수 1로 계산된다.
3.(By Rule Sub)
3의 계산결과가 정수 3이고, 1의 결과가 정수 1이면 3-1은 2로 계산된다.
4.(By 1,2,3)
3-1는 2이다.
5.(By Rule Num)
2는 정수 2로 계산된다.
6.(By Rule Add)
만약 3-1이 정수 2이고, 2가 정수 2이면, (3-1)+2 는 4로 계산된다.
7.(By 4,5,6)
(3-1)+2 는 4이다.
2) Formal Semantics
~으로 계산된다, ~으로 평가된다는 것을 semantic으로 ⇓으로 표현한다.
그러나 위 역시 완전히 formal한 형태는 아니다!
3) Operational Semantics
Operational Semantics을 이용하여 AE 언어의 Semantic을 더 formal하게 작성해 보자 !
Operational Semantics은 수식을 써서 언어의 semantic을 표현하는 것으로서, 프로그램이 기계에서 어떻게 동작하는지 보여주기 위한 것이다.
Operational Semantics는 ❗❗ Inferenence Rule (추론 규칙) ❗❗에 기반한다.
추론규칙은 전제로부터 결론을 이끌어내는 것이다.
🔔 H1, H2, H3 .. Hn : Premises(전제)
🔔 P : conclusion
➡ 만약 모든 premises가 true라면, conclusion도 true라는 의미이다.
n ⇓ n 의 경우 전제가 없다. 항상 True이다.
📌 전제(premise)가 없는 추론은 'action'이라고 한다.
4) Proof Tree
추론 규칙을 이용하여 Operation Semantic을 정의하면, 이를 기반으로 Proof Tree를 만들 수 있다.
일반적 tree 와 달리 ✔ root node가 가장 밑 ✔ 에 있으며, root node는 'conclusion'이다.
자식 노드가 모두 참이면, 부모 노드도 참이다.
h1, h2가 참이면 h4도 참이다.
h3이 참이면 h6도 참이다.
h4 h5 h6이 참이면 p도 참이다.
🔔 Example : Proof for Evaluation
proof tree를 이용하여 (3 - 1) + 2가 4로 evaluate된다고 증명해 보자.
1)
2)
3)
4)
5)
6)
