5.1 데이터 타입 개요 5.2 사례 연구 5.3 타입 검사 Reading Chap 6 제 5 장 데이터 타입 5.1 데이터 타입 개요 5.2 사례 연구 5.3 타입 검사 Reading Chap 6 ©숙대 창병모

5.1 데이터 타입 개요 ©숙대 창병모

기본 타입: 예 사전 정의된 기본 타입 나열 타입 부분범위 타입(Ada, Pascal) boolean, char, int, float, double, … 나열 타입 enum Color {Red, Green, Blue} 부분범위 타입(Ada, Pascal) type digit is range 0 .. 9; 부분범위 타입 없음(C, C++, Java) byte digit; // -128 .. 127 if (digit >9 || digit < 0) throw new DigitException(); © 숙대 창병모

데이터 타입의 의미 다음 선언을 생각해보자 이 변수 선언에서 데이터 타입의 의미는? int x; 그 타입의 변수가 가질 수 있는 값들의 집합 A data type is a set of values. 따라서 위 선언의 의미는 x  Integer © 숙대 창병모

데이터 타입의 의미 데이터 타입의 의미 정의 2 A data type is a set of values + 그 값에 적용 가능한 연산들의 모음(a set of operations) 정의 2 A data type is a set of values + a set of operations on those values. 데이터 타입의 수학적 의미 an algebra (S, Op) where S is a set of values Op is a set of operations on S © 숙대 창병모

타입 구성자란 무엇인가? 기본 타입으로부터 더 복잡한 타입을 구성하는 방법 사용자-정의 타입 Array type Record type Union type Set type Pointer type 사용자-정의 타입 © 숙대 창병모

구조체(레코드) 타입 C의 예 Ada의 예 struct IntCharReal { int i; char c; float r; } type IntCharReal is record i: integer; c: character; r: float; end record; © 숙대 창병모

구조체(레코드) 타입 타입 구성자 struct, record C++의 struct 혹은 class int, char, float로부터 새로운 타입 IntCharReal를 정의한다. struct in C record in Pascal, Ada, ... C++의 struct 혹은 class C의 struct를 확장 데이터뿐 아니라 연산(함수)들을 포함하도록 © 숙대 창병모

배열 타입 C의 배열 선언 Java 배열 크기가 정적 결정 int A[10]; int B[] = {1,2,3,4} 배열 크기 동적 결정 배열 크기가 배열의 일부 int x[]; x = new int[10]; © 숙대 창병모

포인터 타입 지금까지 location(address)을 value로 사용할 수 없었다! C 언어 location(pointer)도 하나의 값처럼 사용할 수 있다. 포인터 변수 선언 S  … | t *x; | t *x = E; 포인터 관련 식 E  … | malloc(E) E 값 크기의 메모리 할당 및 pointer 반환 | &y 변수 x의 pointer | *x 변수 x에 저장된 pointer 참조(따라가기) © 숙대 창병모

예 질문 int *x의 의미는 무엇인가? x가 가질 수 있는 값은 ? *x는 무엇인가 ? 포인터 타입의 의미는 ? { int *x = malloc(4); { int y = 10; *x = y; *x = *x / 2; print *x; x = &y; print *x } 질문 int *x의 의미는 무엇인가? x가 가질 수 있는 값은 ? *x는 무엇인가 ? 포인터 타입의 의미는 ? 지정된 타입의 모든 가능한 주소들의 집합 © 숙대 창병모

순환 타입(Recursive Type) 타입 정의에 자신의 이름을 사용하는 경우 예 이 정의의 문제는 무엇인가? struct CharList { char data; struct CharList next; /* C에서 위법 */ }; 이 정의의 문제는 무엇인가? © 숙대 창병모

C 언어의 순환 타입 포인터는 순환 타입 정의에 유용하다. 예 struct CharListNode { char data; struct CharListNode* next; /* legal in C */ }; typedef struct CharListNode* CharList; © 숙대 창병모

5.2 사례 연구 ©숙대 창병모

C Types Basic Derived void Numeric pointer array function struct union Integral char, int, short, long enum Floating float, double, long double Derived pointer array function struct union © 숙대 창병모

Java Types Primitive boolean Numeric Reference array class interface Integral byte, char, short, int, long Floating float, double Reference array class interface © 숙대 창병모

5.3 타입 검사(Type Checking) ©숙대 창병모

타입 검사 왜 필요한가? 문법에는 맞지만 제대로 실행될 수 없는 프로그램들이 많다! 겉모양은 맞지만 속내용이 잘못되어 제대로 실행될 수 없는 프로그램 속내용이 어떻게 잘못되어 있는가 ? 여러 종류의 잘못이 있겠지만 여기에서 다룰 내용은 데이터 타입이 잘못 사용되는 것(type error) 타입 오류(type error) ? 프로그램이 실행 중에 함수 혹은 데이터가 타입에 맞지 않게 잘못 사용되는 것. © 숙대 창병모

타입 오류 let int x = 1 in x = ! x + 2 end let int x = 1, bool y = true in x = x + y if (…) then x = x + 1 else x = x + y let fun int f(int x): x = x + 1 in f = f + 1 © 숙대 창병모

질문 프로그램이 잘못되었는지 어떻게 결정할 수 있나요? 완전하지는 않지만 타입 정보를 이용해서 결정할 수 있다. 이것이 바로 타입 검사(Type Checking) © 숙대 창병모

프로그램 오류 검증 모든 프로그램들 문법에 맞는 프로그램들 실행 중 타입오류가 없는 프로그램들 정적 타입 검사된 프로그램들 © 숙대 창병모

오류 검증 기술 구문 검사(syntax analysis) 타입 검사(type checking) 프로그램이 구문법(syntax grammar)에 맞는지 검사 1세대 기술로 1970년대에 활발히 연구 개발되었다. 모든 언어에 적용되고 있다. 타입 검사(type checking) 프로그램에서 타입이 올바르게 사용되고 있는지 검사 2세대 기술로 1990년대부터 활발히 연구 개발되었다. 안전한 타입 시스템을 갖춘 언어 ML, Haskell, Smalltalk, Java 정형 검증 기술(formal verification) 정적 분석(static analysis), 정형 검증등을 활용하여 프로그램을 검증하는 3세대 기술로 현재 활발히 연구되고 있다. © 숙대 창병모

타입 검사가 왜 필요한가? 프로그램의 안전한(safe) 실행 타입 검사란 무엇인가? 실행 중에 타입오류로 갑자기 죽는 프로그램을 미리 예방해야 한다. 엄격한 타입 검사는 실행시간 타입 오류를 미리 예방할 수 있다. 타입 검사란 무엇인가? 프로그램에서 타입이 올바르게 사용되고 있는지 검사 프로그램에서 타입에 맞지 않는 계산이 실행 중에 발생할지 미리 검사 정적 타입 검사(static type checking) 실행 전에 타입 오류 미리 검사 컴파일 시간에 타입 오류를 미리 검출할 수 있다. 프로그램 안전성을 위해 매우 중요하다 ! © 숙대 창병모

타입 검사 개요 정적 타입 검사(Static Type Checking) 동적 타입 검사(Dynamically typed) 거의 모든 타입 검사를 컴파일 시간에 한다 Java, Pascal, C++, ML, Haskell 엄격 타입(strongly typed) 언어라고 함 동적 타입 검사(Dynamically typed) 실행 시간에 타입 검사 Lisp, Scheme 타입 검사 안 함 어떤 종류의 타입 검사도 하지 않음(어셈블리어) © 숙대 창병모

타입 및 타입 검사 프로그래머는 식별자의 타입을 선언한다 타입 추론(type inference) 각 식(expression)의 타입을 추론한다. 타입 검사(type checking) 프로그램에서 타입이 올바르게 사용되고 있는지 검사한다. © 숙대 창병모

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

타입 규칙(Typing Rule) 타입 검사에 사용되는 규칙 논리적 추론 규칙(logical inference rule) “If this expression has this type and that expression has the other type, then this third expression must have another type.” “if X and Y then Z” © 숙대 창병모

영어를 타입 규칙으로 표현 Read “x : T” as “x has type T”. 규칙 예 If e1 has type Int and e2 has type Int, then e1 + e2 has type Int (e1 has type Int  e2 has type Int)  e1 + e2 has type Int (e1 : Int  e2 : Int)  e1 + e2 : Int © 숙대 창병모

영어를 타입 규칙으로 표현 추론 규칙 예 일반적 형태 추론 규칙 Hypothesis1 … Hypothesisn (e1 : Int  e2 : Int)  e1+ e2 : Int 일반적 형태 Hypothesis1  …  Hypothesisn  Conclusion 추론 규칙 Hypothesis1 … Hypothesisn Conclusion © 숙대 창병모

타입 규칙 예 정수와 + 식에 대한 타입 규칙: ⊢ n : int ⊢ e1:int ⊢ e2:int ⊢ e1 + e2:int 식 2 + 5의 타입은 ? ⊢ 2:int ⊢ 5:int ⊢ 2 + 5:int 그런데 x+y의 타입은 ? 변수 x와 y의 타입에 따라 다르다! 유효한 변수의 타입을 유지하는 타입 환경(type env)가 필요하다! © 숙대 창병모

타입 규칙 예 Type environment 각 지점에서 유효한 변수들의 타입 정보를 유지한다. T: Var → Type Example: T = {x ↦ int, y ↦ int} 변수 x의 타입은 ? T(x) = t T ⊢ x : t 식 x + y의 타입은 ? T ⊢ x : int T ⊢ y : int T ⊢ x+y : int © 숙대 창병모

타입 규칙의 의미 ⊢는 타입 규칙에 의해서 “증명 가능함”을 의미한다. 안전한(safe) 타입 시스템 ⊢ e : t이면 실제 실행에서 e의 계산된 값이 t 타입이다. If ⊢ e : t and e → v, then v : t © 숙대 창병모

언어 S Stmt S  x = E | S1; S2 | if E then S1 else S2 | while E do S | read x | print E | let t x = e in S end | let fun t f(t x) = S1 in S2 end | return E Expr E  n | x | true | false | f(E) | E + E | E – E | E * E | E / E | E == E | E < E | E > E | !E © 숙대 창병모

타입 규칙: 상수/변수 상수를 위한 규칙 변수를 위한 규칙 T ⊢ n:int T ⊢ true:bool T ⊢ false:bool 변수를 위한 규칙 T(x) = t T ⊢ x : t © 숙대 창병모

타입 규칙: 식/대입문 식을 위한 규칙 T ⊢ E1:int T ⊢ E2:int T ⊢ E1:t T ⊢ E2:t T ⊢ E1 + E2:int T ⊢ E1 == E2 : bool 대입문을 위한 규칙 T ⊢ x:t T ⊢ E:t T ⊢ x = E:void © 숙대 창병모

타입 규칙: 복합문/조건문 T ⊢ S1:void T ⊢ S2:t 복합문을 위한 규칙 조건문를 위한 규칙 T ⊢ S1; S2:t T ⊢ E:bool T ⊢ S1:t T ⊢ S2:t T ⊢ if E then S1 else S2:t © 숙대 창병모

타입 규칙: 반복문/입출력 반복문을 위한 규칙 입출력을 위한 규칙 T ⊢ E:bool T ⊢ S:void T ⊢ while E do S:void 입출력을 위한 규칙 T ⊢ x:t T ⊢ E:t T ⊢ read x:void T ⊢ print E:void © 숙대 창병모

타입 규칙: 블록 블록을 위한 규칙 T ⊢ E:t T[x ↦ t] ⊢ S:t’ T ⊢ let t x = E in S end:t’ 블록이 시작되면 선언된 변수 x의 타입 정보를 추가한다. 추가된 타입 환경에서 S의 타입을 계산한다. 계산된 S의 타입이 let 전체의 타입이 된다. © 숙대 창병모

Example 1 let int x = 0 in x = x + 1 end 타입 검사 {x ↦ int} ⊢ x:int {x ↦ int} ⊢ 1:int {x ↦ int} ⊢ x:int {x ↦ int} ⊢ x + 1:int { } ⊢ 0 : int {x ↦ int} ⊢ x = x + 1:void { } ⊢ let int x = 0 in x = x + 1 end:void © 숙대 창병모

타입 규칙: 함수 fun bool f(int x) : if x > 0 then return true T ⊢ E:t 함수 정의 및 타입 함수 정의 fun bool f(int x) : if x > 0 then return true else return false 함수의 타입 f: int  bool 리턴문의 타입 규칙 T ⊢ E:t T ⊢ return E:t © 숙대 창병모

타입 규칙: 함수 T(f) = t1  t2 T ⊢ E:t1 T[x ↦ t1] ⊢ S:t2 함수 정의의 타입 규칙 T ⊢ fun t2 f(t1 x):S :t1  t2 함수 호출의 타입 규칙 실매개변수 타입 = 형식 매개변수 타입 호출 결과 타입 = 함수의 f의 반환 타입 T(f) = t1  t2 T ⊢ E:t1 T ⊢ f(E):t2 © 숙대 창병모

Example 2 다음 함수의 타입은 bool f(int x) : if x > 0 then return true else return false T[x ↦ int] ⊢ x:int T[x ↦ int] ⊢ 0:int T[x ↦ int] ⊢ true:bool ... T[x ↦ int] ⊢ x > 0:bool T[x ↦ int] ⊢ return true:bool ... T[x ↦ int] ⊢ if … :bool T ⊢ fun bool f(int x):if … :int  bool © 숙대 창병모

Example 3 T(f) = int  bool T ⊢ 1: int 다음 호출에 대한 타입 검사 ? f(1); T ⊢ f(1) : bool © 숙대 창병모

타입 안전성: 사례 Not safe: BCPL family, including C and C++ Casts, pointer arithmetic Almost safe: Algol family, Pascal, Ada. Dangling pointers. Allocate a pointer p to an integer, deallocate the memory referenced by p, then later use the value pointed to by p Safe: Lisp, ML, Smalltalk, and Java Lisp, Smalltalk: dynamically typed ML, Java: statically typed © 숙대 창병모

타입 검사기 구현: 언어 S Syntax S  … Semantics Example | let t x = E in S end | let fun t f(t x {,t x}) : S in S end | return E // 함수 내의 마지막 문장에 나타난다. t  int | bool F  … | f(E {,E}) Semantics 이름 f는 선언된 블록 내에서만 유효하다. 이름 f는 정의된 함수를 나타낸다. Example let int y = 0, fun int square(int x): return x * x in y = square(5) end © 숙대 창병모 © 숙대 창병모 Oct 2007 45

타입 검사기 구현 Type environment State vs Type environment 각 지점에서 유효한 변수/함수들의 타입 정보를 유지한다. 타입 환경 T: Var∪Fun → Type Example T = {x ↦ int, y ↦ int, f ↦ int  int} State vs Type environment s: Var  Int vs T: Var∪Fun  Type 상태 s: 변수들의 값 T: 변수/함수들의 타입 심볼 테이블: 변수들의 값 유지 변수/함수들의 타입 유지 © 숙대 창병모

타입 검사기 구현 S interpreter 수정하여 타입 검사기 구현 상태(변수들의 값) 대신에 타입 환경(변수/함수들의 타입) 유지 State transition 대신에 Typing rule 적용 타입 오류에 대해서 오류 메시지 출력 State transition rule vs Typing rule Expr의 값 계산 vs Expr의 타입 계산 Stmt의 실제 실행 vs Stmt의 타입 규칙을 적용하여 타입이 올바르게 사용되는지 검사 © 숙대 창병모