Microsoft PowerPoint - semantics

Size: px

Start display at page:

Download "Microsoft PowerPoint - semantics"

숙희 서
4 years ago
Views:

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

2 3.1 Operational Semantics 숙대창병모 Sep

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

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

5 동작시맨틱스 (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

6 언어 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

7 기초지식 합집합 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

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

9 상태 (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

10 수식의의미 수식 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

11 문장의의미 문장 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

12 추론규칙 조상추론규칙 X parent Y X ancestor Y Y parent Z X ancestor Y X ancestor Z a parent b b parent c 숙대창병모 Sep

13 전이규칙 (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

14 전이규칙 (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

15 예 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

16 전이규칙 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

17 전이규칙 read READ n (s, read x) s[x n] print PRINT [E]s (s, print E) s 숙대창병모 Sep

18 예 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

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

20 3.2 Axiomatic Semantics 숙대창병모 Sep

21 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

22 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

23 3.3 Denotational Semantics 숙대창병모 Sep

24 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

25 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

26 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

27 Expressions Syntax D 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

28 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

29 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

30 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

31 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

32 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

33 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

34 3.4 Interpreter for Lang. S 숙대창병모 Sep

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

36 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

37 언어 S 인터프리터 기본원리 Recursive Descent Parsing 스타일로진행하면서 한문장씩읽어서해석한다. 어휘분석 HW#2 확장해서구현 gettoken( ) 입력프로그램을토큰들로분리해서리턴 변수들의상태 (state) Symbol table 에변수상태저장 각식, 문장에대한해석 ( 실행 ) 함수 각식, 문장마다하나의해석 ( 실행 ) 함수작성 while 문처리 메모리에입력프로그램저장후 반복적으로읽으면서해석해야한다. 숙대창병모 Sep

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

39 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

40 심볼테이블 심볼테이블 식별자 ( 변수이름 ) 을저장하기위한자료구조 변수이름, 토큰번호, 값저장 코드 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

41 심볼테이블 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

42 수식해석 수식 E 변수를포함한수식값을계산하도록 HW#2 확장 변수값은 symtable[] 에저장되어있음 실행과정 1. E을읽으면서값을계산한다. 2. 변수이름 x를만나면symtable[] 에서해당위치를 lookup() 해서찾고저장되어있는값을사용한다. 숙대창병모 Sep

43 문장해석기구조 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: } }

44 대입문해석 대입문 x = E E 값을 symtable[] 내의변수 x 에저장 실행과정 1. 변수이름 x를읽으면symtable[] 내의해당위치를 lookup() 해서찾는다. 2. E을읽으면서값을계산한다. 3. 계산된 E 값을 symtable[i].val에저장한다. 숙대창병모 Sep

45 조건문해석 조건문 if E then S1 else S2 E 값에따라 S1 혹은 S2 실행실행과정 1. E을읽으면서값을계산한다. 2. E 값이 true 이면 S1를읽고실행한다. 3. E 값이 false 이면 S1를건너뛰고S2를읽어서실행한다. 숙대창병모 Sep

46 반복문해석 반복문 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

47 HW #3 언어 S에대한인터프리터구현 global.h, lex.c, cal.c 참고해서작성 숙대창병모 Sep

Semantic Consistency in Information Exchange

Semantic Consistency in Information Exchange 제 3 장시맨틱스 (Semantics) Reading Chap 13 숙대창병모 1 시맨틱스의필요성 프로그램의미의정확한이해 소프트웨어의정확한명세 소프트웨어시스템에대한검증혹은추론 컴파일러혹은해석기작성의기초 숙대창병모 2 3.1 Operational Semantics 숙대창병모 3 의미론의종류 Operational Semantics 프로그램의동작과정을정의 Denotational