Semantic Consistency in Information Exchange

Size: px

Start display at page:

Download "Semantic Consistency in Information Exchange"

승준 심
5 years ago
Views:

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

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

3 3.1 Operational Semantics 숙대창병모 3

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

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

6 언어 S 정수 변수 식 n Int x Var E Exp Stmt S x = E S; S 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 숙대창병모 6

7 기초지식 합집합 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 {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 숙대창병모 7

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

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 숙대창병모 9

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 숙대창병모 10

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마다상태전이규칙정의 프로그램의의미를상태전이과정으로설명한다. 숙대창병모 11

12 추론규칙 추론규칙 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 숙대창병모 12

13 전이규칙 (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 숙대창병모 13

14 전이규칙 (Transition Rule) 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 숙대창병모 14

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} 숙대창병모 15

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 숙대창병모 16

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

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 숙대창병모 18

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

20 3.2 Other Semantics 숙대창병모 20

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 숙대창병모 21

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! } 숙대창병모 22

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 숙대창병모 23

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. 숙대창병모 24

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

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

27 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 언어 S in EBNF 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 숙대창병모 27

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

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

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

31 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 숙대창병모 31

32 심볼테이블 (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 숙대창병모 32

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

34 파서 / 해석기 parse( ) 파서 / 해석기 expr( ) Recursive Descent Parsing 수행각식, 문장에대한하나의해석 ( 실행 ) 함수포함 식을읽고식의값을계산해서리턴한다. 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 34

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

36 문장해석기구조 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

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

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

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

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

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

42 HW #2 언어 S 에대한인터프리터구현 global.h, lex.c, int.c 참고해서작성 순서 global.h 를읽고이해한다. 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 숙대창병모 42

Microsoft PowerPoint - semantics

Microsoft PowerPoint - semantics 제 3 장시맨틱스 (Semantics) Reading Chap 13 숙대창병모 Sep. 2007 1 3.1 Operational Semantics 숙대창병모 Sep. 2007 2 시맨틱스의필요성 프로그램의미의정확한이해 소프트웨어의정확한명세 소프트웨어시스템에대한검증혹은추론 컴파일러혹은해석기작성의기초 숙대창병모 Sep. 2007 3 의미론의종류 Operational