Bài giảng Chương trình dịch - Chương V: Kiểm tra kiểu

CHƯƠNG V Kiểm tra kiểu 
Mục tiêu : 
 Nắm được cách định nghĩa hệ thống kiểu trong các ngôn ngữ lập trình 
 Cách kiểm tra kiểu trong quá trình biên dịch 
1 
Biểu thức kiểu 
Kiểu của một ngôn ngữ lập trình được kí hiệu bởi các biểu thức kiểu (type expression). 
Biểu thức kiểu được định nghĩa như sau : 
Kiểu cơ sở là một biểu thức kiểu : boolean , char, integer, real, type_error , void 
Một tên kiểu là một biểu thức kiểu 
3. Mỗi kiểu dữ liệu có cấu trúc là một biểu thức kiểu , các cấu trúc bao gồm : 
2 
Mảng (array): Nếu T là một biểu thức kiểu thì array(I , T) là một biểu thức kiểu . Một mảng có   tập chỉ số I và các phần tử có kiểu T 
Tích (product): Nếu T1, T2 là biểu thức kiểu thì tích Đề - các T1* T2 là biểu thức kiểu 
Bản ghi (record): Là cấu trúc bao gồm một bộ các tên trường , kiểu trường 
Con trỏ (pointer): Nếu T là một biểu thức kiểu thì pointer(T ) là một biểu thức kiểu T 
Hàm (function): Hàm là một ánh xạ các phần tử của tập xác định (domain) D lên tập giá trị (range) R. Một hàm là một biểu thức kiểu D  R 
3 
Đặc tả một bộ kiểm tra kiểu đơn giản 
Trong phần này chúng ta mô tả một bộ kiểm tra kiểu cho một ngôn ngữ đơn giản trong đó kiểu của mỗi một định danh được khai báo trước khi sử dụng 
Bộ kiểm tra kiểu (type checker) là một lược đồ dịch , nó tổng hợp kiểu của mỗi biểu thức từ kiểu của các biểu thức con của nó 
4 
Định nghĩa một ngôn ngữ đơn giản : Văn phạm sau sinh ra một chương trình , biểu diễn bởi một ký hiệu chưa kết thúc P chứa một chuỗi các khai báo D và một biểu thức đơn giản E 
	P  D ; E 
	D  D ; D | id : T 
	T  char | integer | array [ num ] of T |  T 
	E  literal | num | id | E mod E | E [E] | E  
Ví dụ 5.1: Chương trình sau sinh bởi văn phạm trên 
	key: integer; 
	key mod 1999 
5 
Ta có lược đồ dịch để lưu trữ kiểu của một định danh 
	 P  D ; E 
	D  D ; D 
	D  id : T                     { addtype( id .entry , T.type ) } 
	T  char                       { T.type := char } 
	T  integer                  { T.type := integer } 
	T   T1                       { T.type := pointer(T1.type) } 
	T  array [ num ] of T1  { T.type := array(1... num .val , T1.type) } 
6 
Kiểm tra kiểu của các biểu thức 
Lược đồ dịch cho kiểm tra kiểu của biểu thức : 
	E  literal                 { E.type := char } 
	E  num                   { E.type := integer } 
	E  id                       { E.type := lookup(id.entry ) } 
	E  E 1 mod E 2        { E.type :=  if  E 1 .type = integer 	 and  E 2 .type = integer          
                                          then   integer   else   type_error } 
	E  E 1 [E 2 ]               { E.type := if   E 2 .type =integer 	   and  E 1 .type = array(s,t ) 
	         then  t   else   type_error } 
	E  E 1                     { E.type :=  if  E 1 .type = pointer(t ) 	 then  t  else       type_error } 
7 
Kiểm tra kiểu của các câu lệnh 
Các câu lệnh cấu tạo lên ngôn ngữ không có giá trị , do đó ta gán cho chúng kiểu void 
Lược đồ dịch cho kiểm tra kiểu của các lệnh : 
	S  id := E    	{ S.type := if     id.type = E.type 	 	then  void  else  type_error } 
	S  if   E then   S 1 	{ S.type := if  E.type = boolean   
	then  S 1 .type  else type_error } 
	S  while   E  do   S 1 	{ S.type := if  E.type = boolean   
	then  S 1 .type  else    type_error } 
	S  S 1 ; S 2      	{ S.type := if  S 1 .type = void  
	and  S 2 .type = void  then  void 
                                                      else  type_error } 
8 
Kiểm tra kiểu của các hàm 
Việc ghép một hàm với một đối (argument) có thể diễn đạt bởi luật sinh : E  E ( E ) 
Lược đồ dịch kiểm tra kiểu cho một hàm : 
	E  E 1 (E 2 )   { E.type :=  if  E 2 .type = s  
	and   E1.type = s -> t   then  t 
                            else    type_error } 
Nếu có nhiều đối có kiểu tương ứng T 1 , T 2 ,..., T n được coi như một đối duy nhất có kiểu T 1* T 2 *...* T n 
9 
Chuyển đổi kiểu 
Xét biểu thức x + i trong đó x có kiểu real và i có kiểu integer. Trình biên dịch có thể thực hiện việc chuyển đổi kiểu để hai toán hạng có cùng kiểu khi phép toán cộng xảy ra 
Bộ kiểm tra kiểu trong trình biên dịch có thể thêm các phép toán biến đổi kiểu vào trong biểu diễn trung gian của chương trình nguồn 
Chẳng hạn ký hiệu hậu tố của x + i có thể là :   x  i  inttoreal   real+ ( inttoreal đổi số nguyên i thành số thực , real+ thực hiện phép cộng các số thực ) 
10 
Ép kiểu (coercion): Việc chuyển một kiểu dữ liệu sang một kiểu khác được gọi là ẩn (implicit) nếu nó được làm tự động bởi compiler và được gọi là hiện (explicit) nếu được giải quyết bởi người lập trình 
Ví dụ 5.2: Hàm ord () trong pascal chuyển kiểu kí tự sang số nguyên , phép chuyển đổi là hiện 
	 Lệnh a:=b; trong đó a kiểu real, b kiểu integer khi thực hiện compiler sẽ thực hiện ép kiểu biến b sang kiểu real trước khi thực hiện lệnh gán , phép chuyển đổi là ẩn 
11