Nguy n Ph ng Tháiễ ươ
B môn Khoa h c Máy tínhộ ọ
http://www.coltech.vnu.vn/~thainp/
Nội dung
Bi u th c ki uể ứ ể
H th ng ki uệ ố ể
Lu t ng nghĩa ki m tra ki uậ ữ ể ể
Giới thiệu
Mô đun phân tích ng nghĩa: ki m tra tính đúng đn v ữ ể ắ ề
m t ng nghĩa c a ch ng trình ngu nặ ữ ủ ươ ồ
Vi c ki m tra đc chia làm hai lo i:ệ ể ượ ạ
ki m tra tĩnh ể
ki m tra đng (ki m tra đng x y ra lúc ch ng trình đích ể ộ ể ộ ả ươ
ch y)ạ
Trong bài gi ng này ta ch xét m t s d ng c a ki m tra ả ỉ ộ ố ạ ủ ể
tĩnh
Giới thiệu (tiếp)
ki m tra ki u: ki m tra v tính đúng đn c a các ki u toán h ng ể ể ể ề ắ ủ ể ạ
trong bi u th c.ể ứ
ki m tra dòng đi u khi n: m t s đi u khi n ph i có c u trúc h p ể ề ể ộ ố ề ể ả ấ ợ
lý, ví d nh l nh ụ ư ệ break trong ngôn ng C ph i n m trong m t ữ ả ằ ộ
vòng l p.ặ
ki m tra tính nh t quán: có nh ng ng c nh mà trong đó m t đi ể ấ ữ ữ ả ộ ố
t ng đc đnh nghĩa ch đúng m t l n. Ví d , trong Pascal, m t ượ ượ ị ỉ ộ ầ ụ ộ
tên ph i đc khai báo duy nh t, các nhãn trong l nh case ph i ả ượ ấ ệ ả
khác nhau, và các ph n t trong ki u vô h ng không đc l p ầ ử ể ướ ượ ặ
l i.ạ
ki m tra quan h tên: Đôi khi m t tên ph i xu t hi n t hai l n tr ể ệ ộ ả ấ ệ ừ ầ ở
lên. Ví d , trong Assembly, m t ch ng trình con có m t tên mà ụ ộ ươ ộ
chúng ph i xu t hi n đu và cu i c a ch ng trình con này.ả ấ ệ ở ầ ố ủ ươ
Biểu thức kiểu
Ki u c a m t c u trúc ngôn ng đc bi u th b i ể ủ ộ ấ ữ ượ ể ị ở
“bi u th c ki u”ể ứ ể
M t bi u th c ki u có th là:ộ ể ứ ể ể
m t ki u c b n ộ ể ơ ả
ki u h p thành: đc xây d ng t các ki u c b n theo ể ợ ượ ự ừ ể ơ ả
m t s toán t nào đóộ ố ử