1、第第5章章 類型和效果系統(tǒng)類型和效果系統(tǒng) 內(nèi)容概述內(nèi)容概述 先前介紹的技術(shù)可用于類型語言和非類型語言先前介紹的技術(shù)可用于類型語言和非類型語言 本章討論如何利用類型上的標(biāo)注來表達(dá)感興趣的本章討論如何利用類型上的標(biāo)注來表達(dá)感興趣的程序分析的性質(zhì)，在類型檢查時(shí)完成這樣的分析程序分析的性質(zhì)，在類型檢查時(shí)完成這樣的分析 首先用加標(biāo)注的類型系統(tǒng)來討論控制流分析及其首先用加標(biāo)注的類型系統(tǒng)來討論控制流分析及其語義可靠性和其它理論性質(zhì)語義可靠性和其它理論性質(zhì) 然后討論計(jì)算加標(biāo)注類型的算法，包括算法的可然后討論計(jì)算加標(biāo)注類型的算法，包括算法的可靠性和完備性靠性和完備性 最后給出一些用類型和效果系統(tǒng)來規(guī)范的其它例最

2、后給出一些用類型和效果系統(tǒng)來規(guī)范的其它例子：副作用分析、異常分析、區(qū)域推導(dǎo)、通信分子：副作用分析、異常分析、區(qū)域推導(dǎo)、通信分析析第第5章章 類型和效果系統(tǒng)類型和效果系統(tǒng) 類型和效果系統(tǒng)概要類型和效果系統(tǒng)概要 效果系統(tǒng)和加標(biāo)注的類型系統(tǒng)的融合效果系統(tǒng)和加標(biāo)注的類型系統(tǒng)的融合 在效果系統(tǒng)中，斷言的典型形式在效果系統(tǒng)中，斷言的典型形式e : 1 2其中其中 告知告知e運(yùn)行時(shí)發(fā)生的事情，例如什么東西運(yùn)行時(shí)發(fā)生的事情，例如什么東西被修改、引發(fā)異常被修改、引發(fā)異常 加標(biāo)注的類型系統(tǒng)用來表達(dá)語言構(gòu)造的類型上的加標(biāo)注的類型系統(tǒng)用來表達(dá)語言構(gòu)造的類型上的標(biāo)注和它子構(gòu)造的類型上的標(biāo)注之間的關(guān)系標(biāo)注和它子構(gòu)造的類型

3、上的標(biāo)注之間的關(guān)系 第第5章章 類型和效果系統(tǒng)類型和效果系統(tǒng)5.1 控制流分析控制流分析以控制流分析為例來介紹加標(biāo)注的類型系統(tǒng)以控制流分析為例來介紹加標(biāo)注的類型系統(tǒng) 介紹介紹FUN語言及其類型系統(tǒng)語言及其類型系統(tǒng) 加標(biāo)注的類型斷言加標(biāo)注的類型斷言 加標(biāo)注的類型系統(tǒng)加標(biāo)注的類型系統(tǒng)關(guān)注計(jì)算到函數(shù)抽象的每個(gè)子表達(dá)式的值關(guān)注計(jì)算到函數(shù)抽象的每個(gè)子表達(dá)式的值 標(biāo)注的等價(jià)標(biāo)注的等價(jià)第第5章章 類型和效果系統(tǒng)類型和效果系統(tǒng)5.2 理論上的性質(zhì)理論上的性質(zhì) 操作語義：無環(huán)境的自然語義操作語義：無環(huán)境的自然語義 語義的正確性語義的正確性用類型系統(tǒng)得出某表達(dá)式的類型是用類型系統(tǒng)得出某表達(dá)式的類型是 ，則該表達(dá)，

4、則該表達(dá)式在操作語義下求得的值的類型也是式在操作語義下求得的值的類型也是 程序分析的解的存在性程序分析的解的存在性1、定義標(biāo)注完全格、定義標(biāo)注完全格2、再定義標(biāo)注類型的完全格、再定義標(biāo)注類型的完全格3、擦掉標(biāo)注后是同樣定型斷言的加標(biāo)注定型斷、擦掉標(biāo)注后是同樣定型斷言的加標(biāo)注定型斷言集合構(gòu)成一個(gè)言集合構(gòu)成一個(gè)Moore family第第5章章 類型和效果系統(tǒng)類型和效果系統(tǒng)5.3 推斷算法推斷算法 利用前面的推理系統(tǒng)：需要使用者有足夠的遠(yuǎn)見利用前面的推理系統(tǒng)：需要使用者有足夠的遠(yuǎn)見來猜測(cè)適當(dāng)?shù)念愋图捌渖系臉?biāo)注來猜測(cè)適當(dāng)?shù)念愋图捌渖系臉?biāo)注 利用推斷算法：利用一種試探性的猜測(cè)（使用標(biāo)利用推斷算法：利用

5、一種試探性的猜測(cè)（使用標(biāo)注變量）而后再被精確化（對(duì)變量進(jìn)行代換）的注變量）而后再被精確化（對(duì)變量進(jìn)行代換）的機(jī)制機(jī)制 基礎(chǔ)類型系統(tǒng)的算法基礎(chǔ)類型系統(tǒng)的算法 控制流分析的算法控制流分析的算法 語法上的可靠性和完備性語法上的可靠性和完備性第第5章章 類型和效果系統(tǒng)類型和效果系統(tǒng)5.4 效果效果 列舉一些更復(fù)雜、功能更強(qiáng)的類型和效果系統(tǒng)列舉一些更復(fù)雜、功能更強(qiáng)的類型和效果系統(tǒng) 它們是：副作用分析、異常分析、區(qū)域推導(dǎo)它們是：副作用分析、異常分析、區(qū)域推導(dǎo) 除了使用子效果外，需要使用子定型、除了使用子效果外，需要使用子定型、let多態(tài)和多態(tài)和多態(tài)遞歸多態(tài)遞歸 實(shí)現(xiàn)技術(shù)也相應(yīng)地變得復(fù)雜實(shí)現(xiàn)技術(shù)也相應(yīng)地變得

6、復(fù)雜第第5章章 類型和效果系統(tǒng)類型和效果系統(tǒng)5.4.1 副作用分析副作用分析 對(duì)每個(gè)表達(dá)式，分析哪些存儲(chǔ)單元被創(chuàng)建、賦值對(duì)每個(gè)表達(dá)式，分析哪些存儲(chǔ)單元被創(chuàng)建、賦值和讀取和讀取 FUN語言增加賦值語句語言增加賦值語句 形式語義形式語義 為副作用分析設(shè)計(jì)帶標(biāo)注的類型系統(tǒng)為副作用分析設(shè)計(jì)帶標(biāo)注的類型系統(tǒng) 舉例舉例第第5章章 類型和效果系統(tǒng)類型和效果系統(tǒng)5.4.2 異常分析異常分析 對(duì)每個(gè)表達(dá)式，分析會(huì)引發(fā)哪些異常對(duì)每個(gè)表達(dá)式，分析會(huì)引發(fā)哪些異常 FUN語言增加和異常有關(guān)的語句語言增加和異常有關(guān)的語句 形式語義形式語義 為異常分析設(shè)計(jì)帶標(biāo)注的類型系統(tǒng)為異常分析設(shè)計(jì)帶標(biāo)注的類型系統(tǒng) 舉例舉例第第5章章

7、類型和效果系統(tǒng)類型和效果系統(tǒng)5.4.3 區(qū)域推理區(qū)域推理 分析存放值的區(qū)域什么時(shí)候可以回收，以便決定分析存放值的區(qū)域什么時(shí)候可以回收，以便決定將它們分配在棧上還是堆上將它們分配在棧上還是堆上 FUN語言增加顯式的區(qū)域信息（存儲(chǔ)分配信息）語言增加顯式的區(qū)域信息（存儲(chǔ)分配信息） 形式語義形式語義 為區(qū)域分析設(shè)計(jì)的推理系統(tǒng)為區(qū)域分析設(shè)計(jì)的推理系統(tǒng) 舉例舉例第第5章章 類型和效果系統(tǒng)類型和效果系統(tǒng)5.5 運(yùn)行行為運(yùn)行行為用類型和效果系統(tǒng)來分析運(yùn)行時(shí)原子動(dòng)作的時(shí)序用類型和效果系統(tǒng)來分析運(yùn)行時(shí)原子動(dòng)作的時(shí)序特點(diǎn)特點(diǎn)具體分析并發(fā)程序的通信行為：進(jìn)程創(chuàng)建、通道具體分析并發(fā)程序的通信行為：進(jìn)程創(chuàng)建、通道分配、通道上發(fā)送和接受數(shù)據(jù)