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

2023/9/181形式語義學(xué)

FormalSemantics本PPT參考了金英老師的課程內(nèi)容2023/8/61形式語義學(xué)

FormalSemantic2023/9/1822023/8/622023/9/183代數(shù)語義學(xué)理論基礎(chǔ)函數(shù)式描述方法程序設(shè)計(jì)語言形式語義指稱語義學(xué)操作語義學(xué)公理語義學(xué)代數(shù)功能執(zhí)行邏輯

關(guān)系模型2023/8/63代數(shù)語義學(xué)理論基礎(chǔ)函數(shù)式描述方法程序設(shè)計(jì)語2023/9/184離散數(shù)學(xué)程序設(shè)計(jì)語言形式語義編譯原理程序設(shè)計(jì)語言理論基礎(chǔ)語義形式化語法形式化2023/8/64離散數(shù)學(xué)程序設(shè)計(jì)語言編譯原理程序設(shè)計(jì)語言理2023/9/185軟件開發(fā)方法程序設(shè)計(jì)語言形式語義程序設(shè)計(jì)方法程序設(shè)計(jì)語言理解抽象能力FormalMethodFormalSpecificationFormalVerification2023/8/65軟件開發(fā)方法程序設(shè)計(jì)語言程序設(shè)計(jì)方法程序設(shè)2023/9/186前言：“形式語義學(xué)”概述What？形式語義學(xué)：給出對(形式)語言及其程序采用形式系統(tǒng)方法進(jìn)行語義定義的方法。分類：從不同的角度研究程序的含義操作語義學(xué)（執(zhí)行）指稱語義學(xué)（功能）公理語義學(xué)（邏輯）代數(shù)語義學(xué)（代數(shù)，抽象數(shù)據(jù)結(jié)構(gòu)）其他2023/8/66前言：“形式語義學(xué)”概述What？2023/9/187Lambda演算2023/8/67Lambda演算2023/9/188關(guān)于Lambda演算

表達(dá)式自由變量（計(jì)算一個表達(dá)式的自由變量集合）替換（計(jì)算）變換規(guī)則（三種變換）歸約范式（性質(zhì)及其計(jì)算）2023/8/68關(guān)于Lambda演算表達(dá)式2023/9/189關(guān)于Lambda演算

表達(dá)式

一個表達(dá)式由變量名、抽象符號，.以及括號等符號構(gòu)成，其語法為：

<表達(dá)式>::=<變量名> |<表達(dá)式><表達(dá)式>|<變量名>.<表達(dá)式>|(<表達(dá)式>)2023/8/69關(guān)于Lambda演算表達(dá)式2023/9/1810關(guān)于Lambda演算變換規(guī)則（三種變換）變換：設(shè)E是表達(dá)式，x是變量，則稱下面變換為α變換（其中y不在FV(x.E)中）

x.E------〉y.[y/x]E

變換：設(shè)(x.E)和E0為表達(dá)式，則稱下面變換為β變換（稱β變換規(guī)則的左部表達(dá)式為β基）

(x.E)E0E[E0/x]

變換：假設(shè)x.Mx是一個表達(dá)式，且滿足條件xFV(M)，則稱下面變換為η變換:(x.Mx)M

2023/8/610關(guān)于Lambda演算變換規(guī)則（三種變換2023/9/1811關(guān)于Lambda演算自由變量（計(jì)算一個表達(dá)式的自由變量集合）表達(dá)式E中變量名x的一次出現(xiàn)稱為自由出現(xiàn)，如果E中任何一個形如x.E’的子表達(dá)式包含該出現(xiàn)；y(xy.y(x.xy))(z(x.xx))的自由變量集合{y,z}替換（計(jì)算） 設(shè)E和E0是表達(dá)式，x是變量名，替換E[E0/x]是表示把E中的所有x的自由出現(xiàn)替換成E0。需要明確變量的自由出現(xiàn)計(jì)算規(guī)則(y.x+y)[y/x]=z.y+z2023/8/611關(guān)于Lambda演算自由變量（計(jì)算一個2023/9/1812關(guān)于Lambda演算范式（性質(zhì)及其計(jì)算）假設(shè)E是一個表達(dá)式，且其中沒有任何一個歸約基，則稱該表達(dá)式為范式。范式的存在性：如果有范式，則最左歸約法一定能求出范式。范式的唯一性：如果有范式則在變換下一定唯一。2023/8/612關(guān)于Lambda演算范式（性質(zhì)及其計(jì)算）2023/9/1813函數(shù)式描述方法2023/8/613函數(shù)式描述方法2023/9/1814關(guān)于函數(shù)式描述方法函數(shù)式語言的特點(diǎn)引用透明性；高階性；模式匹配；并行性；函數(shù)式語言的組成部分程序結(jié)構(gòu)類型及其操作表達(dá)式用函數(shù)式語言來描述算法（解釋器）函數(shù)空間函數(shù)定義（方程）2023/8/614關(guān)于函數(shù)式描述方法函數(shù)式語言的特點(diǎn)2023/9/1815關(guān)于函數(shù)式描述方法函數(shù)式語言的組成部分程序結(jié)構(gòu)函數(shù)定義目標(biāo)表達(dá)式類型及其操作標(biāo)準(zhǔn)類型-集合類型冪集類型-元組類型聯(lián)合類型-序列類型函數(shù)類型-遞歸類型抽象類型2023/8/615關(guān)于函數(shù)式描述方法函數(shù)式語言的組成部分2023/9/1816關(guān)于函數(shù)式描述方法函數(shù)式語言的組成部分表達(dá)式非let表達(dá)式（常量，變量，表達(dá)式，條件表達(dá)式，以及各種操作）let表達(dá)式

letx=E’

inEletrec表達(dá)式

letrecx=E1

inE在表達(dá)式中增加類型說明

2023/8/616關(guān)于函數(shù)式描述方法函數(shù)式語言的組成部分2023/9/1817關(guān)于函數(shù)式描述方法用函數(shù)式語言來描述算法函數(shù)空間：INT*INTBOOL函數(shù)定義（方程）

lookupLa=(nullL→FALSE，

a=hdL→TRUE，lookup(tlL)a)2023/8/617關(guān)于函數(shù)式描述方法用函數(shù)式語言來描述算法2023/9/1818操作語義學(xué)2023/8/618操作語義學(xué)2023/9/18192023/8/6192023/9/1820操作語義學(xué)三種方法解釋器方法抽象機(jī)歸約方法（歸約系統(tǒng)）從實(shí)現(xiàn)的角度，通過程序的執(zhí)行過程來定義程序設(shè)計(jì)語言的語義；2023/8/620操作語義學(xué)三種方法2023/9/1821操作語義學(xué)

抽象機(jī)方法2023/8/621操作語義學(xué)

抽象機(jī)方法2023/9/1822主要思想：針對計(jì)算機(jī)語言，定義一個抽象機(jī)來解釋執(zhí)行將該語言的程序；抽象機(jī)的定義包括兩個部分：抽象機(jī)組成的抽象定義–狀態(tài)結(jié)構(gòu)執(zhí)行機(jī)制的形式定義--狀態(tài)轉(zhuǎn)換規(guī)則針對如下語言結(jié)構(gòu)給出抽象機(jī)定義表達(dá)式語句輸入輸出聲明Block過程/函數(shù)2023/8/622主要思想：2023/9/1823狀態(tài)結(jié)構(gòu)（形式定義）棧（保存中間計(jì)算結(jié)果）語句控制區(qū)表達(dá)式控制區(qū)靜態(tài)環(huán)境區(qū)動態(tài)環(huán)境去堆區(qū)（保存中斷現(xiàn)場）初始狀態(tài)和終止?fàn)顟B(tài)狀態(tài)轉(zhuǎn)換規(guī)則針對每個語法結(jié)構(gòu)給出執(zhí)行過程狀態(tài)到狀態(tài)的映射基于抽象機(jī)的操作語義的定義過程2023/8/623狀態(tài)結(jié)構(gòu)（形式定義）基于抽象機(jī)的操作語義2023/9/1824操作語義學(xué)

歸約方法2023/8/624操作語義學(xué)

歸約方法2023/9/1825歸約方法的主要思想：一種結(jié)構(gòu)化方法（只依賴于成分的結(jié)果）根據(jù)語言的成分給出歸約系統(tǒng)的方法歸約系統(tǒng)是由以下部分組成的：一組歸約公理一組推理規(guī)則，稱為歸約規(guī)則歸約的對象為格局（configuration），歸約的結(jié)果也是格局；初始格局和終止格局；2023/8/625歸約方法的主要思想：2023/9/1826基于歸約方法的操作語義的定義過程格局的形式：<comp1,…,compn>，通過模式給出初始格局和終止格局一組歸約公理：

configure1

configure2

一組歸約規(guī)則形：

A1,……,An

條件公理

configure1

configure2推導(dǎo)出的公理 其中A1,……,An是關(guān)于configure1中成分的公理，而configure2中的成分只能從configure1和A1,……,An中的結(jié)果格局中得到；2023/8/626基于歸約方法的操作語義的定義過程格局的形2023/9/18272023/8/6272023/9/18282023/8/6282023/9/18292023/8/6292023/9/18302023/8/6302023/9/18312023/8/6312023/9/1832指稱語義學(xué)2023/8/632指稱語義學(xué)2023/9/18332023/8/6332023/9/1834指稱語義學(xué)直接指稱語義兩個方面定義指稱語義（五個部分）完整語言某個語法單位給出具體語法元素的指稱語義解釋（語義函數(shù)）根據(jù)該語法元素所屬的語法域的具體的語義指派函數(shù)；確定已知條件（靜態(tài)環(huán)境，動態(tài)環(huán)境）給出語義解釋（函數(shù)；值……）2023/8/634指稱語義學(xué)直接指稱語義2023/9/1835直接指稱語義主要原理：從功能角度出發(fā)，對每一個語法單位（如程序、聲明、語句、表達(dá)式、變量、整數(shù)、標(biāo)識符等），給出其功能的嚴(yán)格形式化描述，即定義功能函數(shù)；功能函數(shù)是描述一個語法單位的語義，因此稱為語義函數(shù)（語義物）；本質(zhì)上是建立語法域到語義函數(shù)域的映射；語法域語義函數(shù)域語義指派函數(shù)2023/8/635直接指稱語義主要原理：語法域語義函數(shù)域語2023/9/1836直接指稱語義直接指稱語義的定義包括：語法域（SyntaxDomain）抽象語法（AbstractSyntax）語義域（SemanticDomain）語義函數(shù)（SemanticFunctions）預(yù)定義函數(shù)（PredefinedFunctions）關(guān)鍵：掌握好每個語法單位的功能；語言不一樣，相同的語法單位其語義也不盡相同；2023/8/636直接指稱語義直接指稱語義的定義包括：關(guān)鍵2023/9/1837過程式語言的直接指稱語義語法域（根據(jù)語言定義應(yīng)給出具體定義）程序聲明（還可以細(xì)化）語句Block表達(dá)式常量類型2023/8/637過程式語言的直接指稱語義語法域（根據(jù)語言2023/9/1838過程式語言的直接指稱語義語義域（根據(jù)語言定義應(yīng)給出具體定義）環(huán)境域靜態(tài)環(huán)境動態(tài)環(huán)境值域存儲域2023/8/638過程式語言的直接指稱語義語義域（根據(jù)語言2023/9/1839過程式語言的直接指稱語義語義函數(shù)針對每個語法單位語義指派函數(shù)空間針對每個語法單位定義語義指派函數(shù)針對每個語法單位中的每種語法元素，定義相應(yīng)的語義方程2023/8/639過程式語言的直接指稱語義語義函數(shù)2023/9/1840公理語義學(xué)2023/8/640公理語義學(xué)2023/9/1841主要思想公理語義學(xué)是基于謂詞邏輯中的邏輯歸納方法，一個程序的語義是建立在每次程序運(yùn)行時都成立的關(guān)于變量的值之間關(guān)系的斷言；定義過程為計(jì)算機(jī)語言建立一個公理系統(tǒng)公理系統(tǒng)由兩部分組成：（1）一組公理；（2）一組推理規(guī)則局限性2023/8/641主要思想2023/9/18422023/8/6422023/9/18432023/8/6432023/9/18442023/8/6442023/9/18452023/8/6452023/9/18462023/8/6462023/9/1847Hoare公理系統(tǒng)2023/8/647Hoare公理系統(tǒng)2023/9/1848公理和命題的形式：{P}S{Q}推理規(guī)則的形式

Hoare公理系統(tǒng)由五條規(guī)則賦值公理復(fù)合推理規(guī)則條件推理規(guī)則循環(huán)推理規(guī)則推論規(guī)則F1，……,FnF2023/8/648公理和命題的形式：{P}S{2023/9/1849最弱前置條件和最強(qiáng)后置條件2023/8/649最弱前置條件和最強(qiáng)后置條件2023/9/1850最弱前置條件的計(jì)算規(guī)則求WP(S,q)WP(skip,q)=q;WP(x:=e,q)=q[e/x];WP(s1;s2,q)=WP(s1,WP(s2,q));WP(if(e,s1,s2),q)=(eWP(s1,q))

(

eWP(s