形式語(yǔ)義-操作語(yǔ)義

1、程序設(shè)計(jì)語(yǔ)言的形式語(yǔ)義,The Formal Semantics of Programming Languages,操作語(yǔ)義,操作語(yǔ)義（operational semantics）通過(guò)描述程序語(yǔ)法構(gòu)造在機(jī)器上的運(yùn)行效果而定義程序的語(yǔ)義。 以抽象機(jī)器為語(yǔ)義解釋對(duì)象 操作語(yǔ)義關(guān)注程序的運(yùn)行效果是怎樣得到的 HOW,操作語(yǔ)義,操作語(yǔ)義概述(1) 1960s，對(duì)編譯程序所產(chǎn)生的目標(biāo)程序標(biāo)準(zhǔn)化、形式化的愿望；自動(dòng)機(jī)理論研究的興旺時(shí)期 抽象機(jī)。抽象機(jī)是操作語(yǔ)義的核心，既是具體機(jī)器的抽象化，又是自動(dòng)機(jī)的高級(jí)化向著直接反映高級(jí)語(yǔ)言語(yǔ)義的方向靠近。 MaCarthy，比較明確的提出用抽象機(jī)表達(dá)操作語(yǔ)義，并用它描

2、述了ALGOL60的一個(gè)子集的語(yǔ)義。 1964年Landin，SECD（Stack,Environment,Control, Dump）;擴(kuò)充為SM（共享機(jī)），描述了ALGOL60完整語(yǔ)義。 1968年，Knuth提出屬性文法。,操作語(yǔ)義,操作語(yǔ)義概述(2) 傳統(tǒng)的操作語(yǔ)義的頂峰是VDL（維也納定義語(yǔ)言），IBM的維也納實(shí)驗(yàn)室，形式化定義PL/1語(yǔ)言 與此同時(shí)，英國(guó)赫斯利實(shí)驗(yàn)室對(duì)PL/1語(yǔ)言 的形式化被ANSI接受為標(biāo)準(zhǔn)（形式化程度較低，規(guī)范的自然語(yǔ)言描述） 操作語(yǔ)義的另一個(gè)變種是變換語(yǔ)義。用分而治之的思想降低復(fù)雜度（抽象復(fù)雜度+翻譯復(fù)雜度）。德國(guó)CIP小組提出的廣譜語(yǔ)言。M5，M4，M3，M

3、2，M1 1981，Plotkin提出結(jié)構(gòu)化的操作語(yǔ)義。把公理化方法引入操作語(yǔ)義中，基本思想是：復(fù)合成分的操作語(yǔ)義可以歸結(jié)為其各個(gè)組成部分的操作語(yǔ)義。,IMP一種簡(jiǎn)單的命令式語(yǔ)言,IMP語(yǔ)言的語(yǔ)法范疇： N，數(shù)集，包括正整數(shù)、負(fù)整數(shù)和零 帶符號(hào)位的正負(fù)十進(jìn)制數(shù)的集合 T，真值集，T=true, false Loc，存儲(chǔ)單元集 字母開(kāi)頭的字母數(shù)字串 Aexp，算術(shù)表達(dá)式集 Bexp，邏輯表達(dá)式集 Com，命令集,IMP一種簡(jiǎn)單的命令式語(yǔ)言,語(yǔ)法成分的元變量（約定）： n，m表示數(shù)集N中的元素 x，y 表示存儲(chǔ)單元集Loc中的元素 a 表示算術(shù)表達(dá)式集Aexp中的元素 b 表示邏輯表達(dá)式集Bexp

4、中的元素 c 表示命令集Com中的元素 可以加上標(biāo)或下標(biāo),IMP一種簡(jiǎn)單的命令式語(yǔ)言,算術(shù)表達(dá)式的抽象語(yǔ)法,IMP一種簡(jiǎn)單的命令式語(yǔ)言,邏輯表達(dá)式的抽象語(yǔ)法,IMP一種簡(jiǎn)單的命令式語(yǔ)言,命令的抽象語(yǔ)法,四種語(yǔ)句 空語(yǔ)句 賦值語(yǔ)句 分支語(yǔ)句 循環(huán)語(yǔ)句 程序命令、程序語(yǔ)句、程序,IMP一種簡(jiǎn)單的命令式語(yǔ)言,定義2.1： IMP語(yǔ)言的算術(shù)表達(dá)式、邏輯表達(dá)式及命令的抽象語(yǔ)法,IMP一種簡(jiǎn)單的命令式語(yǔ)言,IMP語(yǔ)言語(yǔ)法擴(kuò)展：,為了講課方便擴(kuò)充了一些運(yùn)算，非本質(zhì)的。,IMP一種簡(jiǎn)單的命令式語(yǔ)言,例2.1 交換程序及其語(yǔ)法樹(shù)：,IMP一種簡(jiǎn)單的命令式語(yǔ)言,例2.2 階乘程序：,變遷系統(tǒng),操作語(yǔ)義通過(guò)描述程序

5、在抽象機(jī)器上的運(yùn)行過(guò)程來(lái)描述程序的語(yǔ)義。 運(yùn)行過(guò)程用程序狀態(tài)和當(dāng)前要執(zhí)行的命令的變換序列給出。,格局（configuration）,程序的運(yùn)行過(guò)程就是格局的變換序列,變遷系統(tǒng),狀態(tài)： 直觀模型：存儲(chǔ)單元的內(nèi)容決定了當(dāng)前的狀態(tài) 狀態(tài)集合， ：LocN (x)是狀態(tài)下存儲(chǔ)單元x 的值或內(nèi)容,程序中所出現(xiàn)的變量,變遷系統(tǒng),格局： 程序狀態(tài)是一個(gè)特殊的格局 變遷系統(tǒng)（Transition System）（轉(zhuǎn)換系統(tǒng)） 變遷系統(tǒng)是二元組（X, R）,在狀態(tài)下將要執(zhí)行c,語(yǔ)句為空，省略尖括號(hào),變遷系統(tǒng)的狀態(tài)集， 其元素稱為狀態(tài)或格局,RXX 狀態(tài)之間的變遷關(guān)系,變遷系統(tǒng),可以將IMP程序理解為運(yùn)行在一個(gè)變遷

6、系統(tǒng)上 運(yùn)行過(guò)程是程序狀態(tài)和下一步要執(zhí)行的程序語(yǔ)句的變化 變遷關(guān)系(c1,1) (c2, 2)：程序（命令）c1在狀態(tài)1運(yùn)行后得到狀態(tài)2且下一步要執(zhí)行的程序是c2 。 (c1,1) 2：程序（命令）c1在狀態(tài)1運(yùn)行后得到狀態(tài)2且沒(méi)有后續(xù)語(yǔ)句要執(zhí)行（程序結(jié)束） 。,變遷系統(tǒng),小結(jié)：描述IMP語(yǔ)言的操作語(yǔ)義： 格局 程序（命令）c在狀態(tài)下運(yùn)行 程序終止的狀態(tài) 變遷關(guān)系 定義IMP語(yǔ)言的操作語(yǔ)義就是定義適當(dāng)格局之間的變遷關(guān)系 通過(guò)定義IMP語(yǔ)言的每個(gè)命令所引起的變遷來(lái)完成,表達(dá)式的語(yǔ)義,表達(dá)式是IMP語(yǔ)言的最基本的語(yǔ)法成分，包括算術(shù)表達(dá)式和邏輯表達(dá)式 程序執(zhí)行是對(duì)程序狀態(tài)的變換；而表達(dá)式的計(jì)算并不改

7、變程序狀態(tài)，可以看作是對(duì)程序狀態(tài)的某種觀察。 狀態(tài) ：LocN 定義一個(gè)新?tīng)顟B(tài),程序變量x在該狀態(tài)下的值就是v，而其他變量的值不變（未知或不關(guān)心）,表達(dá)式的語(yǔ)義,算術(shù)表達(dá)式的求值,序偶表示狀態(tài)下表達(dá)式a等待求值 求值關(guān)系：,狀態(tài)下表達(dá)式a的求值結(jié)果為n,表達(dá)式的語(yǔ)義,算術(shù)表達(dá)式的求值,求值規(guī)則,積,表達(dá)式的語(yǔ)義,邏輯表達(dá)式的求值,求值規(guī)則（1）,表達(dá)式的語(yǔ)義,邏輯表達(dá)式的求值,求值規(guī)則（2）,表達(dá)式的語(yǔ)義,表達(dá)式的語(yǔ)義,邏輯表達(dá)式的求值,最左順序計(jì)算（短路）,表達(dá)式的語(yǔ)義,說(shuō)明：,規(guī)則一般包括前提和結(jié)論，后面的條件稱為附加條件。 有些規(guī)則沒(méi)有前提部分，前提為空的規(guī)則稱為公理。（有時(shí)在上面加一條

8、實(shí)線） 由前提推出結(jié)論稱為規(guī)則的一個(gè)應(yīng)用。 用特定的數(shù)、存儲(chǔ)單元、表達(dá)式以及狀態(tài)來(lái)替代規(guī)則的元變量，就得到一個(gè)規(guī)則實(shí)例。 求值過(guò)程推導(dǎo)樹(shù)。,表達(dá)式的語(yǔ)義,狀態(tài)0下表達(dá)式(Init+5)+(7+9)的求值， 0(Init)=0,推導(dǎo)樹(shù)由規(guī)則的實(shí)例構(gòu)成，每個(gè)實(shí)例的前提正好是上一層實(shí)例的結(jié)論； 公理位于最頂層，公理的上方?jīng)]有前提部分； 最底層的實(shí)例的結(jié)論稱為整個(gè)推導(dǎo)的結(jié)論。 如果某個(gè)推導(dǎo)存在結(jié)論，稱該結(jié)論是從規(guī)則可精確推導(dǎo)的。 匹配的規(guī)則可能有多條，必須考慮所有左部與格局匹配的規(guī)則；對(duì)于符合條件的所有推導(dǎo)必須并行地構(gòu)造。,表達(dá)式的語(yǔ)義,狀態(tài)下布爾表達(dá)式(x*y)z) +(z+x=0)的求值， (x)

9、=3， (y)=5， (z)=7,表達(dá)式的語(yǔ)義,算術(shù)表達(dá)式的等價(jià) 邏輯表達(dá)式的等價(jià),命令的語(yǔ)義（自然語(yǔ)義）,操作語(yǔ)義定義適當(dāng)格局之間的變遷關(guān)系 程序（命令）通過(guò)執(zhí)行來(lái)改變狀態(tài),表示在狀態(tài)下執(zhí)行完命令c終止于終態(tài)。 例如：,命令的語(yǔ)義（自然語(yǔ)義）,命令的規(guī)則（1）,原子命令,實(shí)例： 初始狀態(tài)下所有存儲(chǔ)單元的值均為0,命令的語(yǔ)義（自然語(yǔ)義）,命令的規(guī)則（2）,順序命令,實(shí)例：,命令的語(yǔ)義（自然語(yǔ)義）,命令的規(guī)則（3）,條件命令,命令的語(yǔ)義（自然語(yǔ)義）,命令的規(guī)則（3）,條件命令實(shí)例：,命令的語(yǔ)義（自然語(yǔ)義）,命令的規(guī)則（4）,循環(huán)命令,命令的語(yǔ)義（自然語(yǔ)義）,命令的規(guī)則（4）,循環(huán)命令實(shí)例,循環(huán)體

10、每執(zhí)行一步的變遷關(guān)系,命令的語(yǔ)義（自然語(yǔ)義）,死循環(huán),這種推導(dǎo)是無(wú)窮的，因此，實(shí)際上不存在狀態(tài)使得：,語(yǔ)義無(wú)定義,命令的語(yǔ)義（自然語(yǔ)義）,命令的規(guī)則小結(jié),命令的語(yǔ)義（自然語(yǔ)義）,推導(dǎo)樹(shù) 例1：交換程序,命令的語(yǔ)義（自然語(yǔ)義）,例2：階乘程序 0(x)=3， 0(y)=0,命令的語(yǔ)義（自然語(yǔ)義）,小結(jié)：自然語(yǔ)義 可以看作如下形式的函數(shù)： 對(duì)任意的命令c，自然語(yǔ)義函數(shù)是從狀態(tài)集到的部分函數(shù) 有定義 無(wú)定義 至多存在一個(gè)終止?fàn)顟B(tài),等價(jià)關(guān)系及證明,命令的等價(jià)（語(yǔ)義等價(jià)）,例：,等價(jià)關(guān)系及證明,命題2.8（P16）,證明：,對(duì)所有的狀態(tài)，有：,兩方面： “” “”,等價(jià)關(guān)系及證明,（1）“”,等價(jià)關(guān)系及

11、證明,等價(jià)關(guān)系及證明,等價(jià)關(guān)系及證明,（2）“”,等價(jià)關(guān)系及證明,由于：,所以：,等價(jià)關(guān)系及證明,自然語(yǔ)義小結(jié),自然語(yǔ)義 至多存在一個(gè)終止?fàn)顟B(tài) 語(yǔ)義等價(jià)關(guān)系,自然語(yǔ)義小結(jié),自然語(yǔ)義小結(jié),練習(xí)：整除程序的推導(dǎo)樹(shù)：,自然語(yǔ)義小結(jié),練習(xí)：整除程序的推導(dǎo)樹(shù)：,信息工程學(xué)院計(jì)算機(jī)系,另一種語(yǔ)義（結(jié)構(gòu)化操作語(yǔ)義）,與自然語(yǔ)義比較 自然語(yǔ)義所給出的變遷關(guān)系是一步到位的,另一種語(yǔ)義（結(jié)構(gòu)化操作語(yǔ)義） 描述程序執(zhí)行中每一小步的中間狀態(tài),另一種語(yǔ)義（結(jié)構(gòu)化操作語(yǔ)義）,原子命令的結(jié)構(gòu)化操作語(yǔ)義,另一種語(yǔ)義（結(jié)構(gòu)化操作語(yǔ)義）,順序命令的結(jié)構(gòu)化操作語(yǔ)義,另一種語(yǔ)義（結(jié)構(gòu)化操作語(yǔ)義）,條件命令的結(jié)構(gòu)化操作語(yǔ)義,另一種語(yǔ)義（結(jié)構(gòu)化操作語(yǔ)義）,循環(huán)命令的結(jié)構(gòu)化操作語(yǔ)義,另一種語(yǔ)義（結(jié)構(gòu)化操作語(yǔ)義）,規(guī)則：,另一種語(yǔ)義（結(jié)構(gòu)化操作語(yǔ)義）,例1：交換程序,推導(dǎo)序列,另一種語(yǔ)義（結(jié)構(gòu)化操作語(yǔ)義）,推導(dǎo)序列,另一種語(yǔ)義（結(jié)構(gòu)化操作語(yǔ)義）,另一種語(yǔ)義（結(jié)構(gòu)化操作語(yǔ)義）,例2：階乘程序,另一種語(yǔ)義（結(jié)構(gòu)化操作語(yǔ)義）,例2：階乘程序,另一種語(yǔ)義（結(jié)構(gòu)化操作語(yǔ)義）,例2：階乘程序,另一種語(yǔ)義（結(jié)構(gòu)化操作語(yǔ)義）,例2：階乘程序,另一種語(yǔ)義（結(jié)構(gòu)化操作語(yǔ)義）,例2：階乘程序,另一種語(yǔ)