제3장 시맨틱스(Semantics) Reading Chap 13 © 숙대 창병모

시맨틱스의 필요성 프로그램 의미의 정확한 이해 소프트웨어의 정확한 명세 소프트웨어 시스템에 대한 검증 혹은 추론 컴파일러 혹은 해석기 작성의 기초 © 숙대 창병모

3.1 Operational Semantics © 숙대 창병모

의미론의 종류 Operational Semantics Denotational Semantics 프로그램의 동작 과정을 정의 Denotational Semantics 프로그램의 의미를 함수 형태로 정의 Axiomatic Semantics 프로그램의 시작 상태와 종료 상태를 논리적 선언(assertion) 형태로 정의 © 숙대 창병모

동작 시맨틱스(Operational Semantics) 기본 아이디어 프로그램의 의미를 상태 전이(실행) 과정으로 설명한다. 각 문장 S마다 상태 전이 규칙 정의 예제 read x; y = 1; while (x != 1) do (y = y*x; x = x-1) x 값을 읽는다. { x ↦ n } if READ n y에 1 배정 { x ↦ n, y ↦ 1 } x 값이 1이 아닌지 검사 거짓이면 종료 참이면 y 값을 x 값과 현재 y 값의 곱으로 변경 { x ↦ n, y ↦1*n } x 값 1 감소 { x ↦ n-1, y ↦ n } 3 번부터 반복 © 숙대 창병모

언어 S 정수 변수 식 Stmt S  x = E | S; S n  Int | if E then S | if E then S else S | while E do S | read x | print E Expr E  n | x | true | false | E + E | E – E | E * E | E / E | E == E | E < E | E > E | !E Prgm P  S 정수 n  Int 변수 x  Var 식 E  Exp © 숙대 창병모

기초 지식 합집합 곱집합 함수집합 함수 f ∈A → B 함수 수정 f[a ↦b] A + B = { a | a ∈ A ∨ a ∈ B} 곱집합 A x B = {(a,b)| a ∈A ∧ b∈B} 함수집합 A → B = {f | f : A → B} 함수 f ∈A → B {a1↦b1, a2↦b2, …, an↦bn} 함수 수정 f[a ↦b] f[a ↦ b](x) = { b if x = a f(x) otherwise © 숙대 창병모

변수 및 상태 [23 + 5] vs [x + y] [x + y]의 의미는 ? 변수 x, y의 현재 값에 따라 다르다. 변수들의 현재 값을 무엇이라고 할까요? 상태(State) also called Environment © 숙대 창병모

상태(State) 상태(A state) 변수들의 현재 값 하나의 함수로 생각할 수 있다. s  Var  Int 모든 상태들의 집합 State = Var  Int 상태 s에서 변수 값 s(x) 상태 갱신: s’ = s[y ↦ v] s’ (x) = { s(x) if x != y v if x = y © 숙대 창병모

수식의 의미 수식 E의 의미 상태 s에서 수식 E의 의미 상태 s에서 수식 E의 값 [E]s s = {x ↦1, y ↦ 3} [x+y]s = 4 상태 s에서 수식 E의 의미 [true]s = T [false]s = F [n]s = n [x]s = s(x) [E1 + E2]s = [E1]s + [E2]s [E1 == E2]s = T if [E1]s == [E2]s F otherwise … © 숙대 창병모

문장의 의미 문장 S의 의미 문장 S가 상태 s를 s’으로 변경시킨다. 상태 전이(state transition)라고 한다. (s, S)  s’ where s is the initial state S is a statement s’ is the final state 동작 시맨틱스 각 문장 S마다 상태 전이 규칙 정의 프로그램의 의미를 상태 전이 과정으로 설명한다. s S s’ © 숙대 창병모

추론 규칙 추론 규칙 p -> q p q 조상 추론 규칙 X parent Y X parent Y ∧ Y ancestor Z X ancestor Y X ancestor Z a parent b b parent c © 숙대 창병모

전이 규칙(Transition Rule) assignment (s, id = E)  s[id ↦ [E]s] sequence (s, S1)  s’, (s’, S2)  s” (s, S1; S2)  s” s S1 s’ S2 s” © 숙대 창병모

전이 규칙(Transition Rule) if-then-else (s, S1)  s’ (s, if E then S1 else S2)  s’ (s, S2)  s’ if [E]s = T if [E]s = F s E F T S1 S2 s’ s’ © 숙대 창병모 14

예1 x = 1; y = 2; if x > y then max =x; else max =y; s0 = { } (s0, x = 1)  s1 s1 = {x ↦ 1} (s1, y = 2)  s2 s2 = {x ↦ 1, y ↦ 2} (s2, if x >y …)  s3 [x>y] s2= F (s2, max=y)  s3 s3 = {x ↦ 1, y ↦ 2, max ↦ 2} © 숙대 창병모

전이 규칙 while (s, S)  s’, (s’, while E do S)  s” if [E]s = T if [E]s = F s” s s’ S S . . . S © 숙대 창병모

전이 규칙 read print READ n (s, read id)  s[id ↦ n] PRINT [E]s (s, print E)  s © 숙대 창병모 17

예2 read x; y = 1; while (x != 1) do (y = y*x; x = x-1) s0 = { } (s0, read x)  s1 s1 = {x ↦ 3} (s1, y = 1)  s2 s2 = {x ↦ 3, y ↦ 1} (s2, while …)  s” [x != 1]s2= T (s2, y =x*y; x = x-1)  s3 s3 = {x ↦ 2, y ↦ 3} (s3, while …)  s” [x != 1]s3= T (s3, y =x*y; x = x-1)  s4 s4 = {x ↦ 1, y ↦ 6} (s4, while …)  s” [x !=1]s4 = F s” = s4 © 숙대 창병모

지금까지 한 것/앞으로 할 것! Topic Logic Implementation ------------------------------------------------ Syntax Grammar Parser Semantics Semantics rules Interpreter Type Typing rules Type checker © 숙대 창병모

3.2 Other Semantics © 숙대 창병모

Axiomatic Semantics read x; y = 1; while (x != 1) do (y = x*y; x = x-1) If x = n holds before the program is executed then y = n! will hold when the execution terminates. Properties of programs are specified as assertions { P } S { Q } where S is a statement P is the precondition and Q is the postcondition © 숙대 창병모

Pre- and post conditions 예제 read x; { x=n } y =1; { x=n and y=1} while (x !=1) do (y =x *y; x = x-1) { x=1 and y=n! } © 숙대 창병모

Denotational Semantics Describe meaning of programs by mathematical Function from states to states for each statement Operational semantics (s, S)  s’ for each statement S Denotational semantics s’ = f(s, S) for each statement S © 숙대 창병모

Denotational Semantics read x; y = 1; while (x != 1) do (y = y*x; x = x-1) The program’s computation is a function from states to states: The final state will be equal to the initial state except that the value of x = 1 and the value of y = the factorial of the value of x in the initial state. © 숙대 창병모

3.3 Interpreter for Lang. S © 숙대 창병모

언어 S의 인터프리터 언어 S의 인터프리터 구현 구성 요소 동작 시맨틱스(Operational Semantics)에 따라 구현 Recursive Descent Parsing 방식을 확장해서 구현 구성 요소 어휘 분석(lexical analyzer) 심볼 테이블(Symbol table) 변수들의 상태(state) 파서(parser) 각 식, 문장에 대한 해석(실행) 함수 © 숙대 창병모

언어 S in EBNF Stmt S  id = E | (S {; S}) | if E then S end | if E then S else S | while E do S | read id | print E Expr E  true | false | AE | AE == AE | AE != AE | AE < AE | AE > AE | !E Aexpr AE  T {+T | -T} Term T  F {*F | /F} Factor F  n | id | (AE) Prgm P  S © 숙대 창병모

언어 S 인터프리터 기본원리 어휘분석 심볼 테이블(Symbol table) 파서(parser) 메모리에서 S 프로그램을 Recursive Descent Parsing 스타일로 한 문장씩 읽은 후 해석하여 실행한다. 어휘분석 getToken( ) 메모리에서 S 프로그램을 읽어서 토큰들로 분리해서 리턴 Chapter 2 of Aho, Sethi, and Ullman, Compilers: Dragon Book 심볼 테이블(Symbol table) 심볼 테이블에 상태(변수들의 값)을 저장한다. 파서(parser) Recursive Descent Parsing 스타일로 읽으면서 각 식, 문장에 대한 해석(실행) 함수 수행 © 숙대 창병모

S 인터프리터 전체 구성 M[ ] lex.c int.c symtable[ ] init() getToken() factor() { … token = getToken() …} term() { } expr() { } stmt() { } parse() { } © 숙대 창병모

자료 구조 M[] symtable[] 입력 S 프로그램 저장을 위한 배열 M[] pc M[]의 인덱스 변수 이름과 그 값을 저장하기 위한 자료구조 스택 형태로 구현 © 숙대 창병모

어휘 분석 getToken() 토큰의 종류 M[]에 저장된 S 프로그램을 읽어서 호출될 때마다 하나의 토큰을 반환한다. 키워드, 수, 변수 이름, 기타 문자 처리하도록 확장 토큰의 종류 keyword: if return IF; … keyword: print return PRINT number return NUM; tokenval = val of the number identifier return ID; tokenval = i such that symtable[i] contains the name other char c return c; tokenval = NONE © 숙대 창병모

심볼 테이블 심볼 테이블(Symbol Table) 코드 식별자(변수 이름)과 그 값을 저장하기 위한 자료구조 변수 이름, 토큰 번호, 값 저장 코드 struct entry { char *lexptr; int token; int val; } struct entry symtable[ ] int lookup(char[] s) return position of entry for s int push(char[] s, int tok) push s and return top position © 숙대 창병모

심볼 테이블 symtable[] ( x = 1; y = 2; if x > y then max =x else max =y ) symtable[] token val lexptr 2 lastentry ID ID 2 ID 1 … lastchar lexemes[] x \0 y \0 max \0 © 숙대 창병모

파서/해석기 expr( ) stmt( ) parse( ) 파서/해석기 식을 읽고 식의 값을 계산해서 리턴한다. Recursive Descent Parsing 수행 각 식, 문장에 대한 하나의 해석(실행) 함수 포함 expr( ) 식을 읽고 식의 값을 계산해서 리턴한다. stmt( ) 문장을 읽고 문장에 따라 해석하여 실행한다. Stmt S  id = E | (S {; S}) | if E then S end | if E then S else S | while E do S | read id | print E © 숙대 창병모

수식 해석 expr() 변수를 포함한 수식 값을 계산하도록 HW#1 확장 변수 값은 symtable[]에 저장되어 있음 실행 과정 1. expr( ) E을 읽으면서 값을 계산한다. 2. term( ) 3. factor( ) 3.1 getToken()은 변수 이름 x를 만나면 symtable[]에서 해당 위치를 lookup()해서 찾아 준다. loc = tokenval; 3.2 symtable[loc].val에 저장되어 있는 값을 사용하여 계산한다. © 숙대 창병모

문장 해석기 구조 void stmt( ) { int loc, result, whilestart; switch(token) { // S  id = E case ID: loc = tokenval; // symtable[] 내의 저장 위치 match(ID); if (token == ‘=‘) { match(‘=‘); result = expr( ); symtable[loc].val = result; } break; case ‘(‘: // S  ( S {;S} ) case IF: // S  if E then S else S | if E then S end case WHILE: // S  while E do S case READ: // S  read id case PRINT: // S  print E

대입문 해석 대입문 id = E E 값을 symtable[] 내의 변수 id에 저장 실행 과정 1. getToken()은 변수 id를 읽으면 symtable[] 내의 해당 위치를 찾아 tokenval에 저장해 둔다. loc = tokenval; 2. E을 읽으면서 값을 계산한다. 3. 계산된 E 값을 symtable[loc].val에 저장한다. © 숙대 창병모

read 문 해석 read 문 read id 입력 값을 symtable[] 내의 변수 id에 저장 실행 과정 1. match(READ) getToken()은 변수 id를 읽으면 symtable[] 내의 해당 위치를 찾아 tokenval에 저장해 둔다. loc = tokenval; 2. 입력 값을 받는다. 3. 입력 값을 symtable[loc].val에 저장한다. © 숙대 창병모

print 문 해석 print 문 print E E 값을 출력한다. 실행 과정 1. match(PRINT) 2. expr() : E을 읽으면서 값을 계산한다. 3. 계산된 값을 프린트한다. © 숙대 창병모

조건문 해석 조건문 if E then S1 else S2 한 stmt 건너 뛰기 E 값에 따라 S1 혹은 S2 실행 실행 과정 1. expr(): E을 읽으면서 값을 계산한다. 2. E 값이 true 이면 S1를 읽고 실행하고 S2는 건너 뛴다. 3. E 값이 false 이면 S1를 건너 뛰고 S2를 읽어서 실행한다. 한 stmt 건너 뛰기 matchstmt() © 숙대 창병모

반복문 해석 반복문 while E do S E와 S를 반복적으로 읽으면서 해석한다. 실행 과정 whilestart = pc; 2. expr(): E을 읽으면서 값을 계산한다. 3. E 값이 true 이면 S를 읽고 실행하고 저장된 시작위치로 돌아가서 2부터 반복 pc = whilestart; token = getToken(); 4. E 값이 false 이면 S를 건너뛰고 진행한다. match(DO); matchstmt(); © 숙대 창병모

HW #2 언어 S에 대한 인터프리터 구현 global.h, lex.c, int.c 참고해서 작성 순서 getToken() 을 읽고 이해한다. expr() 을 완성한다. stmt() 을 완성한다. S  (S; S) | read id | print E | if E then S end | if E then S else S | while E do S © 숙대 창병모