Syntax는 form 형식에 관한 것이고, Semantics는 의미에 관한 것이다.

Motivation

프로그래밍 언어에서 "프로그램이 의미하는 것(what it means)"을 포착하는 건 매우 어렵다.

❓그렇다면 왜 "의미"를 포착하려고 노력하는가?

1. 컴파일러/인터프리터 개발자가 무엇을 해야 하는지 알려주기 위해
2. 우리가 작성한 프로그램을 컴파일러가 제대로 실행했는지 검증하기 위해

Program Verification 프로그램 검증

이 프로그램이 제대로 동작하는지, 사양(specification)에 맞게 작동하는지 수학적으로 증명하는 과정이다.

→ 즉, 이 코드가 '옳은 일(correct job)'을 하는지 판단하는 과정이야.

• 정의된 의미(Semantics)에 따라 프로그램이 올바르게 작동하는지를 수학적으로 증명하는 것을 의미함

💡 머신만으로는 부분적인 semantic만 파악가능하다. (개발자의 의도가 담겨있기에)

⇒ 완전한 의미 파악을 위해서는 인간 + 머신이 요구된다.

📌 프로그램 검증을 시도해볼 가치가 있는 상황 4가지

1. 단순화된 언어 사용하기 ⇒ symbol sentence
2. 정형화된 명세 (formal specification)를 작성하기
3. 그 단순화된 언어의 의미를 수학적으로 정의하기 ⇒ symbol mean을 파악
4. 모든 걸 합쳐서 실제로 프로그램이 옳음을 증명하기

❓ 왜 복잡한 P.L에서는 어려울까?