編程語(yǔ)言詳細(xì)課程課件

第五章類(lèi)型檢查

本章內(nèi)容靜態(tài)檢查中最典型的部分—類(lèi)型檢查： 類(lèi)型系統(tǒng)、類(lèi)型檢查、多態(tài)函數(shù)、重載忽略其它的靜態(tài)檢查：控制流檢查、唯一性檢查、關(guān)聯(lián)名字檢查分析器類(lèi)型檢查器中間代碼生成器語(yǔ)法樹(shù)語(yǔ)法樹(shù)中間表示記號(hào)流第五章類(lèi)型檢查本章內(nèi)容分析類(lèi)型中間語(yǔ)法樹(shù)語(yǔ)法樹(shù)中間15.1

類(lèi)型在編程語(yǔ)言中的作用5.1.1

執(zhí)行錯(cuò)誤和安全語(yǔ)言介紹一些和程序運(yùn)行有聯(lián)系的概念5.1類(lèi)型在編程語(yǔ)言中的作用5.1.1執(zhí)行錯(cuò)誤和安全語(yǔ)言25.1

類(lèi)型在編程語(yǔ)言中的作用5.1.1

執(zhí)行錯(cuò)誤和安全語(yǔ)言程序運(yùn)行時(shí)的執(zhí)行錯(cuò)誤分成兩類(lèi)會(huì)被捕獲的錯(cuò)誤（trappederror）5.1類(lèi)型在編程語(yǔ)言中的作用5.1.1執(zhí)行錯(cuò)誤和安全語(yǔ)言35.1

類(lèi)型在編程語(yǔ)言中的作用5.1.1

執(zhí)行錯(cuò)誤和安全語(yǔ)言程序運(yùn)行時(shí)的執(zhí)行錯(cuò)誤分成兩類(lèi)會(huì)被捕獲的錯(cuò)誤（trappederror）例：非法指令錯(cuò)誤5.1類(lèi)型在編程語(yǔ)言中的作用5.1.1執(zhí)行錯(cuò)誤和安全語(yǔ)言45.1

類(lèi)型在編程語(yǔ)言中的作用5.1.1

執(zhí)行錯(cuò)誤和安全語(yǔ)言程序運(yùn)行時(shí)的執(zhí)行錯(cuò)誤分成兩類(lèi)會(huì)被捕獲的錯(cuò)誤（trappederror）例：非法指令錯(cuò)誤、非法內(nèi)存訪問(wèn)5.1類(lèi)型在編程語(yǔ)言中的作用5.1.1執(zhí)行錯(cuò)誤和安全語(yǔ)言55.1

類(lèi)型在編程語(yǔ)言中的作用5.1.1

執(zhí)行錯(cuò)誤和安全語(yǔ)言程序運(yùn)行時(shí)的執(zhí)行錯(cuò)誤分成兩類(lèi)會(huì)被捕獲的錯(cuò)誤（trappederror）例：非法指令錯(cuò)誤、非法內(nèi)存訪問(wèn)、除數(shù)為零5.1類(lèi)型在編程語(yǔ)言中的作用5.1.1執(zhí)行錯(cuò)誤和安全語(yǔ)言65.1

類(lèi)型在編程語(yǔ)言中的作用5.1.1

執(zhí)行錯(cuò)誤和安全語(yǔ)言程序運(yùn)行時(shí)的執(zhí)行錯(cuò)誤分成兩類(lèi)會(huì)被捕獲的錯(cuò)誤（trappederror）例：非法指令錯(cuò)誤、非法內(nèi)存訪問(wèn)、除數(shù)為零引起計(jì)算立即停止5.1類(lèi)型在編程語(yǔ)言中的作用5.1.1執(zhí)行錯(cuò)誤和安全語(yǔ)言75.1

類(lèi)型在編程語(yǔ)言中的作用5.1.1

執(zhí)行錯(cuò)誤和安全語(yǔ)言程序運(yùn)行時(shí)的執(zhí)行錯(cuò)誤分成兩類(lèi)會(huì)被捕獲的錯(cuò)誤（trappederror）例：非法指令錯(cuò)誤、非法內(nèi)存訪問(wèn)、除數(shù)為零引起計(jì)算立即停止不會(huì)被捕獲的錯(cuò)誤（untrappederror）

5.1類(lèi)型在編程語(yǔ)言中的作用5.1.1執(zhí)行錯(cuò)誤和安全語(yǔ)言85.1

類(lèi)型在編程語(yǔ)言中的作用5.1.1

執(zhí)行錯(cuò)誤和安全語(yǔ)言程序運(yùn)行時(shí)的執(zhí)行錯(cuò)誤分成兩類(lèi)會(huì)被捕獲的錯(cuò)誤（trappederror）例：非法指令錯(cuò)誤、非法內(nèi)存訪問(wèn)、除數(shù)為零引起計(jì)算立即停止不會(huì)被捕獲的錯(cuò)誤（untrappederror）

例：下標(biāo)變量的訪問(wèn)越過(guò)了數(shù)組的末端5.1類(lèi)型在編程語(yǔ)言中的作用5.1.1執(zhí)行錯(cuò)誤和安全語(yǔ)言95.1

類(lèi)型在編程語(yǔ)言中的作用5.1.1

執(zhí)行錯(cuò)誤和安全語(yǔ)言程序運(yùn)行時(shí)的執(zhí)行錯(cuò)誤分成兩類(lèi)會(huì)被捕獲的錯(cuò)誤（trappederror）例：非法指令錯(cuò)誤、非法內(nèi)存訪問(wèn)、除數(shù)為零引起計(jì)算立即停止不會(huì)被捕獲的錯(cuò)誤（untrappederror）

例：下標(biāo)變量的訪問(wèn)越過(guò)了數(shù)組的末端例：跳到一個(gè)錯(cuò)誤的地址，該地址開(kāi)始的內(nèi)存正好代表一個(gè)指令序列5.1類(lèi)型在編程語(yǔ)言中的作用5.1.1執(zhí)行錯(cuò)誤和安全語(yǔ)言105.1

類(lèi)型在編程語(yǔ)言中的作用5.1.1

執(zhí)行錯(cuò)誤和安全語(yǔ)言程序運(yùn)行時(shí)的執(zhí)行錯(cuò)誤分成兩類(lèi)會(huì)被捕獲的錯(cuò)誤（trappederror）例：非法指令錯(cuò)誤、非法內(nèi)存訪問(wèn)、除數(shù)為零引起計(jì)算立即停止不會(huì)被捕獲的錯(cuò)誤（untrappederror）

例：下標(biāo)變量的訪問(wèn)越過(guò)了數(shù)組的末端例：跳到一個(gè)錯(cuò)誤的地址，該地址開(kāi)始的內(nèi)存正好代表一個(gè)指令序列錯(cuò)誤可能會(huì)有一段時(shí)間未引起注意5.1類(lèi)型在編程語(yǔ)言中的作用5.1.1執(zhí)行錯(cuò)誤和安全語(yǔ)言115.1

類(lèi)型在編程語(yǔ)言中的作用5.1.1

執(zhí)行錯(cuò)誤和安全語(yǔ)言良行為的程序不同場(chǎng)合對(duì)良行為的定義略有區(qū)別例如，沒(méi)有任何不會(huì)被捕獲錯(cuò)誤的程序5.1類(lèi)型在編程語(yǔ)言中的作用5.1.1執(zhí)行錯(cuò)誤和安全語(yǔ)言125.1

類(lèi)型在編程語(yǔ)言中的作用5.1.1

執(zhí)行錯(cuò)誤和安全語(yǔ)言良行為的程序不同場(chǎng)合對(duì)良行為的定義略有區(qū)別例如，沒(méi)有任何不會(huì)被捕獲錯(cuò)誤的程序安全語(yǔ)言任何合法程序都是良行為的5.1類(lèi)型在編程語(yǔ)言中的作用5.1.1執(zhí)行錯(cuò)誤和安全語(yǔ)言135.1

類(lèi)型在編程語(yǔ)言中的作用5.1.1

執(zhí)行錯(cuò)誤和安全語(yǔ)言良行為的程序不同場(chǎng)合對(duì)良行為的定義略有區(qū)別例如，沒(méi)有任何不會(huì)被捕獲錯(cuò)誤的程序安全語(yǔ)言任何合法程序都是良行為的通常是設(shè)計(jì)一個(gè)類(lèi)型系統(tǒng)，通過(guò)靜態(tài)的類(lèi)型檢查來(lái)拒絕不會(huì)被捕獲錯(cuò)誤5.1類(lèi)型在編程語(yǔ)言中的作用5.1.1執(zhí)行錯(cuò)誤和安全語(yǔ)言145.1

類(lèi)型在編程語(yǔ)言中的作用5.1.1

執(zhí)行錯(cuò)誤和安全語(yǔ)言良行為的程序不同場(chǎng)合對(duì)良行為的定義略有區(qū)別例如，沒(méi)有任何不會(huì)被捕獲錯(cuò)誤的程序安全語(yǔ)言任何合法程序都是良行為的通常是設(shè)計(jì)一個(gè)類(lèi)型系統(tǒng)，通過(guò)靜態(tài)的類(lèi)型檢查來(lái)拒絕不會(huì)被捕獲錯(cuò)誤但是，設(shè)計(jì)一個(gè)類(lèi)型系統(tǒng)，它正好只拒絕不會(huì)被捕獲錯(cuò)誤是非常困難的5.1類(lèi)型在編程語(yǔ)言中的作用5.1.1執(zhí)行錯(cuò)誤和安全語(yǔ)言155.1

類(lèi)型在編程語(yǔ)言中的作用5.1.1

執(zhí)行錯(cuò)誤和安全語(yǔ)言禁止錯(cuò)誤（forbiddenerror）不會(huì)被捕獲錯(cuò)誤集合+會(huì)被捕獲錯(cuò)誤的一個(gè)子集5.1類(lèi)型在編程語(yǔ)言中的作用5.1.1執(zhí)行錯(cuò)誤和安全語(yǔ)言165.1

類(lèi)型在編程語(yǔ)言中的作用5.1.1

執(zhí)行錯(cuò)誤和安全語(yǔ)言禁止錯(cuò)誤（forbiddenerror）不會(huì)被捕獲錯(cuò)誤集合+會(huì)被捕獲錯(cuò)誤的一個(gè)子集為語(yǔ)言設(shè)計(jì)類(lèi)型系統(tǒng)的目標(biāo)是在排除禁止錯(cuò)誤5.1類(lèi)型在編程語(yǔ)言中的作用5.1.1執(zhí)行錯(cuò)誤和安全語(yǔ)言175.1

類(lèi)型在編程語(yǔ)言中的作用5.1.1

執(zhí)行錯(cuò)誤和安全語(yǔ)言禁止錯(cuò)誤（forbiddenerror）不會(huì)被捕獲錯(cuò)誤集合+會(huì)被捕獲錯(cuò)誤的一個(gè)子集為語(yǔ)言設(shè)計(jì)類(lèi)型系統(tǒng)的目標(biāo)是在排除禁止錯(cuò)誤良行為程序和安全語(yǔ)言也可基于禁止錯(cuò)誤來(lái)定義5.1類(lèi)型在編程語(yǔ)言中的作用5.1.1執(zhí)行錯(cuò)誤和安全語(yǔ)言185.1

類(lèi)型在編程語(yǔ)言中的作用5.1.2類(lèi)型化語(yǔ)言和類(lèi)型系統(tǒng)類(lèi)型化的語(yǔ)言變量的類(lèi)型變量在程序執(zhí)行期間的取值范圍5.1類(lèi)型在編程語(yǔ)言中的作用5.1.2類(lèi)型化語(yǔ)言和類(lèi)型系195.1

類(lèi)型在編程語(yǔ)言中的作用5.1.2類(lèi)型化語(yǔ)言和類(lèi)型系統(tǒng)類(lèi)型化的語(yǔ)言變量的類(lèi)型類(lèi)型化的語(yǔ)言變量都被給定類(lèi)型的語(yǔ)言并且表達(dá)式、語(yǔ)句等語(yǔ)法構(gòu)造的類(lèi)型都是可以靜態(tài)確定的例如，類(lèi)型boolean的變量x在程序每次運(yùn)行時(shí)的值只能是布爾值，not(x)總有意義5.1類(lèi)型在編程語(yǔ)言中的作用5.1.2類(lèi)型化語(yǔ)言和類(lèi)型系205.1

類(lèi)型在編程語(yǔ)言中的作用5.1.2類(lèi)型化語(yǔ)言和類(lèi)型系統(tǒng)類(lèi)型化的語(yǔ)言變量的類(lèi)型類(lèi)型化的語(yǔ)言未類(lèi)型化的語(yǔ)言不限制變量值范圍的語(yǔ)言：

一個(gè)運(yùn)算可以作用到任意的運(yùn)算對(duì)象，其結(jié)果可能是一個(gè)有意義的值、一個(gè)錯(cuò)誤、一個(gè)異?；蛞粋€(gè)語(yǔ)言未加定義的結(jié)果例如：LISP語(yǔ)言5.1類(lèi)型在編程語(yǔ)言中的作用5.1.2類(lèi)型化語(yǔ)言和類(lèi)型系215.1

類(lèi)型在編程語(yǔ)言中的作用5.1.2類(lèi)型化語(yǔ)言和類(lèi)型系統(tǒng)類(lèi)型化的語(yǔ)言變量的類(lèi)型類(lèi)型化的語(yǔ)言未類(lèi)型化的語(yǔ)言顯式類(lèi)型化語(yǔ)言類(lèi)型是語(yǔ)法的一部分5.1類(lèi)型在編程語(yǔ)言中的作用5.1.2類(lèi)型化語(yǔ)言和類(lèi)型系225.1

類(lèi)型在編程語(yǔ)言中的作用5.1.2類(lèi)型化語(yǔ)言和類(lèi)型系統(tǒng)類(lèi)型化的語(yǔ)言變量的類(lèi)型類(lèi)型化的語(yǔ)言未類(lèi)型化的語(yǔ)言顯式類(lèi)型化語(yǔ)言隱式類(lèi)型化的語(yǔ)言不存在隱式類(lèi)型化的主流語(yǔ)言，但可能存在忽略類(lèi)型信息的程序片段，例如不需要程序員聲明函數(shù)的參數(shù)類(lèi)型5.1類(lèi)型在編程語(yǔ)言中的作用5.1.2類(lèi)型化語(yǔ)言和類(lèi)型系235.1

類(lèi)型在編程語(yǔ)言中的作用5.1.2類(lèi)型化語(yǔ)言和類(lèi)型系統(tǒng)類(lèi)型系統(tǒng)語(yǔ)言的組成部分,由一組定型規(guī)則（typingrule）構(gòu)成，這組規(guī)則用來(lái)給各種語(yǔ)言構(gòu)造指派類(lèi)型5.1類(lèi)型在編程語(yǔ)言中的作用5.1.2類(lèi)型化語(yǔ)言和類(lèi)型系245.1

類(lèi)型在編程語(yǔ)言中的作用5.1.2類(lèi)型化語(yǔ)言和類(lèi)型系統(tǒng)類(lèi)型系統(tǒng)語(yǔ)言的組成部分,由一組定型規(guī)則（typingrule）構(gòu)成，這組規(guī)則用來(lái)給各種語(yǔ)言構(gòu)造指派類(lèi)型設(shè)計(jì)類(lèi)型系統(tǒng)的根本目的是用靜態(tài)檢查的方式來(lái)保證合法程序運(yùn)行時(shí)的良行為5.1類(lèi)型在編程語(yǔ)言中的作用5.1.2類(lèi)型化語(yǔ)言和類(lèi)型系255.1

類(lèi)型在編程語(yǔ)言中的作用5.1.2類(lèi)型化語(yǔ)言和類(lèi)型系統(tǒng)類(lèi)型系統(tǒng)語(yǔ)言的組成部分,由一組定型規(guī)則（typingrule）構(gòu)成，這組規(guī)則用來(lái)給各種語(yǔ)言構(gòu)造指派類(lèi)型設(shè)計(jì)類(lèi)型系統(tǒng)的根本目的是用靜態(tài)檢查的方式來(lái)保證合法程序運(yùn)行時(shí)的良行為類(lèi)型系統(tǒng)的形式化類(lèi)型表達(dá)式、定型斷言、定型規(guī)則5.1類(lèi)型在編程語(yǔ)言中的作用5.1.2類(lèi)型化語(yǔ)言和類(lèi)型系265.1

類(lèi)型在編程語(yǔ)言中的作用5.1.2類(lèi)型化語(yǔ)言和類(lèi)型系統(tǒng)類(lèi)型系統(tǒng)語(yǔ)言的組成部分,由一組定型規(guī)則（typingrule）構(gòu)成，這組規(guī)則用來(lái)給各種語(yǔ)言構(gòu)造指派類(lèi)型設(shè)計(jì)類(lèi)型系統(tǒng)的根本目的是用靜態(tài)檢查的方式來(lái)保證合法程序運(yùn)行時(shí)的良行為類(lèi)型系統(tǒng)的形式化類(lèi)型表達(dá)式、定型斷言、定型規(guī)則類(lèi)型檢查算法通常是靜態(tài)地完成類(lèi)型檢查5.1類(lèi)型在編程語(yǔ)言中的作用5.1.2類(lèi)型化語(yǔ)言和類(lèi)型系275.1

類(lèi)型在編程語(yǔ)言中的作用5.1.2類(lèi)型化語(yǔ)言和類(lèi)型系統(tǒng)良類(lèi)型的程序沒(méi)有類(lèi)型錯(cuò)誤的程序5.1類(lèi)型在編程語(yǔ)言中的作用5.1.2類(lèi)型化語(yǔ)言和類(lèi)型系285.1

類(lèi)型在編程語(yǔ)言中的作用5.1.2類(lèi)型化語(yǔ)言和類(lèi)型系統(tǒng)良類(lèi)型的程序沒(méi)有類(lèi)型錯(cuò)誤的程序合法程序良類(lèi)型程序（若語(yǔ)言定義中無(wú)其它方式表示的約束）5.1類(lèi)型在編程語(yǔ)言中的作用5.1.2類(lèi)型化語(yǔ)言和類(lèi)型系295.1

類(lèi)型在編程語(yǔ)言中的作用5.1.2類(lèi)型化語(yǔ)言和類(lèi)型系統(tǒng)良類(lèi)型的程序沒(méi)有類(lèi)型錯(cuò)誤的程序合法程序良類(lèi)型程序（若語(yǔ)言定義中無(wú)其它方式表示的約束）類(lèi)型可靠（typesound）的語(yǔ)言所有良類(lèi)型程序（合法程序）都是良行為的類(lèi)型可靠的語(yǔ)言一定是安全的語(yǔ)言5.1類(lèi)型在編程語(yǔ)言中的作用5.1.2類(lèi)型化語(yǔ)言和類(lèi)型系305.1

類(lèi)型在編程語(yǔ)言中的作用5.1.2類(lèi)型化語(yǔ)言和類(lèi)型系統(tǒng)語(yǔ)法的和靜態(tài)的概念 動(dòng)態(tài)的概念 類(lèi)型化語(yǔ)言 安全語(yǔ)言 良類(lèi)型程序 良行為的程序5.1類(lèi)型在編程語(yǔ)言中的作用5.1.2類(lèi)型化語(yǔ)言和類(lèi)型系315.1

類(lèi)型在編程語(yǔ)言中的作用5.1.2類(lèi)型化語(yǔ)言和類(lèi)型系統(tǒng)未類(lèi)型化語(yǔ)言可以通過(guò)徹底的運(yùn)行時(shí)詳細(xì)檢查來(lái)排除所有的禁止錯(cuò)誤如LISP語(yǔ)言5.1類(lèi)型在編程語(yǔ)言中的作用5.1.2類(lèi)型化語(yǔ)言和類(lèi)型系325.1

類(lèi)型在編程語(yǔ)言中的作用5.1.2類(lèi)型化語(yǔ)言和類(lèi)型系統(tǒng)未類(lèi)型化語(yǔ)言可以通過(guò)徹底的運(yùn)行時(shí)詳細(xì)檢查來(lái)排除所有的禁止錯(cuò)誤如LISP語(yǔ)言類(lèi)型化語(yǔ)言類(lèi)型檢查也可以放在運(yùn)行時(shí)完成，但影響效率一般都是靜態(tài)檢查，類(lèi)型系統(tǒng)被用來(lái)支持靜態(tài)檢查靜態(tài)檢查語(yǔ)言通常也需要一些運(yùn)行時(shí)的檢查數(shù)組訪問(wèn)越界檢查5.1類(lèi)型在編程語(yǔ)言中的作用5.1.2類(lèi)型化語(yǔ)言和類(lèi)型系335.1

類(lèi)型在編程語(yǔ)言中的作用5.1.2類(lèi)型化語(yǔ)言和類(lèi)型系統(tǒng)實(shí)際使用的一些語(yǔ)言并不安全禁止錯(cuò)誤集合沒(méi)有囊括所有不會(huì)被捕獲的錯(cuò)誤Pascal語(yǔ)言

無(wú)標(biāo)志的變體記錄類(lèi)型函數(shù)型參數(shù)5.1類(lèi)型在編程語(yǔ)言中的作用5.1.2類(lèi)型化語(yǔ)言和類(lèi)型系345.1

類(lèi)型在編程語(yǔ)言中的作用5.1.2類(lèi)型化語(yǔ)言和類(lèi)型系統(tǒng)實(shí)際使用的一些語(yǔ)言并不安全禁止錯(cuò)誤集合沒(méi)有囊括所有不會(huì)被捕獲的錯(cuò)誤Pascal語(yǔ)言用C語(yǔ)言的共用體（union）來(lái)舉例 unionU{intu1;int

u2;}u; int

p; u.u1=10; p=u.u2;

p=0;5.1類(lèi)型在編程語(yǔ)言中的作用5.1.2類(lèi)型化語(yǔ)言和類(lèi)型系355.1

類(lèi)型在編程語(yǔ)言中的作用5.1.2類(lèi)型化語(yǔ)言和類(lèi)型系統(tǒng)實(shí)際使用的一些語(yǔ)言并不安全C語(yǔ)言還有很多不安全的并且被廣泛使用的特征，如： 指針?biāo)阈g(shù)運(yùn)算、類(lèi)型強(qiáng)制、參數(shù)個(gè)數(shù)可變5.1類(lèi)型在編程語(yǔ)言中的作用5.1.2類(lèi)型化語(yǔ)言和類(lèi)型系365.1

類(lèi)型在編程語(yǔ)言中的作用5.1.2類(lèi)型化語(yǔ)言和類(lèi)型系統(tǒng)實(shí)際使用的一些語(yǔ)言并不安全C語(yǔ)言還有很多不安全的并且被廣泛使用的特征，如： 指針?biāo)阈g(shù)運(yùn)算、類(lèi)型強(qiáng)制、參數(shù)個(gè)數(shù)可變?cè)谡Z(yǔ)言設(shè)計(jì)的歷史上，安全性考慮不足是因?yàn)閺?qiáng)調(diào)代碼的執(zhí)行效率5.1類(lèi)型在編程語(yǔ)言中的作用5.1.2類(lèi)型化語(yǔ)言和類(lèi)型系375.1

類(lèi)型在編程語(yǔ)言中的作用5.1.2類(lèi)型化語(yǔ)言和類(lèi)型系統(tǒng)實(shí)際使用的一些語(yǔ)言并不安全C語(yǔ)言還有很多不安全的并且被廣泛使用的特征，如： 指針?biāo)阈g(shù)運(yùn)算、類(lèi)型強(qiáng)制、參數(shù)個(gè)數(shù)可變?cè)谡Z(yǔ)言設(shè)計(jì)的歷史上，安全性考慮不足是因?yàn)閺?qiáng)調(diào)代碼的執(zhí)行效率在現(xiàn)代語(yǔ)言設(shè)計(jì)上，安全性的位置越來(lái)越重要5.1類(lèi)型在編程語(yǔ)言中的作用5.1.2類(lèi)型化語(yǔ)言和類(lèi)型系385.1

類(lèi)型在編程語(yǔ)言中的作用5.1.2類(lèi)型化語(yǔ)言和類(lèi)型系統(tǒng)實(shí)際使用的一些語(yǔ)言并不安全C語(yǔ)言還有很多不安全的并且被廣泛使用的特征，如： 指針?biāo)阈g(shù)運(yùn)算、類(lèi)型強(qiáng)制、參數(shù)個(gè)數(shù)可變?cè)谡Z(yǔ)言設(shè)計(jì)的歷史上，安全性考慮不足是因?yàn)閺?qiáng)調(diào)代碼的執(zhí)行效率在現(xiàn)代語(yǔ)言設(shè)計(jì)上，安全性的位置越來(lái)越重要C的一些問(wèn)題已經(jīng)在C++中得以緩和更多一些問(wèn)題在Java中已得到解決5.1類(lèi)型在編程語(yǔ)言中的作用5.1.2類(lèi)型化語(yǔ)言和類(lèi)型系395.1

類(lèi)型在編程語(yǔ)言中的作用5.1.3

類(lèi)型化語(yǔ)言的優(yōu)點(diǎn)從工程的觀點(diǎn)看，類(lèi)型化語(yǔ)言有下面一些優(yōu)點(diǎn)

開(kāi)發(fā)的實(shí)惠較早發(fā)現(xiàn)錯(cuò)誤類(lèi)型信息還具有文檔作用5.1類(lèi)型在編程語(yǔ)言中的作用5.1.3類(lèi)型化語(yǔ)言的優(yōu)點(diǎn)405.1

類(lèi)型在編程語(yǔ)言中的作用5.1.3

類(lèi)型化語(yǔ)言的優(yōu)點(diǎn)從工程的觀點(diǎn)看，類(lèi)型化語(yǔ)言有下面一些優(yōu)點(diǎn)

開(kāi)發(fā)的實(shí)惠較早發(fā)現(xiàn)錯(cuò)誤類(lèi)型信息還具有文檔作用

編譯的實(shí)惠程序模塊可以相互獨(dú)立地編譯5.1類(lèi)型在編程語(yǔ)言中的作用5.1.3類(lèi)型化語(yǔ)言的優(yōu)點(diǎn)415.1

類(lèi)型在編程語(yǔ)言中的作用5.1.3

類(lèi)型化語(yǔ)言的優(yōu)點(diǎn)從工程的觀點(diǎn)看，類(lèi)型化語(yǔ)言有下面一些優(yōu)點(diǎn)

開(kāi)發(fā)的實(shí)惠較早發(fā)現(xiàn)錯(cuò)誤類(lèi)型信息還具有文檔作用

編譯的實(shí)惠程序模塊可以相互獨(dú)立地編譯運(yùn)行的實(shí)惠可得到更有效的空間安排和訪問(wèn)方式5.1類(lèi)型在編程語(yǔ)言中的作用5.1.3類(lèi)型化語(yǔ)言的優(yōu)點(diǎn)425.2

描述類(lèi)型系統(tǒng)的語(yǔ)言類(lèi)型系統(tǒng)主要用來(lái)說(shuō)明編程語(yǔ)言的定型規(guī)則,它獨(dú)立于類(lèi)型檢查算法5.2描述類(lèi)型系統(tǒng)的語(yǔ)言類(lèi)型系統(tǒng)主要用來(lái)說(shuō)明編程語(yǔ)言的定型435.2

描述類(lèi)型系統(tǒng)的語(yǔ)言類(lèi)型系統(tǒng)主要用來(lái)說(shuō)明編程語(yǔ)言的定型規(guī)則,它獨(dú)立于類(lèi)型檢查算法定義一個(gè)類(lèi)型系統(tǒng)，一種重要的設(shè)計(jì)目標(biāo)是存在有效的類(lèi)型檢查算法5.2描述類(lèi)型系統(tǒng)的語(yǔ)言類(lèi)型系統(tǒng)主要用來(lái)說(shuō)明編程語(yǔ)言的定型445.2

描述類(lèi)型系統(tǒng)的語(yǔ)言類(lèi)型系統(tǒng)主要用來(lái)說(shuō)明編程語(yǔ)言的定型規(guī)則,它獨(dú)立于類(lèi)型檢查算法定義一個(gè)類(lèi)型系統(tǒng)，一種重要的設(shè)計(jì)目標(biāo)是存在有效的類(lèi)型檢查算法類(lèi)型系統(tǒng)的基本概念可用于各類(lèi)語(yǔ)言，包括函數(shù)式語(yǔ)言、命令式語(yǔ)言和并行語(yǔ)言等5.2描述類(lèi)型系統(tǒng)的語(yǔ)言類(lèi)型系統(tǒng)主要用來(lái)說(shuō)明編程語(yǔ)言的定型455.2

描述類(lèi)型系統(tǒng)的語(yǔ)言類(lèi)型系統(tǒng)主要用來(lái)說(shuō)明編程語(yǔ)言的定型規(guī)則,它獨(dú)立于類(lèi)型檢查算法定義一個(gè)類(lèi)型系統(tǒng)，一種重要的設(shè)計(jì)目標(biāo)是存在有效的類(lèi)型檢查算法類(lèi)型系統(tǒng)的基本概念可用于各類(lèi)語(yǔ)言，包括函數(shù)式語(yǔ)言、命令式語(yǔ)言和并行語(yǔ)言等本節(jié)討論用形式方法來(lái)描述類(lèi)型系統(tǒng)5.2描述類(lèi)型系統(tǒng)的語(yǔ)言類(lèi)型系統(tǒng)主要用來(lái)說(shuō)明編程語(yǔ)言的定型465.2

描述類(lèi)型系統(tǒng)的語(yǔ)言類(lèi)型系統(tǒng)主要用來(lái)說(shuō)明編程語(yǔ)言的定型規(guī)則,它獨(dú)立于類(lèi)型檢查算法定義一個(gè)類(lèi)型系統(tǒng)，一種重要的設(shè)計(jì)目標(biāo)是存在有效的類(lèi)型檢查算法類(lèi)型系統(tǒng)的基本概念可用于各類(lèi)語(yǔ)言，包括函數(shù)式語(yǔ)言、命令式語(yǔ)言和并行語(yǔ)言等本節(jié)討論用形式方法來(lái)描述類(lèi)型系統(tǒng)然后討論實(shí)例語(yǔ)言時(shí)：先定義語(yǔ)法，再給出類(lèi)型系統(tǒng)的形式描述，最后寫(xiě)出類(lèi)型檢查的翻譯方案5.2描述類(lèi)型系統(tǒng)的語(yǔ)言類(lèi)型系統(tǒng)主要用來(lái)說(shuō)明編程語(yǔ)言的定型475.2

描述類(lèi)型系統(tǒng)的語(yǔ)言類(lèi)型系統(tǒng)的形式化類(lèi)型系統(tǒng)是一種邏輯系統(tǒng)

有關(guān)自然數(shù)的邏輯系統(tǒng)- 自然數(shù)表達(dá)式（需要定義它的語(yǔ)法）

a+b,3-良形公式 （邏輯斷言，需要定義它的語(yǔ)法）

a+b=3,(d=3)(c<10)-推理規(guī)則 a<b,b<ca<c5.2描述類(lèi)型系統(tǒng)的語(yǔ)言類(lèi)型系統(tǒng)的形式化a<b,485.2

描述類(lèi)型系統(tǒng)的語(yǔ)言類(lèi)型系統(tǒng)的形式化類(lèi)型系統(tǒng)是一種邏輯系統(tǒng)

有關(guān)自然數(shù)的邏輯系統(tǒng) 類(lèi)型系統(tǒng)- 自然數(shù)表達(dá)式 類(lèi)型表達(dá)式

a+b,3 intint-良形公式

a+b=3,(d=3)(c<10) -推理規(guī)則 a<b,b<ca<c5.2描述類(lèi)型系統(tǒng)的語(yǔ)言類(lèi)型系統(tǒng)的形式化a<b,495.2

描述類(lèi)型系統(tǒng)的語(yǔ)言類(lèi)型系統(tǒng)的形式化類(lèi)型系統(tǒng)是一種邏輯系統(tǒng)

有關(guān)自然數(shù)的邏輯系統(tǒng) 類(lèi)型系統(tǒng)- 自然數(shù)表達(dá)式 類(lèi)型表達(dá)式

a+b,3 intint-良形公式 定型斷言

a+b=3,(d=3)(c<10) {x:int}|–x+3:int-推理規(guī)則 ({x:int}叫做定型環(huán)境)a<b,b<ca<c5.2描述類(lèi)型系統(tǒng)的語(yǔ)言類(lèi)型系統(tǒng)的形式化a<b,505.2

描述類(lèi)型系統(tǒng)的語(yǔ)言類(lèi)型系統(tǒng)的形式化類(lèi)型系統(tǒng)是一種邏輯系統(tǒng)

有關(guān)自然數(shù)的邏輯系統(tǒng) 類(lèi)型系統(tǒng)- 自然數(shù)表達(dá)式 類(lèi)型表達(dá)式

a+b,3 intint-良形公式 定型斷言

a+b=3,(d=3)(c<10) {x:int}|–x+3:int-推理規(guī)則 定型規(guī)則

|–M:int,|–N:int

|–M+N:int

a<b,b<ca<c5.2描述類(lèi)型系統(tǒng)的語(yǔ)言類(lèi)型系統(tǒng)的形式化|–M515.2

描述類(lèi)型系統(tǒng)的語(yǔ)言類(lèi)型系統(tǒng)的形式化類(lèi)型表達(dá)式具體語(yǔ)法：出現(xiàn)在編程語(yǔ)言及定型斷言中抽象語(yǔ)法：出現(xiàn)在類(lèi)型檢查的實(shí)現(xiàn)中下一節(jié)開(kāi)始舉例定型斷言本節(jié)討論它的一般形式定型規(guī)則本節(jié)討論它的一般形式5.2描述類(lèi)型系統(tǒng)的語(yǔ)言類(lèi)型系統(tǒng)的形式化525.2

描述類(lèi)型系統(tǒng)的語(yǔ)言5.2.1

斷言斷言的形式 |–S

S的所有自由變量都聲明在

中其中

是一個(gè)靜態(tài)定型環(huán)境，如x1:T1,…,xn:TnS的形式隨斷言形式的不同而不同斷言有三種具體形式5.2描述類(lèi)型系統(tǒng)的語(yǔ)言5.2.1斷言535.2

描述類(lèi)型系統(tǒng)的語(yǔ)言環(huán)境斷言

|–

該斷言表示

是良形的環(huán)境將用推理規(guī)則來(lái)定義環(huán)境的語(yǔ)法(而不是用文法)5.2描述類(lèi)型系統(tǒng)的語(yǔ)言環(huán)境斷言545.2

描述類(lèi)型系統(tǒng)的語(yǔ)言環(huán)境斷言

|–

該斷言表示

是良形的環(huán)境將用推理規(guī)則來(lái)定義環(huán)境的語(yǔ)法語(yǔ)法斷言

|–

nat

在環(huán)境

下，nat是類(lèi)型表達(dá)式將用推理規(guī)則來(lái)定義類(lèi)型表達(dá)式的語(yǔ)法(而不是用文法)5.2描述類(lèi)型系統(tǒng)的語(yǔ)言環(huán)境斷言555.2

描述類(lèi)型系統(tǒng)的語(yǔ)言環(huán)境斷言

|–

該斷言表示

是良形的環(huán)境將用推理規(guī)則來(lái)定義環(huán)境的語(yǔ)法語(yǔ)法斷言

|–

nat

在環(huán)境

下，nat是類(lèi)型表達(dá)式將用推理規(guī)則來(lái)定義類(lèi)型表達(dá)式的語(yǔ)法定型斷言

|–

M:T 在環(huán)境

下，M具有類(lèi)型T 例：

|–true:boolean x:nat

|–x+1:nat將用推理規(guī)則來(lái)確定語(yǔ)法構(gòu)造實(shí)例的類(lèi)型5.2描述類(lèi)型系統(tǒng)的語(yǔ)言環(huán)境斷言565.2

描述類(lèi)型系統(tǒng)的語(yǔ)言有效斷言

|–

true:boolean無(wú)效斷言

|–true:nat5.2描述類(lèi)型系統(tǒng)的語(yǔ)言有效斷言575.2

描述類(lèi)型系統(tǒng)的語(yǔ)言5.2.2

推理規(guī)則習(xí)慣表示法前提、結(jié)論公理、推理規(guī)則

1

|–S1,…,

n|–Sn

|–S5.2描述類(lèi)型系統(tǒng)的語(yǔ)言5.2.2推理規(guī)則1|–585.2

描述類(lèi)型系統(tǒng)的語(yǔ)言5.2.2

推理規(guī)則（規(guī)則名） （注釋?zhuān)? 推理規(guī)則 （注釋?zhuān)┉h(huán)境規(guī)則 (Env

)

|–

5.2描述類(lèi)型系統(tǒng)的語(yǔ)言5.2.2推理規(guī)則595.2

描述類(lèi)型系統(tǒng)的語(yǔ)言5.2.2

推理規(guī)則（規(guī)則名） （注釋?zhuān)? 推理規(guī)則 （注釋?zhuān)┉h(huán)境規(guī)則 (Env

) 語(yǔ)法規(guī)則 (TypeBool)

|–

|–

|–boolean5.2描述類(lèi)型系統(tǒng)的語(yǔ)言5.2.2推理規(guī)則|–605.2

描述類(lèi)型系統(tǒng)的語(yǔ)言5.2.2

推理規(guī)則（規(guī)則名） （注釋?zhuān)? 推理規(guī)則 （注釋?zhuān)┉h(huán)境規(guī)則 (Env

) 語(yǔ)法規(guī)則 (TypeBool) 定型規(guī)則 (Val+)

|–

|–

|–boolean

|–M:int,|–N:int

|–M+N:int

5.2描述類(lèi)型系統(tǒng)的語(yǔ)言5.2.2推理規(guī)則|–615.2

描述類(lèi)型系統(tǒng)的語(yǔ)言5.2.3

類(lèi)型檢查和類(lèi)型推斷類(lèi)型檢查 用語(yǔ)法制導(dǎo)的方式，根據(jù)上下文有關(guān)的定型規(guī)則來(lái)判定程序構(gòu)造是否為良類(lèi)型的程序構(gòu)造的過(guò)程5.2描述類(lèi)型系統(tǒng)的語(yǔ)言5.2.3類(lèi)型檢查和類(lèi)型推斷625.2

描述類(lèi)型系統(tǒng)的語(yǔ)言5.2.3

類(lèi)型檢查和類(lèi)型推斷類(lèi)型檢查 用語(yǔ)法制導(dǎo)的方式，根據(jù)上下文有關(guān)的定型規(guī)則來(lái)判定程序構(gòu)造是否為良類(lèi)型的程序構(gòu)造的過(guò)程類(lèi)型推斷 類(lèi)型信息不完全的情況下的定型判定問(wèn)題 例如：f(x:t)=E

和f(x)=E的區(qū)別5.2描述類(lèi)型系統(tǒng)的語(yǔ)言5.2.3類(lèi)型檢查和類(lèi)型推斷635.3

簡(jiǎn)單類(lèi)型檢查器的說(shuō)明5.3.1

一個(gè)簡(jiǎn)單的語(yǔ)言P

D;SD

D;D|id:TT

boolean|integer|array[num]ofT|

T|T‘

’TS

id:=E|ifEthenS|whileEdoS|S;SE

truth|num|id|EmodE|E[E]|

E

|E(E)5.3簡(jiǎn)單類(lèi)型檢查器的說(shuō)明5.3.1一個(gè)簡(jiǎn)單的語(yǔ)言645.3

簡(jiǎn)單類(lèi)型檢查器的說(shuō)明例：

i:integer;

j:integer;

j:=imod20005.3簡(jiǎn)單類(lèi)型檢查器的說(shuō)明例：655.3

簡(jiǎn)單類(lèi)型檢查器的說(shuō)明5.3.2類(lèi)型系統(tǒng)環(huán)境規(guī)則(Env

) (DeclVar)其中id:T是該簡(jiǎn)單語(yǔ)言的一個(gè)聲明語(yǔ)句略去了基于程序中所有聲明語(yǔ)句來(lái)構(gòu)成整個(gè)的規(guī)則

|–

|

T,id

dom(

)

,id:T|

5.3簡(jiǎn)單類(lèi)型檢查器的說(shuō)明5.3.2類(lèi)型系統(tǒng)|T,665.3

簡(jiǎn)單類(lèi)型檢查器的說(shuō)明語(yǔ)法規(guī)則(TypeBool) (TypeInt)(TypeVoid)void用于表示語(yǔ)句類(lèi)型表明編程語(yǔ)言和定型斷言的類(lèi)型表達(dá)式并非完全一致

|

|

boolean

|

|

integer

|

|

void5.3簡(jiǎn)單類(lèi)型檢查器的說(shuō)明語(yǔ)法規(guī)則||675.3

簡(jiǎn)單類(lèi)型檢查器的說(shuō)明語(yǔ)法規(guī)則(TypeRef)(T

void) (TypeArray)(T

void) (N>0)(TypeFunction)(T1,T2

void)定型斷言中的類(lèi)型表達(dá)式也可以用抽象語(yǔ)法

|

T

|

pointer(T)

|

T,

|

N:integer

|

array(N,T)

|

T1,

|

T2

|

T1

T25.3簡(jiǎn)單類(lèi)型檢查器的說(shuō)明語(yǔ)法規(guī)則|T|685.3

簡(jiǎn)單類(lèi)型檢查器的說(shuō)明定型規(guī)則——表達(dá)式(ExpTruth) (ExpNum)(ExpId)

|

|

truth:boolean

|

|

num:integer

1,id:T,

2|

1,id:T,

2|

id:T5.3簡(jiǎn)單類(lèi)型檢查器的說(shuō)明定型規(guī)則——表達(dá)式|695.3

簡(jiǎn)單類(lèi)型檢查器的說(shuō)明定型規(guī)則——表達(dá)式(ExpMod) (ExpIndex)

(0

E2

N1)(ExpDeref)

|

E1:integer,

|

E2:integer

|

E1modE2:integer

|

E1:array(N,T),

|

E2:integer

|

E1[E2]:T

|

E:pointer(T)

|

E

:T5.3簡(jiǎn)單類(lèi)型檢查器的說(shuō)明定型規(guī)則——表達(dá)式|E705.3

簡(jiǎn)單類(lèi)型檢查器的說(shuō)明定型規(guī)則——表達(dá)式(ExpFunCall)

|

E1:T1

T2,

|

E2:T1

|

E1(E2):T25.3簡(jiǎn)單類(lèi)型檢查器的說(shuō)明定型規(guī)則——表達(dá)式|E715.3

簡(jiǎn)單類(lèi)型檢查器的說(shuō)明定型規(guī)則——語(yǔ)句(StateAssign)(T=booleanor

T=integer)(StateIf)(StateWhile)

|

id:T,

|

E:T

|

id:=E:void

|

E:boolean,

|

S:void

|

ifEthenS:void

|

E:boolean,

|

S:void

|

whileEdoS:void5.3簡(jiǎn)單類(lèi)型檢查器的說(shuō)明定型規(guī)則——語(yǔ)句|id725.3

簡(jiǎn)單類(lèi)型檢查器的說(shuō)明定型規(guī)則——語(yǔ)句(StateSeq)

|

S1:void,

|

S2:void

|

S1;S2:void5.3簡(jiǎn)單類(lèi)型檢查器的說(shuō)明定型規(guī)則——語(yǔ)句|S1735.3

簡(jiǎn)單類(lèi)型檢查器的說(shuō)明5.3.3

類(lèi)型檢查設(shè)計(jì)語(yǔ)法制導(dǎo)的類(lèi)型檢查器設(shè)計(jì)依據(jù)是上節(jié)的類(lèi)型系統(tǒng)類(lèi)型環(huán)境的信息進(jìn)入符號(hào)表對(duì)類(lèi)型表達(dá)式采用抽象語(yǔ)法 具體：array[N]ofT 抽象：array(N,T)

T

pointer(T)考慮到報(bào)錯(cuò)的需要，增加了類(lèi)型type_error5.3簡(jiǎn)單類(lèi)型檢查器的說(shuō)明5.3.3類(lèi)型檢查745.3

簡(jiǎn)單類(lèi)型檢查器的說(shuō)明5.3.3

類(lèi)型檢查——聲明語(yǔ)句D

D;DD

id

:T {addtype(id.entry,T.type)}

addtype：把類(lèi)型信息填入符號(hào)表5.3簡(jiǎn)單類(lèi)型檢查器的說(shuō)明5.3.3類(lèi)型檢查——聲明語(yǔ)句755.3

簡(jiǎn)單類(lèi)型檢查器的說(shuō)明5.3.3

類(lèi)型檢查——聲明語(yǔ)句D

D;DD

id

:T {addtype(id.entry,T.type)}T

boolean {T.type=boolean}T

integer

{T.type=integer}T

T1

{T.type=pointer(T1.type)}5.3簡(jiǎn)單類(lèi)型檢查器的說(shuō)明5.3.3類(lèi)型檢查——聲明語(yǔ)句765.3

簡(jiǎn)單類(lèi)型檢查器的說(shuō)明5.3.3

類(lèi)型檢查——聲明語(yǔ)句D

D;DD

id

:T {addtype(id.entry,T.type)}T

boolean {T.type=boolean}T

integer

{T.type=integer}T

T1

{T.type=pointer(T1.type)}T

array

[num]ofT1

{T.type=array(num.val,T1.type)}5.3簡(jiǎn)單類(lèi)型檢查器的說(shuō)明5.3.3類(lèi)型檢查——聲明語(yǔ)句775.3

簡(jiǎn)單類(lèi)型檢查器的說(shuō)明5.3.3

類(lèi)型檢查——聲明語(yǔ)句D

D;DD

id

:T {addtype(id.entry,T.type)}T

boolean {T.type=boolean}T

integer

{T.type=integer}T

T1

{T.type=pointer(T1.type)}T

array

[num]ofT1

{T.type=array(num.val,T1.type)}T

T1

‘

’T2

{T.type=T1.type

T2.type}5.3簡(jiǎn)單類(lèi)型檢查器的說(shuō)明5.3.3類(lèi)型檢查——聲明語(yǔ)句785.3

簡(jiǎn)單類(lèi)型檢查器的說(shuō)明類(lèi)型檢查——表達(dá)式E

truth

{E.type=boolean}E

num

{E.type=integer}E

id

{E.type=lookup(id.entry)}5.3簡(jiǎn)單類(lèi)型檢查器的說(shuō)明類(lèi)型檢查——表達(dá)式795.3

簡(jiǎn)單類(lèi)型檢查器的說(shuō)明類(lèi)型檢查——表達(dá)式E

truth

{E.type=boolean}E

num

{E.type=integer}E

id

{E.type=lookup(id.entry)}E

E1

modE2

{E.type=ifE1.type==integerand

E2.type==integertheninteger

elsetype_error}5.3簡(jiǎn)單類(lèi)型檢查器的說(shuō)明類(lèi)型檢查——表達(dá)式805.3

簡(jiǎn)單類(lèi)型檢查器的說(shuō)明類(lèi)型檢查——表達(dá)式E

E1[E2]{E.type=ifE2.type==integerand E1.type==array(s,t)thent elsetype_error}5.3簡(jiǎn)單類(lèi)型檢查器的說(shuō)明類(lèi)型檢查——表達(dá)式815.3

簡(jiǎn)單類(lèi)型檢查器的說(shuō)明類(lèi)型檢查——表達(dá)式E

E1[E2]{E.type=ifE2.type==integerand E1.type==array(s,t)thent elsetype_error}E

E1

{E.type=ifE1.type==pointer(t)thent elsetype_error}5.3簡(jiǎn)單類(lèi)型檢查器的說(shuō)明類(lèi)型檢查——表達(dá)式825.3

簡(jiǎn)單類(lèi)型檢查器的說(shuō)明類(lèi)型檢查——表達(dá)式E

E1[E2]{E.type=ifE2.type==integerand E1.type==array(s,t)thent elsetype_error}E

E1

{E.type=ifE1.type==pointer(t)thent elsetype_error}E

E1(E2){E.type=ifE2.type==sand E1.type==s

tthent

elsetype_error}5.3簡(jiǎn)單類(lèi)型檢查器的說(shuō)明類(lèi)型檢查——表達(dá)式835.3

簡(jiǎn)單類(lèi)型檢查器的說(shuō)明類(lèi)型檢查——語(yǔ)句S

id:=E{if

(id.type==E.type&&E.type

{boolean,integer})S.type=void;

elseS.type=type_error;}

5.3簡(jiǎn)單類(lèi)型檢查器的說(shuō)明類(lèi)型檢查——語(yǔ)句845.3

簡(jiǎn)單類(lèi)型檢查器的說(shuō)明類(lèi)型檢查——語(yǔ)句S

id:=E{if

(id.type==E.type&&E.type

{boolean,integer})S.type=void;

elseS.type=type_error;}

S

ifEthenS1{S.type=ifE.type==boolean thenS1.type elsetype_error}5.3簡(jiǎn)單類(lèi)型檢查器的說(shuō)明類(lèi)型檢查——語(yǔ)句855.3

簡(jiǎn)單類(lèi)型檢查器的說(shuō)明類(lèi)型檢查——語(yǔ)句S

whileEdoS1

{S.type=ifE.type==booleanthenS1.type

elsetype_error}5.3簡(jiǎn)單類(lèi)型檢查器的說(shuō)明類(lèi)型檢查——語(yǔ)句865.3

簡(jiǎn)單類(lèi)型檢查器的說(shuō)明類(lèi)型檢查——語(yǔ)句S

whileEdoS1

{S.type=ifE.type==booleanthenS1.type

elsetype_error}S

S1;S2

{S.type=ifS1.type==voidand S2.type==voidthenvoid

elsetype_error}5.3簡(jiǎn)單類(lèi)型檢查器的說(shuō)明類(lèi)型檢查——語(yǔ)句875.3

簡(jiǎn)單類(lèi)型檢查器的說(shuō)明類(lèi)型檢查——程序P

D;S

{P.type=ifS.type==voidthenvoid elsetype_error}5.3簡(jiǎn)單類(lèi)型檢查器的說(shuō)明類(lèi)型檢查——程序885.3

簡(jiǎn)單類(lèi)型檢查器的說(shuō)明5.3.4類(lèi)型轉(zhuǎn)換E

E1opE2{E.type= ifE1.type==integerandE2.type==integer theninteger elseifE1.type==integerandE2.type==real thenreal elseifE1.type==realandE2.type==integer thenreal

elseifE1.type==realandE2.type==real thenreal elsetype_error}5.3簡(jiǎn)單類(lèi)型檢查器的說(shuō)明5.3.4類(lèi)型轉(zhuǎn)換895.4

多態(tài)函數(shù)5.4.1為什么要使用多態(tài)函數(shù)例：用Pascal語(yǔ)言寫(xiě)不出求表長(zhǎng)度的通用程序typelink=

cell; cell=record info:integer; next:link end;5.4多態(tài)函數(shù)5.4.1為什么要使用多態(tài)函數(shù)905.4

多態(tài)函數(shù)functionlength(lptr:link):integer; varlen:integer; begin len:=0; whilelptr<>nildobegin len:=len+1; lptr:=lptr

.next end; length:=lenend;5.4多態(tài)函數(shù)functionlength(lpt915.4

多態(tài)函數(shù)用ML語(yǔ)言很容易寫(xiě)出求表長(zhǎng)度的程序而不必管表元的類(lèi)型。funlength(lptr)= ifnull(lptr)then0 elselength(tl(lptr))+1;5.4多態(tài)函數(shù)用ML語(yǔ)言很容易寫(xiě)出求表長(zhǎng)度的程序而不925.4

多態(tài)函數(shù)用ML語(yǔ)言很容易寫(xiě)出求表長(zhǎng)度的程序而不必管表元的類(lèi)型。funlength(lptr)= ifnull(lptr)then0 elselength(tl(lptr))+1;length([“sun”,“mon”,“tue”])length([10,9,8])都等于35.4多態(tài)函數(shù)用ML語(yǔ)言很容易寫(xiě)出求表長(zhǎng)度的程序而不935.4

多態(tài)函數(shù)多態(tài)函數(shù)允許變?cè)胁煌念?lèi)型5.4多態(tài)函數(shù)多態(tài)函數(shù)945.4

多態(tài)函數(shù)多態(tài)函數(shù)允許變?cè)胁煌念?lèi)型體中的語(yǔ)句可以在變?cè)?lèi)型不同的情況下執(zhí)行（區(qū)別于重載的特征）5.4多態(tài)函數(shù)多態(tài)函數(shù)955.4

多態(tài)函數(shù)多態(tài)函數(shù)允許變?cè)胁煌念?lèi)型體中的語(yǔ)句可以在變?cè)?lèi)型不同的情況下執(zhí)行（區(qū)別于重載的特征）多態(tài)算符用于以不同類(lèi)型的變?cè)獔?zhí)行的代碼段5.4多態(tài)函數(shù)多態(tài)函數(shù)965.4

多態(tài)函數(shù)多態(tài)函數(shù)允許變?cè)胁煌念?lèi)型體中的語(yǔ)句可以在變?cè)?lèi)型不同的情況下執(zhí)行（區(qū)別于重載的特征）多態(tài)算符用于以不同類(lèi)型的變?cè)獔?zhí)行的代碼段例如：數(shù)組索引5.4多態(tài)函數(shù)多態(tài)函數(shù)975.4

多態(tài)函數(shù)多態(tài)函數(shù)允許變?cè)胁煌念?lèi)型體中的語(yǔ)句可以在變?cè)?lèi)型不同的情況下執(zhí)行（區(qū)別于重載的特征）多態(tài)算符用于以不同類(lèi)型的變?cè)獔?zhí)行的代碼段例如：數(shù)組索引、函數(shù)作用5.4多態(tài)函數(shù)多態(tài)函數(shù)985.4

多態(tài)函數(shù)多態(tài)函數(shù)允許變?cè)胁煌念?lèi)型體中的語(yǔ)句可以在變?cè)?lèi)型不同的情況下執(zhí)行（區(qū)別于重載的特征）多態(tài)算符用于以不同類(lèi)型的變?cè)獔?zhí)行的代碼段例如：數(shù)組索引、函數(shù)作用、通過(guò)指針間接訪問(wèn)5.4多態(tài)函數(shù)多態(tài)函數(shù)995.4

多態(tài)函數(shù)多態(tài)函數(shù)允許變?cè)胁煌念?lèi)型體中的語(yǔ)句可以在變?cè)?lèi)型不同的情況下執(zhí)行（區(qū)別于重載的特征）多態(tài)算符用于以不同類(lèi)型的變?cè)獔?zhí)行的代碼段例如：數(shù)組索引、函數(shù)作用、通過(guò)指針間接訪問(wèn)C語(yǔ)言手冊(cè)中關(guān)于指針&的論述是：如果運(yùn)算對(duì)象的類(lèi)型是‘…’，那么結(jié)果類(lèi)型是指向‘…’的指針”5.4多態(tài)函數(shù)多態(tài)函數(shù)1005.4

多態(tài)函數(shù)5.4.2

類(lèi)型變量length的類(lèi)型可以寫(xiě)成

.list(

)

integer

允許使用類(lèi)型變量，還便于討論未知類(lèi)型在不要求標(biāo)識(shí)符的聲明先于使用的語(yǔ)言中，通過(guò)類(lèi)型變量的使用去確定程序變量的類(lèi)型5.4多態(tài)函數(shù)5.4.2類(lèi)型變量1015.4

多態(tài)函數(shù)例：functionderef(p); begin returnp

end; 5.4多態(tài)函數(shù)例：1025.4

多態(tài)函數(shù)例：functionderef(p); --對(duì)p的類(lèi)型一無(wú)所知：

begin returnp

end; 5.4多態(tài)函數(shù)例：1035.4

多態(tài)函數(shù)例：functionderef(p); --對(duì)p的類(lèi)型一無(wú)所知：

begin returnp --

=pointer(

)end; 5.4多態(tài)函數(shù)例：1045.4

多態(tài)函數(shù)例：functionderef(p); --對(duì)p的類(lèi)型一無(wú)所知：

begin returnp --

=pointer(

)end; deref的類(lèi)型是

.pointer(

)

5.4多態(tài)函數(shù)例：1055.4

多態(tài)函數(shù)5.4.3一個(gè)含多態(tài)函數(shù)的語(yǔ)言P

D;E 引入類(lèi)型變量、笛卡D

D;D|id:Q 兒積類(lèi)型、多態(tài)函數(shù)

Q

type-variable.Q|T T

T‘

’T|T

T |unary-constructor

(T) |basic-type |type-variable |(T)E

E(E)|E,E|id5.4多態(tài)函數(shù)5.4.3一個(gè)含多態(tài)函數(shù)的語(yǔ)言1065.4

多態(tài)函數(shù)5.4.3一個(gè)含多態(tài)函數(shù)的語(yǔ)言P

D;E 引入類(lèi)型變量、笛卡D

D;D|id:Q 兒積類(lèi)型、多態(tài)函數(shù)

Q

type-variable.Q|T T

T‘

’T|T

T 這是一個(gè)抽象語(yǔ)言, |unary-constructor

(T)忽略了函數(shù)定義的 |basic-type 函數(shù)體 |type-variable |(T)E

E(E)|E,E|id5.4多態(tài)函數(shù)5.4.3一個(gè)含多態(tài)函數(shù)的語(yǔ)言1075.4

多態(tài)函數(shù)5.4.3一個(gè)含多態(tài)函數(shù)的語(yǔ)言P

D;ED

D;D|id:QQ

type-variable.Q|TT

T‘

’T|T

T |unary-constructor

(T) 一個(gè)程序： |basic-type deref:

.pointer(

)

; |type-variableq:pointer(pointer(integer)); |(T) deref(deref(q))E

E(E)|E,E|id5.4多態(tài)函數(shù)5.4.3一個(gè)含多態(tài)函數(shù)的語(yǔ)言1085.4

多態(tài)函數(shù)類(lèi)型系統(tǒng)中增加的推理規(guī)則

環(huán)境規(guī)則

(EnvVar)語(yǔ)法規(guī)則(TypeVar)(TypeProduct)

|

,

dom(

)

,

|

1,

,

2|

1,

,

2|

|

T1,

|

T2

|

T1

T25.4多態(tài)函數(shù)類(lèi)型系統(tǒng)中增加的推理規(guī)則|1095.4

多態(tài)函數(shù)類(lèi)型系統(tǒng)中增加的推理規(guī)則

語(yǔ)法規(guī)則(TypeParenthesis)(TypeForall)(TypeFresh)

|

T

|

(T)

,

|

T

|

.T

|

.T,

,

i|

,

i

|

[

i

/

]T

5.4多態(tài)函數(shù)類(lèi)型系統(tǒng)中增加的推理規(guī)則|1105.4

多態(tài)函數(shù)類(lèi)型系統(tǒng)中增加的推理規(guī)則定型規(guī)則(ExpPair)(ExpFunCall)(S是T1和T3的最一般的合一代換)

|

E1:T1，|

E2:T2

|

E1,E2:T1

T2

|

E1:T1

T2,

|

E2:T3

|

E1(E2):S(T2)5.4多態(tài)函數(shù)類(lèi)型系統(tǒng)中增加的推理規(guī)則|E1115.4

多態(tài)函數(shù)5.4.4

代換、實(shí)例和合一代換:類(lèi)型表達(dá)式中的類(lèi)型變量用其所代表的類(lèi)型表達(dá)式去替換5.4多態(tài)函數(shù)5.4.4代換、實(shí)例和合一1125.4

多態(tài)函數(shù)5.4.4

代換、實(shí)例和合一代換:類(lèi)型表達(dá)式中的類(lèi)型變量用其所代表的類(lèi)型表達(dá)式去替換functionsubst(t:type_expression):

type_expression;begin ift是基本類(lèi)型thenreturnt elseift是類(lèi)型變量thenreturnS(t) elseift是t1

t2thenreturn

subst(t1)

subst(t2)end5.4多態(tài)函數(shù)5.4.4代換、實(shí)例和合一1135.4

多態(tài)函數(shù)實(shí)例

把subst函數(shù)用于t后所得的類(lèi)型表達(dá)式是t的一個(gè)實(shí)例，用S(t)表示。例子（s<t表示s是t的實(shí)例）pointer(integer)<pointer(

)pointer(real)<pointer(

)integer

integer<

pointer(

)<

<

5.4多態(tài)函數(shù)實(shí)例1145.4

多態(tài)函數(shù)下面左邊的類(lèi)型表達(dá)式不是右邊的實(shí)例integer real

代換不能用于基本類(lèi)型integer

real

的代換不一致integer

的所有出現(xiàn)都應(yīng)該代換5.4多態(tài)函數(shù)下面左邊的類(lèi)型表達(dá)式不是右邊的實(shí)例1155.4

多態(tài)函數(shù)合一

如果存在某個(gè)代換S使得S(t1)=S(t2)，那么這兩個(gè)表達(dá)式t1和t2能夠合一最一般的合一代換S(t1)=S(t2)；對(duì)任何其它滿(mǎn)足S

(t1)=S

(t2)的代換S

，代換S

(t1)是S(t1)的實(shí)例5.4多態(tài)函數(shù)合一1165.4

多態(tài)函數(shù)5.4.5多態(tài)函數(shù)的類(lèi)型檢查多態(tài)函數(shù)和普通函數(shù)在類(lèi)型檢查上的區(qū)別(1)同一多態(tài)函數(shù)的不同出現(xiàn)無(wú)須變?cè)邢嗤?lèi)型apply:

oderefo:pointer(

o)

oapply:

iderefi:pointer(

i)

iq:pointer(pointer(integer))deref(deref

(q))的帶標(biāo)記的語(yǔ)法樹(shù)5.4多態(tài)函數(shù)5.4.5多態(tài)函數(shù)的類(lèi)型檢查appl1175.4

多態(tài)函數(shù)(2)必須把類(lèi)型相同的概念推廣到類(lèi)型合一apply:

oderefo:pointer(

o)

oapply:

iderefi

:pointer(

i)

iq:pointer(pointer(integer))deref(deref

(q))的帶標(biāo)記的語(yǔ)法樹(shù)5.4多態(tài)函數(shù)(2)必須把類(lèi)型相同的概念推廣到類(lèi)型合1185.4

多態(tài)函數(shù)(2)必須把類(lèi)型相同的概念推廣到類(lèi)型合一(3)要記錄類(lèi)型表達(dá)式合一的結(jié)果apply:

oderefo:pointer(

o)

oapply:

iderefi

:pointer(

i)

iq:pointer(pointer(integer))deref(deref

(q))的帶標(biāo)記的語(yǔ)法樹(shù)5.4多態(tài)函數(shù)(2)必須把類(lèi)型相同的概念推廣到類(lèi)型合1195.4

多態(tài)函數(shù)檢查多態(tài)函數(shù)的翻譯方案E

E1(E2) {p=mkleaf(newtypevar); unify(E1.type,mknode(‘

’,E2.type,p));

E.type=p}E

E1,E2

{E.type=mknode(‘

’,E1.type,E2.type)}E

id {E.type=fresh(lookup(id.entry))}5.4多態(tài)函數(shù)檢查多態(tài)函數(shù)的翻譯方案1205.4

多態(tài)函數(shù)apply:

oderefo:pointer(

o)

oapply:

iderefi

:pointer(

i)

iq:pointer(pointer(integer))表

達(dá)

式

：

類(lèi)

型

代

換

q:pointer(pointer(integer))derefi:pointer(

i)

i

derefi(q):pointer(integer)

i=pointer(integer)derefo:pointer(

o)

o

derefo(derefi(q)):integer

o=integer

5.4多態(tài)函數(shù)apply:oderefo:poi1215.4

多態(tài)函數(shù)確定表長(zhǎng)度的ML函數(shù)funlength(lptr)= ifnull(lptr)then0 elselength(tl(lptr))+1;5.4多態(tài)函數(shù)確定表長(zhǎng)度的ML函數(shù)1225.4

多態(tài)函數(shù)length:

; lptr:

;if:

.boolean

;null:

.list(

)

boolean;tl:

.list(

)

list(

);0:integer;1:integer;+:integer

integer

integer;match:

.

;match( length(lptr), if(null(lptr),0,length(tl(lptr))+1))5.4多態(tài)函數(shù)length:; lptr1235.4

多態(tài)函數(shù)行

定

型

斷

言

代

換

規(guī)

則

(1)lptr:

(ExpId)

(2)length:

(ExpId)

(3)length(lptr):

=

(ExpFunCall)

(4)lptr:

從(1)可得

(5)null:list(

n)

boolean

(ExpId)和(TypeFresh)

(6)null(lptr):boolean

=list(

n)(ExpFunCall)

(7)0:integer

(ExpNum)

(8)lptr:list(

n)從(1)可得

5.4多態(tài)函數(shù)行定型斷言代換規(guī)1245.4

多態(tài)函數(shù)行

定

型

斷

言

代

換

規(guī)

則

(9)tl:list(

t)

list(

t)(ExpId)和(TypeFresh)(10)tl(lptr):list(

n)

t=

n

(ExpFunCall)(11)length:list(

n)

從(2)可得

(12)length(tl(lptr)):

(ExpFunCall)

(13)1:integer

(ExpNum)(14)+:integer

integer

integer

(ExpId)5.4多態(tài)函數(shù)行定型斷言代換規(guī)1255.4

多態(tài)函數(shù)行

定

型

斷

言

代

換

規(guī)

則

(15)

length(tl(lptr))+1:

integer

=integer

(ExpFunCall)(16)if:boolean

i

i

i

(ExpId)和(TypeFresh)(17)if(...):integer

i=integer

(ExpFunCall)(18)match:

m

m

m

(ExpId)和(TypeFresh)

(19)match(…):integer

m=integer

(ExpFunCall)5.4多態(tài)函數(shù)行定型斷言代換規(guī)1265.4

多態(tài)函數(shù)funlength(lptr)= ifnull(lptr)then0 elselength(tl(lptr))+1;length函數(shù)的類(lèi)型是

.list(

)

integer

5.4多態(tài)函數(shù)funlength(lptr)=1275.5

類(lèi)型表達(dá)式的等價(jià)當(dāng)允許對(duì)類(lèi)型表達(dá)式命名后：類(lèi)型表達(dá)式是否相同就有了不同的解釋出現(xiàn)了結(jié)構(gòu)等價(jià)和名字等價(jià)兩個(gè)不同的概念typelink=

cell;var next :link; last :link; p :

cell; q,r :

cell;5.5類(lèi)型表達(dá)式的等價(jià)當(dāng)允許對(duì)類(lèi)型表達(dá)式命名后：1285.5

類(lèi)型表達(dá)式的等價(jià)5.5.1類(lèi)型表達(dá)式的結(jié)構(gòu)等價(jià)兩個(gè)類(lèi)型表達(dá)式完全相同（當(dāng)無(wú)類(lèi)型名時(shí)）typelink=

cell;var next :link; last :link; p :

cell; q,r :

cell;5.5類(lèi)型表達(dá)式的等價(jià)5.5.1類(lèi)型表達(dá)式的結(jié)構(gòu)等價(jià)1295.5

類(lèi)型表達(dá)式的等價(jià)5.5.1類(lèi)型表達(dá)式的結(jié)構(gòu)等價(jià)兩個(gè)類(lèi)型表達(dá)式完全相同（當(dāng)無(wú)類(lèi)型名時(shí)）類(lèi)型表達(dá)式樹(shù)一樣typelink=

cell;var next :link; last :link; p :

cell; q,r :

cell;5.5類(lèi)型表達(dá)式的等價(jià)5.5.1類(lèi)型表達(dá)式的結(jié)構(gòu)等價(jià)1305.5

類(lèi)型表達(dá)式的等價(jià)5.5.1類(lèi)型表達(dá)式的結(jié)構(gòu)等價(jià)兩個(gè)類(lèi)型表達(dá)式完全相同（當(dāng)無(wú)類(lèi)型名時(shí)）類(lèi)型表達(dá)式樹(shù)一樣相同的類(lèi)型構(gòu)造符作用于相同的子表達(dá)式typelink=

cell;var next :link; last :link; p :

cell; q,r :

cell;5.5類(lèi)型表達(dá)式的等價(jià)5.5.1類(lèi)型表達(dá)式的結(jié)構(gòu)等價(jià)1315.5

類(lèi)型表達(dá)式的等價(jià)5.5.1類(lèi)型表達(dá)式的結(jié)構(gòu)等價(jià)兩個(gè)類(lèi)型表達(dá)式完全相同（當(dāng)無(wú)類(lèi)型名時(shí)）把類(lèi)型名都用它們定義的類(lèi)型表達(dá)式代換，所得兩類(lèi)型表達(dá)式完全相同(類(lèi)型定義無(wú)環(huán)時(shí))typelink=

cell;var next :link; last :link; p :

cell; q,r :

cell;5.5類(lèi)型表達(dá)式的等價(jià)5.5.1類(lèi)型表達(dá)式的結(jié)構(gòu)等價(jià)1325.5

類(lèi)型表達(dá)式的等價(jià)類(lèi)型表達(dá)式的結(jié)構(gòu)等價(jià)測(cè)試sequiv(s,t)(無(wú)類(lèi)型名時(shí))ifs

和t

是相同的基本類(lèi)型then returntrueelseifs==array(s1,s2)andt==array(t1,t2)then returnsequiv(s1,t1)andsequiv(s2,t2)elseifs==s1

s2andt==t1

t2then returnsequiv(s1,t1)andsequiv(s2,t2)elseifs==pointer(s1)andt==pointer(t1)then returnsequiv(s1,t1)elseifs==s1

s2andt==t1

t2then returnsquiv(s1,t1)andsequiv(s2,t2)elsereturnfalse5.5類(lèi)型表達(dá)式的等價(jià)類(lèi)型表達(dá)式的結(jié)構(gòu)等價(jià)測(cè)試sequi1335.5

類(lèi)型表達(dá)式的等價(jià)5.5.2類(lèi)型表達(dá)式的名字等價(jià)把每個(gè)類(lèi)型名看成是一個(gè)可區(qū)別的類(lèi)型typelink=

cell;var next :link; last :link; p :

cell; q,r :

cell;5.5類(lèi)型表達(dá)式的等價(jià)5.5.2類(lèi)型表達(dá)式的名字等價(jià)1345.5

類(lèi)型表達(dá)式的等價(jià)5.5.2