形式語(yǔ)義學(xué)程序設(shè)計(jì)語(yǔ)言原理課件

1、2022/8/71形式語(yǔ)義學(xué)Formal Semantics本PPT參考了金英老師的課程內(nèi)容2022/8/722022/8/73代數(shù)語(yǔ)義學(xué)理論基礎(chǔ)函數(shù)式描述方法程序設(shè)計(jì)語(yǔ)言形式語(yǔ)義指稱語(yǔ)義學(xué)操作語(yǔ)義學(xué)公理語(yǔ)義學(xué)代數(shù)功能執(zhí)行邏輯 關(guān)系模型2022/8/74離散數(shù)學(xué)程序設(shè)計(jì)語(yǔ)言形式語(yǔ)義編譯原理程序設(shè)計(jì)語(yǔ)言理論基礎(chǔ)語(yǔ)義形式化語(yǔ)法形式化2022/8/75軟件開發(fā)方法程序設(shè)計(jì)語(yǔ)言形式語(yǔ)義程序設(shè)計(jì)方法程序設(shè)計(jì)語(yǔ)言理解抽象能力Formal MethodFormal SpecificationFormal Verification2022/8/76前言：“形式語(yǔ)義學(xué)”概述What？形式語(yǔ)義學(xué)：給出對(duì)(形式)語(yǔ)

2、言及其程序采用形式系統(tǒng)方法進(jìn)行語(yǔ)義定義的方法。分類：從不同的角度研究程序的含義操作語(yǔ)義學(xué)（執(zhí)行）指稱語(yǔ)義學(xué)（功能）公理語(yǔ)義學(xué)（邏輯）代數(shù)語(yǔ)義學(xué)（代數(shù)，抽象數(shù)據(jù)結(jié)構(gòu)）其他2022/8/77Lambda演算2022/8/78關(guān)于Lambda演算表達(dá)式自由變量（計(jì)算一個(gè)表達(dá)式的自由變量集合） 替換（計(jì)算） 變換規(guī)則 （三種變換）歸約 范式（性質(zhì)及其計(jì)算）2022/8/79關(guān)于Lambda演算表達(dá)式 一個(gè)表達(dá)式由變量名、抽象符號(hào)，.以及括號(hào)等符號(hào)構(gòu)成， 其語(yǔ)法為： := | | . | ( )2022/8/710關(guān)于Lambda演算變換規(guī)則 （三種變換）變換：設(shè)E是表達(dá)式，x是變量，則稱下面變換為變換

3、（其中y不在 FV( x.E )中） x.E - y.y/x E 變換：設(shè) (x.E)和E0為表達(dá)式，則稱下面變換為變換（稱變換規(guī)則的左部表達(dá)式為基） (x.E)E0 EE0/x變換：假設(shè)x.Mx是一個(gè)表達(dá)式，且滿足條件xFV(M)，則稱下面變換為變換: (x.M x) M 2022/8/711關(guān)于Lambda演算自由變量（計(jì)算一個(gè)表達(dá)式的自由變量集合） 表達(dá)式E中變量名x的一次出現(xiàn)稱為自由出現(xiàn)，如果E中任何一個(gè)形如x. E的子表達(dá)式包含該出現(xiàn)；y (x y. y (x. x y ) ) (z (x. x x) )的自由變量集合y, z替換（計(jì)算） 設(shè)E和E0是表達(dá)式，x是變量名，替換EE0/

4、x是表示 把E中的所有x的自由出現(xiàn)替換成E0。需要明確變量的自由出現(xiàn)計(jì)算規(guī)則( y. x+y) y/x = z. y+z2022/8/712關(guān)于Lambda演算范式（性質(zhì)及其計(jì)算）假設(shè)E是一個(gè)表達(dá)式，且其中沒有任何一個(gè)歸約基，則稱該表達(dá)式為范式。范式的存在性：如果有范式，則最左歸約法一定能求出范式。范式的唯一性：如果有范式則在變換下一定唯一。2022/8/713函數(shù)式描述方法2022/8/714關(guān)于函數(shù)式描述方法函數(shù)式語(yǔ)言的特點(diǎn)引用透明性；高階性；模式匹配；并行性；函數(shù)式語(yǔ)言的組成部分程序結(jié)構(gòu)類型及其操作表達(dá)式用函數(shù)式語(yǔ)言來(lái)描述算法（解釋器）函數(shù)空間函數(shù)定義（方程）2022/8/715關(guān)于函數(shù)

5、式描述方法函數(shù)式語(yǔ)言的組成部分程序結(jié)構(gòu)函數(shù)定義目標(biāo)表達(dá)式類型及其操作標(biāo)準(zhǔn)類型 - 集合類型冪集類型 - 元組類型聯(lián)合類型 - 序列類型函數(shù)類型 - 遞歸類型抽象類型2022/8/716關(guān)于函數(shù)式描述方法函數(shù)式語(yǔ)言的組成部分表達(dá)式非let表達(dá)式（常量，變量，表達(dá)式，條件表達(dá)式，以及各種操作） let表達(dá)式 let x = E in E letrec表達(dá)式 letrec x = E1 in E在表達(dá)式中增加類型說(shuō)明 2022/8/717關(guān)于函數(shù)式描述方法用函數(shù)式語(yǔ)言來(lái)描述算法函數(shù)空間：INT* INT BOOL函數(shù)定義（方程） lookup L a = (null LFALSE， a=hd LTR

6、UE，lookup (tl L) a )2022/8/718操作語(yǔ)義學(xué)2022/8/7192022/8/720操作語(yǔ)義學(xué)三種方法解釋器方法抽象機(jī)歸約方法（歸約系統(tǒng)）從實(shí)現(xiàn)的角度，通過(guò)程序的執(zhí)行過(guò)程來(lái)定義程序設(shè)計(jì)語(yǔ)言的語(yǔ)義；2022/8/721操作語(yǔ)義學(xué)抽象機(jī)方法2022/8/722主要思想：針對(duì)計(jì)算機(jī)語(yǔ)言，定義一個(gè)抽象機(jī)來(lái)解釋執(zhí)行將該語(yǔ)言的程序；抽象機(jī)的定義包括兩個(gè)部分：抽象機(jī)組成的抽象定義 狀態(tài)結(jié)構(gòu)執(zhí)行機(jī)制的形式定義 - 狀態(tài)轉(zhuǎn)換規(guī)則針對(duì)如下語(yǔ)言結(jié)構(gòu)給出抽象機(jī)定義表達(dá)式語(yǔ)句輸入輸出聲明Block過(guò)程/函數(shù)2022/8/723狀態(tài)結(jié)構(gòu)（形式定義）棧（保存中間計(jì)算結(jié)果）語(yǔ)句控制區(qū)表達(dá)式控制區(qū)靜態(tài)

7、環(huán)境區(qū)動(dòng)態(tài)環(huán)境去堆區(qū)（保存中斷現(xiàn)場(chǎng)）初始狀態(tài)和終止?fàn)顟B(tài)狀態(tài)轉(zhuǎn)換規(guī)則針對(duì)每個(gè)語(yǔ)法結(jié)構(gòu)給出執(zhí)行過(guò)程狀態(tài)到狀態(tài)的映射基于抽象機(jī)的操作語(yǔ)義的定義過(guò)程2022/8/724操作語(yǔ)義學(xué)歸約方法2022/8/725歸約方法的主要思想：一種結(jié)構(gòu)化方法（只依賴于成分的結(jié)果）根據(jù)語(yǔ)言的成分給出歸約系統(tǒng)的方法歸約系統(tǒng)是由以下部分組成的：一組歸約公理一組推理規(guī)則，稱為歸約規(guī)則歸約的對(duì)象為格局（configuration），歸約的結(jié)果也是格局；初始格局和終止格局；2022/8/726基于歸約方法的操作語(yǔ)義的定義過(guò)程格局的形式：，通過(guò)模式給出初始格局和終止格局一組歸約公理：configure1 configure2 一組歸

8、約規(guī)則形： A1,An 條件公理configure1 configure2 推導(dǎo)出的公理其中A1,An是關(guān)于configure1中成分的公理，而configure2中的成分只能從configure1和A1,An中的結(jié)果格局中得到；2022/8/7272022/8/7282022/8/7292022/8/7302022/8/7312022/8/732指稱語(yǔ)義學(xué)2022/8/7332022/8/734指稱語(yǔ)義學(xué)直接指稱語(yǔ)義兩個(gè)方面定義指稱語(yǔ)義（五個(gè)部分）完整語(yǔ)言 某個(gè)語(yǔ)法單位給出具體語(yǔ)法元素的指稱語(yǔ)義解釋（語(yǔ)義函數(shù)）根據(jù)該語(yǔ)法元素所屬的語(yǔ)法域的具體的語(yǔ)義指派函數(shù)；確定已知條件（靜態(tài)環(huán)境，動(dòng)態(tài)環(huán)境）

9、給出語(yǔ)義解釋（函數(shù)；值）2022/8/735直接指稱語(yǔ)義主要原理：從功能角度出發(fā)，對(duì)每一個(gè)語(yǔ)法單位（如程序、聲明、語(yǔ)句、表達(dá)式、變量、整數(shù)、標(biāo)識(shí)符等），給出其功能的嚴(yán)格形式化描述，即定義功能函數(shù)；功能函數(shù)是描述一個(gè)語(yǔ)法單位的語(yǔ)義，因此稱為語(yǔ)義函數(shù)（語(yǔ)義物）；本質(zhì)上是建立語(yǔ)法域到語(yǔ)義函數(shù)域的映射；語(yǔ)法域語(yǔ)義函數(shù)域語(yǔ)義指派函數(shù)2022/8/736直接指稱語(yǔ)義直接指稱語(yǔ)義的定義包括：語(yǔ)法域 （Syntax Domain）抽象語(yǔ)法 （Abstract Syntax）語(yǔ)義域 （Semantic Domain）語(yǔ)義函數(shù) （Semantic Functions）預(yù)定義函數(shù) （Predefined Funct

10、ions）關(guān)鍵：掌握好每個(gè)語(yǔ)法單位的功能；語(yǔ)言不一樣，相同的語(yǔ)法單位其語(yǔ)義也不盡相同；2022/8/737過(guò)程式語(yǔ)言的直接指稱語(yǔ)義語(yǔ)法域（根據(jù)語(yǔ)言定義應(yīng)給出具體定義）程序聲明（還可以細(xì)化）語(yǔ)句Block表達(dá)式常量類型2022/8/738過(guò)程式語(yǔ)言的直接指稱語(yǔ)義語(yǔ)義域（根據(jù)語(yǔ)言定義應(yīng)給出具體定義）環(huán)境域 靜態(tài)環(huán)境動(dòng)態(tài)環(huán)境值域存儲(chǔ)域2022/8/739過(guò)程式語(yǔ)言的直接指稱語(yǔ)義語(yǔ)義函數(shù)針對(duì)每個(gè)語(yǔ)法單位語(yǔ)義指派函數(shù)空間針對(duì)每個(gè)語(yǔ)法單位定義語(yǔ)義指派函數(shù)針對(duì)每個(gè)語(yǔ)法單位中的每種語(yǔ)法元素，定義相應(yīng)的語(yǔ)義方程2022/8/740公理語(yǔ)義學(xué)2022/8/741主要思想公理語(yǔ)義學(xué)是基于謂詞邏輯中的邏輯歸納方法，一

11、個(gè)程序的語(yǔ)義是建立在每次程序運(yùn)行時(shí)都成立的關(guān)于變量的值之間關(guān)系的斷言；定義過(guò)程為計(jì)算機(jī)語(yǔ)言建立一個(gè)公理系統(tǒng)公理系統(tǒng)由兩部分組成：（1）一組公理；（2）一組推理規(guī)則局限性2022/8/7422022/8/7432022/8/7442022/8/7452022/8/7462022/8/747Hoare 公理系統(tǒng)2022/8/748公理和命題的形式： P S Q 推理規(guī)則的形式 Hoare公理系統(tǒng)由五條規(guī)則賦值公理復(fù)合推理規(guī)則條件推理規(guī)則循環(huán)推理規(guī)則推論規(guī)則F1， , FnF2022/8/749最弱前置條件和最強(qiáng)后置條件2022/8/750最弱前置條件的計(jì)算規(guī)則求WP(S,q)WP(skip,q)

12、= q;WP(x:=e,q) = qe/x;WP(s1;s2,q) = WP(s1,WP(s2,q);WP(if(e,s1,s2),q) = (e WP(s1,q) (e WP(s2,q) 為什么沒有給出while語(yǔ)句的WP求法？比較復(fù)雜2022/8/751最強(qiáng)后置條件的計(jì)算規(guī)則求SP(p,S)SP(p,skip) = p;SP(p,x:=e) = x(px/x x=ex/x);SP(p,s1;s2) = SP(SP(s1,p),s2);SP(p,if(e,s1,s2) = (SP(pe,s1) SP(pe,s2)2022/8/752程序正確性證明2022/8/753程序正確性證明程序正確性證明目的證明驗(yàn)