동적 의미론 ① 조작적, 표시적

프로그램의 뜻을 말이 아닌 것으로 적을 수 있을까?

하나로 정해진 것이 없다

뜻을 적는 방법은 셋입니다

프로그램을 실행할 때의 뜻을 다루는 것이 동적 의미론(dynamic semantics)입니다. 구문에는 BNF가 있지만, 뜻을 적는 데는 널리 합의된 표기법이 하나로 정해져 있지 않습니다. 조작적(operational), 표시적(denotational), 공리적(axiomatic) 의미론 세 가지를 봅니다.

왜 적어 두나

뜻을 정확히 적어야 하는 이유

뜻을 체계적으로 적어 두어야 하는 이유는 다섯 가지입니다. 언어를 쓰는 사람과 만드는 사람이 같은 뜻으로 읽어야 하고, 적어 둔 정의가 있어야 그것으로 증명하고, 만들고, 고칠 수 있습니다.

조작적 의미론

실행해서 상태가 바뀌는 것을 봅니다

조작적 의미론(operational semantics)은 프로그램을 기계에서 실행했을 때 기계의 상태가 어떻게 바뀌는지로 뜻을 적습니다. 상태는 변수마다 지금 들어 있는 값입니다. 세 문장을 실행하며 x와 y가 바뀌어 간 과정이 이 프로그램의 뜻입니다.

예시입니다.

어떤 기계에서

단순한 가상 머신을 세웁니다

실제 컴퓨터는 복잡해서 그 위에서 뜻을 설명하기 어렵습니다. 그래서 단순하게 만든 가상 머신(virtual machine)을 씁니다. 번역기가 소스를 그 머신의 명령으로 옮기고, 시뮬레이터가 그 머신을 실행해 봅니다.

가상 머신은 소프트웨어로 흉내 낸 컴퓨터입니다. 조작적 의미론은 직관적이어서 언어 설명서에 자주 쓰입니다.

표시적 의미론

뜻을 수학의 값에 짝지어 줍니다

표시적 의미론(denotational semantics)은 실행 과정을 따라가지 않습니다. 언어의 요소마다 짝이 될 수학의 대상을 정하고, 요소를 그 대상으로 보내는 의미 함수를 정의합니다. 식의 뜻은 정수 하나이거나 error입니다.

식 네 개는 예시입니다. 1970년에 스콧과 스트래치가 제안했고, 셋 가운데 가장 추상적입니다.

상태도 수학으로

문장은 상태를 새 상태로 바꾸는 함수

프로그램 상태(program state)는 모든 변수의 지금 값이고, 이름과 값의 쌍들로 적습니다. 변수의 뜻은 상태에서 찾은 값, 문장의 뜻은 상태를 새 상태로 바꾸는 함수입니다. 반복문의 뜻은 다 돌고 난 뒤의 상태입니다.

값은 예시입니다. VARMAP은 이 강의가 따르는 교재가 쓰는 함수 이름입니다. 엄밀하지만 복잡해서 주로 언어 설계에 쓰입니다.

다음 편

셋째 방법은 프로그램이 맞다는 것을 증명하려고 만든 것입니다

9편프로그램이 맞다고 증명할 수 있을까? 2강 목록