제 3 장시맨틱스 (Semantics) Reading Chap 13 숙대창병모 Sep. 2007 1
3.1 Operational Semantics 숙대창병모 Sep. 2007 2
시맨틱스의필요성 프로그램의미의정확한이해 소프트웨어의정확한명세 소프트웨어시스템에대한검증혹은추론 컴파일러혹은해석기작성의기초 숙대창병모 Sep. 2007 3
의미론의종류 Operational Semantics 프로그램의동작과정을정의 Denotational Semantics 프로그램의의미를함수형태로정의 Axiomatic Semantics 프로그램의시작상태와종료상태를논리적선언 (assertion) 형태로정의 숙대창병모 Sep. 2007 4
동작시맨틱스 (Operational Semantics) 기본아이디어 프로그램의의미 ( 실행 ) 를상태전이과정으로설명한다. 각문장S마다상태전이규칙정의 예제 read x; y = 1; while (x!= 1) do (y = y*x; x = x-1) 1. x 값을읽는다. 2. y에 1 배정 3. x 값이 1이아닌지검사 4. 거짓이면종료 5. 참이면 y 값을 x 값과현재 y 값의곱으로변경 6. x 값 1 감소 7. 3 번부터반복 숙대창병모 Sep. 2007 5
언어 S Stmt S x = E 정수 n Int S; S 변수 if E then S x Var if E then S else S 식 while E do S E Exp 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 숙대창병모 Sep. 2007 6
기초지식 합집합 A + B = { a a A a B} 곱집합 A x B = {(a,b) a A b B} 함수집합 A B = {f f : A B} = {f f A B} 함수 f A B {a 1 b 1, a 2 b 2,, a n b n } 함수수정 f[a b] f[a b](x) = { b f(x) if x = a otherwise 숙대창병모 Sep. 2007 7
변수및상태 [23 + 5] vs [x + y] [x + y] 의의미는? 변수 x, y 의현재값에따라다르다. 변수들의현재값을무엇이라고할까요? 상태 (State) 숙대창병모 Sep. 2007 8
상태 (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 숙대창병모 Sep. 2007 9
수식의의미 수식 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 숙대창병모 Sep. 2007 10
문장의의미 문장 S의의미 문장 S가상태s를 s 으로변경시킨다. 상태전이 (state transition) 라고한다. (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마다상태전이규칙정의 프로그램의의미를상태전이과정으로설명한다. 숙대창병모 Sep. 2007 11
추론규칙 조상추론규칙 X parent Y X ancestor Y Y parent Z X ancestor Y X ancestor Z a parent b b parent c 숙대창병모 Sep. 2007 12
전이규칙 (Transition Relation) assignment (s, x = E) s[x [E]s] sequence (s, S1) s, (s, S2) s (s, S1; S2) s s S1 s S2 s 숙대창병모 Sep. 2007 13
전이규칙 (Transition Relation) if-then-else (s, S1) s (s, if E then S1 else S2) s if [E]s = T s (s, S2) s (s, if E then S1 else S2) s if [E]s = F E F T s S1 S2 s 숙대창병모 Sep. 2007 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} 숙대창병모 Sep. 2007 15
전이규칙 while (s, S) s, (s, while E do S) s if [E]s = T (s, while E do S) s (s, while E do S) s if [E]s = F s s s S S... S 숙대창병모 Sep. 2007 16
전이규칙 read READ n (s, read x) s[x n] print PRINT [E]s (s, print E) s 숙대창병모 Sep. 2007 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 숙대창병모 Sep. 2007 18
지금까지한것 / 앞으로할것! Topic Logic Implementation ------------------------------------------------ Syntax Grammar Parser Semantics Semantics rules Interpreter Type Typing rules Type checker 숙대창병모 Sep. 2007 19
3.2 Axiomatic Semantics 숙대창병모 Sep. 2007 20
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 숙대창병모 Sep. 2007 21
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! } 숙대창병모 Sep. 2007 22
3.3 Denotational Semantics 숙대창병모 Sep. 2007 23
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 숙대창병모 Sep. 2007 24
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. 숙대창병모 Sep. 2007 25
Trivial Example: Binary Numbers Syntax B 0 1 N B NB E N E+E Semantics value function V : Exp Int V [ 0 ] = 0 V [ 1 ] = 1 V [ NB ] = 2*V[ N ] + V[ B ] V [ E 1 +E 2 ] = V[ E 1 ] + V[ E 2 ] 숙대창병모 Sep. 2007 26
Expressions Syntax D 0 1 2 9 N D ND E x n E + E Semantics value function V : Exp x State Int state s : Var Int V [ x ] s = s(x) V [ 0 ] s = 0 V [ 1 ] s = 1 V [ ND ] s = 10 * V [ N ] s + V [ D ] s V [ E 1 + E 2 ] s = V [ E 1 ] s + V [ E 2 ] s 숙대창병모 Sep. 2007 27
Semantics of Lang. S Syntax S x=e if B then S else S S;S while B do S Semantics C : Statements (State State) s = C(S, s) = C[S] s for each statement S A function for each statement S that returns the post state from the pre state 숙대창병모 Sep. 2007 28
Semantics of Assignment C[ x = E ] is a function : State State C[ x = E ] s = s where s : Var Int s = s[x V[E]s] 숙대창병모 Sep. 2007 29
Semantics of Conditional C[ if E then S1 else S2 ] is a function : State State C[ if E then S1 else S2 ] s = C[ S1 ] s if V[ E ] s is true C[ S2 ] s if V[ E ] s is false 숙대창병모 Sep. 2007 30
Semantics of Iteration C[ while E do S ] is a function : State State C[ while E do S ] = the function f such that f(s) = s if V [ E ]s is false f(s) = f( C[ S ] s ) if V [ E ]s is true f(s) = f(s 1 ) s 1 = C[ S ] s if V[E]s is true f(s 1 ) = f(s 2 ) s 2 = C[ S ] s 1 if V[E] s 1 is true f(s n ) = s n if V[E] s n is false 숙대창병모 Sep. 2007 31
Semantics of Compound Statement Compositionality The meaning of a compound program is defined from the meanings of its parts. C[ S1;S2 ] is a composition of two functions C[ S1;S2 ] s = C[ S2 ] C[ S1 ] s 숙대창병모 Sep. 2007 32
Perspective Denotational semantics Assign mathematical meanings to programs in a structured, principled way Imperative programs define mathematical functions Impact Influential theory Applications via abstract interpretation, type theory, static analysis 숙대창병모 Sep. 2007 33
3.4 Interpreter for Lang. S 숙대창병모 Sep. 2007 34
언어 S 의인터프리터 언어 S 의인터프리터구현 구성요소 동작시맨틱스 (Operational Semantics) 에따라구현 Recursive Descent Parsing 방식을확장해서구현 어휘분석 (lexical analyzer) 변수들의상태 (state) 각식, 문장에대한해석 ( 실행 ) 함수 숙대창병모 Sep. 2007 35
Stmt S x = E (S {; S}) if E then S else S while E do S read x print E 언어 S in EBNF Expr E true false T {+T -T} T == T T!= T T < T T > T!E Term T F {*F /F} Factor F n x (E) Prgm P S 숙대창병모 Sep. 2007 36
언어 S 인터프리터 기본원리 Recursive Descent Parsing 스타일로진행하면서 한문장씩읽어서해석한다. 어휘분석 HW#2 확장해서구현 gettoken( ) 입력프로그램을토큰들로분리해서리턴 변수들의상태 (state) Symbol table 에변수상태저장 각식, 문장에대한해석 ( 실행 ) 함수 각식, 문장마다하나의해석 ( 실행 ) 함수작성 while 문처리 메모리에입력프로그램저장후 반복적으로읽으면서해석해야한다. 숙대창병모 Sep. 2007 37
자료구조 M[] 입력프로그램저장을위한배열 M[] i M[] 의인덱스 symtable[] 변수이름과그값을저장하기위한심볼테이블스택형태로구현 숙대창병모 Sep. 2007 38
gettoken() 어휘분석 Lexical Analyzer로 M[] 에저장된입력프로그램을읽어서토큰을반환한다. 키워드, 수, 변수이름, 기타문자처리하도록확장 토큰의종류 keyword: if return IF; keyword: print return PRINT number return NUM; tokenval = val of the number name return ID; tokenval = i such that symtable[i] contains the name other char c return c; tokenval = NONE 숙대창병모 Sep. 2007 39
심볼테이블 심볼테이블 식별자 ( 변수이름 ) 을저장하기위한자료구조 변수이름, 토큰번호, 값저장 코드 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 숙대창병모 Sep. 2007 40
심볼테이블 symtable[] token val lexptr x = 1; y = 2; if x > y then max =x; else max =y; lastentry ID 2 ID 2 ID 1 lastchar lexemes[] x \0 y \0 max \0 숙대창병모 Sep. 2007 41
수식해석 수식 E 변수를포함한수식값을계산하도록 HW#2 확장 변수값은 symtable[] 에저장되어있음 실행과정 1. E을읽으면서값을계산한다. 2. 변수이름 x를만나면symtable[] 에서해당위치를 lookup() 해서찾고저장되어있는값을사용한다. 숙대창병모 Sep. 2007 42
문장해석기구조 void stmt( ) { int loc, result; switch(token) { case ID: loc = tokenval; match(id); if (token == = ) { match( = ); result = expr( ); symtable[loc].val = result; } break; case ( : case IF: case WHILE: case READ: case PRINT: } }
대입문해석 대입문 x = E E 값을 symtable[] 내의변수 x 에저장 실행과정 1. 변수이름 x를읽으면symtable[] 내의해당위치를 lookup() 해서찾는다. 2. E을읽으면서값을계산한다. 3. 계산된 E 값을 symtable[i].val에저장한다. 숙대창병모 Sep. 2007 44
조건문해석 조건문 if E then S1 else S2 E 값에따라 S1 혹은 S2 실행실행과정 1. E을읽으면서값을계산한다. 2. E 값이 true 이면 S1를읽고실행한다. 3. E 값이 false 이면 S1를건너뛰고S2를읽어서실행한다. 숙대창병모 Sep. 2007 45
반복문해석 반복문 while E do S E와 S를반복적으로읽으면서해석 Stack W[] 이용해서구현 실행과정 1. while 문을처음만나면시작위치, 끝위치를W[] 스택에 push() ( 위치는 M[] 의인덱스i) 2. E을읽으면서값을계산한다. 3. E 값이 true 이면 S를읽고실행한다. 스택 W[] 에저장된시작위치로돌아가서 2부터반복 4. E 값이 false 이면스택을 pop() 하고스택에저장된끝위치로가서진행한다. 숙대창병모 Sep. 2007 46
HW #3 언어 S에대한인터프리터구현 global.h, lex.c, cal.c 참고해서작성 숙대창병모 Sep. 2007 47