第四章程序語言的性質(zhì)1第四章程序語言的性質(zhì)1語言的形式化模型BNF為描述程序設(shè)計語言的屬性提供了一種很好的手段，但并不是充分的手段。BNF回答了程序看起來象什么，但沒有回答程序是做什么的。形式化模型采用精確的數(shù)學(xué)模型來刻畫研究對象，為研究、分析和操縱研究對象提供嚴(yán)謹(jǐn)?shù)臄?shù)學(xué)工具和手段。本章將介紹下列形式化模型：形式文法：喬姆斯基文法分級語言的語義：屬性文法、指稱語義程序的驗(yàn)證2語言的形式化模型BNF為描述程序設(shè)計語言的屬性提供了一種很好4.1語言的形式化性質(zhì)喬姆斯基分級文法語言的能力34.1語言的形式化性質(zhì)喬姆斯基分級文法3喬姆斯基分級文法文法由非終結(jié)符、終結(jié)符、開始（非終結(jié)）符、及產(chǎn)生式構(gòu)成文法的類別3型文法：正則文法，定義詞法的模型2型文法：BNF文法，上下文無關(guān)文法1型文法：上下文有關(guān)文法0型文法：4喬姆斯基分級文法文法43型文法：正則文法為詞法分析器提供模型。這類文法的大多數(shù)性質(zhì)都是可判定的如，能產(chǎn)生什么樣的串、給定串是否屬于文法規(guī)定的語言、語言中的串是否有限等正則文法可以產(chǎn)生形如an的串，其中a為有限字符序列正則文法只能計數(shù)有限數(shù)常用于關(guān)鍵字或單詞掃描53型文法：正則文法為詞法分析器提供模型。52型文法—上下文無關(guān)文法產(chǎn)生式的形式為：X,其中可以是終結(jié)符和非終結(jié)符的任意序列同樣，這類文法的大多數(shù)性質(zhì)都是可判定的如，能產(chǎn)生什么樣的串、給定串是否屬于文法規(guī)定的語言、語言是否為空等可用來計數(shù)和比較兩個項(xiàng)，產(chǎn)生形如ancbn的串可以用堆棧來實(shí)現(xiàn)可用來自動產(chǎn)生程序的語法分析樹2型和3型文法的相關(guān)問題都已基本上得到解決62型文法—上下文無關(guān)文法產(chǎn)生式的形式為：X,其中1型文法—上下文有關(guān)文法產(chǎn)生式的形式為：,其中任意非終結(jié)符串，是終結(jié)符和非終結(jié)符的任意序列，但中的符號個數(shù)應(yīng)不多于的符號個數(shù)從開始符開始導(dǎo)出的串的長度是遞增的在生成串時，需要使用固定數(shù)量的存儲空間，例如識別上下文無關(guān)文法無法識別的串a(chǎn)ncnbn上下文有關(guān)文法太復(fù)雜，很難用于程序設(shè)計語言人們對上下文有關(guān)文法的很多特征還不太清楚71型文法—上下文有關(guān)文法產(chǎn)生式的形式為：,其中0型文法—非限定型文法對產(chǎn)生式的形式?jīng)]有任何限制可用來識別任意可計算的函數(shù)其大多數(shù)性質(zhì)都是不可判定的返回80型文法—非限定型文法對產(chǎn)生式的形式?jīng)]有任何限制返不可判定性不同類型的文法越來越復(fù)雜，產(chǎn)生的語言也越來越復(fù)雜，但是否說明計算機(jī)解決問題的能力可以越來越強(qiáng)，沒有限制？例如：能否編寫一個C語言程序來判斷另一個C語言程序能否結(jié)束？但這基本上是不可能的，這不是編程人員的問題，而是因?yàn)橛嬎銠C(jī)所基于的數(shù)學(xué)模型本身的局限性而導(dǎo)致的。9不可判定性不同類型的文法越來越復(fù)雜，產(chǎn)生的語言也越來越復(fù)雜，圖靈機(jī)一般來說，用一種語言編寫的程序也可以用其他另一種語言來實(shí)現(xiàn)。那么是否存在某個程序，只能用某種語言來實(shí)現(xiàn)，而用其他語言就無法實(shí)現(xiàn)？如果沒有，那么有哪些程序是其它程序設(shè)計語言無法表示的，為什么還需要那么多種不同的語言？如果我們將能夠表示所有計算的語言都稱為通用語言，那么是不是所有語言都是通用語言？如果是，是否存在更簡單的通用語言？10圖靈機(jī)一般來說，用一種語言編寫的程序也可以用其他另一種語言來圖靈機(jī)的結(jié)構(gòu)圖靈機(jī)是一種用來定義可計算函數(shù)的抽象計算機(jī)圖靈機(jī)只有一個單一的數(shù)據(jù)結(jié)構(gòu)，即一個稱為“帶子”的可變長線性數(shù)組帶子被分為很多格，每格上只包含一個字符圖靈機(jī)還有一個指針變量，稱為“讀出頭”，它總是指向帶子上的某個格。11圖靈機(jī)的結(jié)構(gòu)圖靈機(jī)是一種用來定義可計算函數(shù)的抽象計算機(jī)11圖靈機(jī)的操作圖靈機(jī)只提供幾個簡單的操作：讀出頭所指定位置的字符可以被讀出或被修改。程序可以根據(jù)讀出的值進(jìn)行轉(zhuǎn)移。讀出頭可以左右移動。如果讀出頭移動到帶子的最末端，則自動在帶子上加上一格，并賦予一個空字符作為初始值。12圖靈機(jī)的操作圖靈機(jī)只提供幾個簡單的操作：12圖靈機(jī)的運(yùn)行圖靈機(jī)開始運(yùn)行時，帶子上存放輸入數(shù)據(jù)，讀出頭指向輸入數(shù)據(jù)的最左端的字符；圖靈機(jī)根據(jù)預(yù)先編好的操作序列讀寫帶子上的數(shù)據(jù)、或移動讀出頭；如果最終能夠停機(jī)，則帶子上的內(nèi)容就是最后的輸出結(jié)果。13圖靈機(jī)的運(yùn)行圖靈機(jī)開始運(yùn)行時，帶子上存放輸入數(shù)據(jù)，讀出頭指向圖靈機(jī)的能力任意可計算函數(shù)都可以用圖靈機(jī)計算出來（Church論題）圖靈機(jī)等價于0型文法確定型圖靈機(jī)等價于非確定型圖靈機(jī)。14圖靈機(jī)的能力任意可計算函數(shù)都可以用圖靈機(jī)計算出來（Churc停機(jī)問題是否存在某個通用的算法，它能夠斷定任意給定的圖靈機(jī)在任意的輸入下能否停機(jī)？停機(jī)問題是不可判斷的，即不存在這樣的通用算法。任意一個不可判斷的問題，都等價于停機(jī)問題。結(jié)論：任何一種程序設(shè)計語言都可能代替其它語言程序設(shè)計語言不存在質(zhì)的區(qū)別，只有量的區(qū)別，如是否優(yōu)美、易用、高效等任何一種程序設(shè)計語言都有它存在的理由返回15停機(jī)問題是否存在某個通用的算法，它能夠斷定任意給定的圖靈機(jī)在4.2語言的語義程序設(shè)計語言基本上都是以上下文無關(guān)文法(特別是LR(k)文法)的核心設(shè)計的。但語法分析已經(jīng)不再是人們感興趣的研究問題了。現(xiàn)在的問題是如何確定程序的含義（即語義）。164.2語言的語義程序設(shè)計語言基本上都是以上下文無關(guān)文法(特語言的語義語言的手冊必須定義語言中每個結(jié)構(gòu)的含義，包括單獨(dú)結(jié)構(gòu)的含義以及和其他結(jié)構(gòu)組合時的含義。語言提供了不同結(jié)構(gòu)，用戶（為了寫正確的程序，預(yù)測語句的執(zhí)行效果）和實(shí)現(xiàn)者（正確地實(shí)現(xiàn)語言）需要這些結(jié)構(gòu)的精確定義。大多數(shù)語言中，形式文法用于定義語法，一段文字或例子用于定義語義，但定義是不精確的，有二義性，不同作者可能有不同理解。語義定義問題還是理論研究的目標(biāo)，但至今沒有令人滿意的解答。已有各種形式方法用于語義定義。17語言的語義語言的手冊必須定義語言中每個結(jié)構(gòu)的含義，包括單獨(dú)結(jié)語義建模（1）—文法模型對定義語言的BNF文法進(jìn)行擴(kuò)展，給出程序的語法分析樹，從樹中抽取出附加信息。屬性文法便是抽取附加信息的一種方式。18語義建模（1）—文法模型對定義語言的BNF文法進(jìn)行擴(kuò)展，給出語義建模（2）—命令或操作模型定義程序如何在某虛擬機(jī)上執(zhí)行。通常描述為一自動機(jī)，但比語法用的簡單自動機(jī)遠(yuǎn)為復(fù)雜。自動機(jī)有內(nèi)部狀態(tài)——對應(yīng)程序執(zhí)行時的內(nèi)部狀態(tài)，包括所有變量的值、執(zhí)行程序本身、以及各種系統(tǒng)定義的數(shù)據(jù)結(jié)構(gòu)。19語義建模（2）—命令或操作模型定義程序如何在某虛擬機(jī)上執(zhí)行。語義建模（2）—命令或操作模型一組形式定義的操作用于刻劃自動機(jī)內(nèi)部狀態(tài)如何改變。此外還需定義程序文本如何翻譯成自動機(jī)的初始狀態(tài)。語言的操作定義對語言如何實(shí)際執(zhí)行給出了相當(dāng)直接的抽象。也可能提出一個更抽象的模型，作為語言的軟件解釋的基礎(chǔ)。70年代的VDL（ViennaDefinitionLanguage）是一個操作方法。它擴(kuò)展語法分析樹已包含機(jī)器解釋器。計算的狀態(tài)是程序樹加上描述機(jī)器中所有數(shù)據(jù)的樹。每條語句的執(zhí)行使樹的狀態(tài)發(fā)生變化。20語義建模（2）—命令或操作模型一組形式定義的操作用于刻劃自動語義建模（3）—作用型模型試圖直接構(gòu)造每個程序的函數(shù)的定義，采用層次式的構(gòu)造方式。程序中每個基本的或程序員定義的操作代表一個數(shù)學(xué)函數(shù)。語言的程序控制結(jié)構(gòu)用于將這些函數(shù)復(fù)合為更大的序列，代表表達(dá)式和語言。語句序列和條件分叉表示為個體函數(shù)構(gòu)造而成的函數(shù)。循環(huán)通常表示為遞歸函數(shù)。最終，為整個程序?qū)С鲆粋€完整的函數(shù)模型，指稱語義歸于此類。21語義建模（3）—作用型模型試圖直接構(gòu)造每個程序的函數(shù)的定義，語義建模（4）—公理模型使用謂詞演算，每個語法結(jié)構(gòu)的語義被描述為公理或推導(dǎo)規(guī)則，用于導(dǎo)出結(jié)構(gòu)的執(zhí)行效果。從一個初始假設(shè)開始，假設(shè)輸入變量滿足一定的約束，在程序語句執(zhí)行后，使用公理和推導(dǎo)規(guī)則來推導(dǎo)其他變量值需滿足的限制，最終，程序的結(jié)果被證明滿足希望的約束（描述了它們的值和輸入值的關(guān)系）。如Hoare的公理語義。22語義建模（4）—公理模型使用謂詞演算，每個語法結(jié)構(gòu)的語義被描語義建模（5）—規(guī)約模型描述實(shí)現(xiàn)程序的各個函數(shù)的關(guān)系，只要我們可以證明一個實(shí)現(xiàn)符合了所有的函數(shù)間的關(guān)系，則稱實(shí)現(xiàn)相對于規(guī)約是正確的。代數(shù)數(shù)據(jù)類型是形式規(guī)約的一種形式。例如：實(shí)現(xiàn)棧的程序，S表示棧，則有公理，pop(push(S,x))=S任何一個實(shí)現(xiàn)如果能保持這種關(guān)系，則稱是棧的正確實(shí)現(xiàn)。23語義建模（5）—規(guī)約模型描述實(shí)現(xiàn)程序的各個函數(shù)的關(guān)系，只要我語義模型—小結(jié)上述各種形式語義模型各有優(yōu)點(diǎn)，但均不能稱為完全實(shí)用的和適用的，各有其適合范圍。操作語義為語言的實(shí)現(xiàn)提供了一種形式模型，但對用戶來說太細(xì)節(jié)公理語義易于理解，但很難用來定義復(fù)雜的程序設(shè)計語言，且缺乏對語言實(shí)現(xiàn)的支持返回24語義模型—小結(jié)上述各種形式語義模型各有優(yōu)點(diǎn)，但均不能稱為完全語義建模—屬性文法這是最早的開發(fā)語義模型的工作之一。其思想是對分析樹中的每個結(jié)點(diǎn)關(guān)聯(lián)一個函數(shù)，從而給出結(jié)點(diǎn)的語義內(nèi)容。屬性文法的創(chuàng)建過程是為文法中的每一條規(guī)則都定義相關(guān)的語義函數(shù)。繼承屬性是一個函數(shù)，它將樹中非終結(jié)符值和樹中更高層的非終結(jié)符值相關(guān)聯(lián)。換言之，任何規(guī)則右端的非終結(jié)符的函數(shù)值是左端非終結(jié)符的函數(shù)。綜合屬性是一個函數(shù)，它將左端非終結(jié)符和右端非終結(jié)符的值相關(guān)聯(lián)，這些屬性在樹中向上傳遞信息，即從樹中下層信息進(jìn)行“綜合”。25語義建模—屬性文法這是最早的開發(fā)語義模型的工作之一。25屬性文法例：考慮算術(shù)表達(dá)式的簡單文法。

E→T|E+T T→P|T×P P→I|(E)其語義通過文法中非終結(jié)符間的關(guān)系集合定義。如：下面函數(shù)生成該文法生成的任意表達(dá)式的值： 產(chǎn)生式 屬性

E→E+T Value(E1)=V(E2)+V(T) E→T V(E)=V(T) T→T×P V(T1)=V(T2)×V(P) T→P V(T)=V(P) P→I V(P)=數(shù)I的值

P→(E) V（P）=V（E）26屬性文法例：考慮算術(shù)表達(dá)式的簡單文法。26屬性文法下圖是一個屬性樹，它給出了表達(dá)式2+4×(1+2)值27屬性文法下圖是一個屬性樹，它給出了表達(dá)式2+4×(1+2)值屬性文法屬性文法可用于在語法樹中傳遞語義信息。例如，聲明信息可以通過語言的聲明產(chǎn)生式收集。沿樹向下傳的符號表信息可用于生成表達(dá)式代碼。下面屬性可加到非終結(jié)符<decl>和<declaration>來創(chuàng)建一個程序中聲明的名字集合。 產(chǎn)生式 屬性<declaration>::=<decl><declaration> decl_set(declaration1)=declaname(decl) ∪decl_set(declaration2)<declaration>::=<decl> decl_set(declaration)=decl-name(decl)<decl>::=declarex decl-name(decl)=x(decl)::=declarey decl-name(decl)=y(decl)::=declarez decl-name(decl)=z這是綜合屬性，包含程序中聲明的名字集合。該屬性可以沿樹向下傳遞，成為繼承屬性，用于正確地生成數(shù)據(jù)的代碼。28屬性文法屬性文法可用于在語法樹中傳遞語義信息。例如，聲明信息屬性文法的使用首先創(chuàng)建語法分析樹。屬性文法假設(shè)你已經(jīng)知道表達(dá)式是如何推導(dǎo)出來的，它并不關(guān)心是如何分析推導(dǎo)出來的。定義屬性的函數(shù)可以是任意給定的，因此定義屬性的過程完全是手工完成的。如果只有綜合屬性，并且文法是LR(k)，那么，屬性文法可以用來在語法分析時自動產(chǎn)程中間代碼。這就是YACC如何工作的，它利用屬性文法來計算所有非終結(jié)符的值。在構(gòu)造分析樹時，非終結(jié)符的信息逐層向上傳遞給分析樹上層的非終結(jié)符。語法分析完畢，所有屬性的值將計算出來。返回29屬性文法的使用首先創(chuàng)建語法分析樹。屬性文法假設(shè)你已經(jīng)知道表達(dá)指稱語義指稱語義是一種用來描述程序設(shè)計語言的語義的作用型語義模型指稱語義基于-演算30指稱語義指稱語義是一種用來描述程序設(shè)計語言的語義的作用型語義-演算-演算是一種和圖靈機(jī)的計算能力相當(dāng)?shù)睦碚撚嬎隳Ｐ?演算可以作為程序設(shè)計語言的函數(shù)調(diào)用的模型Algol和Lisp都采用來-演算的函數(shù)調(diào)用語義指稱語義是對-演算的擴(kuò)充，它將-演算擴(kuò)充為一種通用的數(shù)據(jù)類型理論31-演算-演算是一種和圖靈機(jī)的計算能力相當(dāng)?shù)睦碚撚嬎隳Ｐ?-演算的表達(dá)式-表達(dá)式可以遞歸地定義如下：變量名為-表達(dá)式如果M為一個-表達(dá)式，則x.M也是一個-表達(dá)式如果F和A都是-表達(dá)式，則(FA)也是-表達(dá)式，其中F為操作符，A為操作數(shù)。形式語法： -expr::=id|id.-expr|(-expr-expr)x相當(dāng)于申明參數(shù)變量x，沒有申明的變量為自由變量，否則為約束變量。x.M相當(dāng)于函數(shù)申明，其中x相當(dāng)于M的參數(shù)。例如： xx.xx.(xy)x.y(x.xy.y)32-演算的表達(dá)式-表達(dá)式可以遞歸地定義如下：32-表達(dá)式的操作-表達(dá)式只有一種操作：約簡(FA)約簡相當(dāng)于將A作為實(shí)際參數(shù)，替換F的形式參數(shù)的所有出現(xiàn)(x.MA)M’，相當(dāng)于用A替換M中x的所有自由出現(xiàn)。例如：(x.xy)y(x.(xy)x.x)

x.xyy注意：約簡并不一定能簡化原來的表達(dá)式(x.(xx)x.(xx))(x.(xx)x.(xx))……33-表達(dá)式的操作-表達(dá)式只有一種操作：約簡33指稱語義指稱語義的基本思想是定義一個語義函數(shù)（指稱函數(shù)），把程序的意義映射到某種意義清晰的數(shù)學(xué)對象（就像用中文解釋英文）作為被指的數(shù)學(xué)對象可以根據(jù)需要選擇對于簡單的程序語言，一種很自然的選擇是把程序的語義定義為（指稱為）從狀態(tài)到狀態(tài)的函數(shù)。定義語義就是定義好每個程序?qū)?yīng)的函數(shù)。程序的狀態(tài)由標(biāo)識符到值的映射集合構(gòu)成

S={id|value,…}34指稱語義指稱語義的基本思想是定義一個語義函數(shù)（指稱函數(shù)），把指稱語義表達(dá)式的語義[e]Sval語句的語義[s]SS程序的語義[m]valval35指稱語義表達(dá)式的語義35指稱語義設(shè)為程序的當(dāng)前狀態(tài)表達(dá)式的語義常數(shù)：[n]=n變量：[x]=(x)算術(shù)表達(dá)式：[e1+e2]=[e1]+[e2]語句的語義賦值語句：[x=e]=

{x|[e]}復(fù)合語句：[s1;s2]=[s2]([s1])條件語句：[ifbthens1elses2]= if[b]then[s1]else[s2]程序的語義[m]valval返回36指稱語義設(shè)為程序的當(dāng)前狀態(tài)返回36程序驗(yàn)證在編程時，人們越來越關(guān)心程序的正確性和可靠性。人們在設(shè)計程序設(shè)計語言時，也希望通過增加新的特征來增強(qiáng)程序的正確性和可靠性。我們可以用程序語義，按以下方式來探討程序的正確性問題：給定程序P，其含義是什么？即，它的規(guī)范描述S是什么？給定規(guī)范描述S，開發(fā)實(shí)現(xiàn)了該規(guī)范描述的程序P規(guī)范描述S和程序P是否完成了相同的功能（執(zhí)行了相同的函數(shù)）？相當(dāng)于語義建模問題軟件工程的核心問題程序驗(yàn)證的核心問題37程序驗(yàn)證在編程時，人們越來越關(guān)心程序的正確性和可靠性。人們在程序驗(yàn)證測試不能保證程序的正確性如果能找到不依賴于測試的保證程序正確性的方法，產(chǎn)生的程序就能更加可靠：程序計算了一個函數(shù)如果能給出該函數(shù)的規(guī)范描述，并且能夠根據(jù)程序知道它到底計算了一個什么樣的函數(shù)，那么，如果能夠證明程序所計算的函數(shù)與給定的函數(shù)等價或相同，就能證明程序的正確性，而不需再測試。38程序驗(yàn)證測試不能保證程序的正確性38形式化的規(guī)范描述任一程序都可以表示成流程圖基調(diào)：函數(shù)名：定義域

值域fun1:S1andP1S3fun2:S1andnot(P1)S3fun3:S3andnot(P3)S4fun4:S3andP3S4S2andP2=S4S2andnot(P2)=S3P1P2P3

Fcn1Fcn4Fcn3Fcn2S1S2S3S439形式化的規(guī)范描述任一程序都可以表示成流程圖P1P2P3Fcn形式化的規(guī)范描述（續(xù)）這樣，程序可以看成是一個定義在其基本成分上的復(fù)雜函數(shù)： C(fun1,fun2,fun3,fun4,p1,p2,p3):

S1

S4如果我們能夠形式化地推導(dǎo)出上述關(guān)系，那么我們就能夠從數(shù)學(xué)上證明，給定S1,程序?qū)⒔K止于狀態(tài)S4。但是：證明非常困難。另外，在證明時，我們總是想證明程序和某個給定的形式化規(guī)范等價，但問題是，如果沒有給出規(guī)范描述，“程序是否正確？”可能就沒有了意義。40形式化的規(guī)范描述（續(xù)）這樣，程序可以看成是一個定義在其基本成公理化驗(yàn)證用謂詞邏輯公式來刻畫程序的語義、用謂詞演算來驗(yàn)證程序的正確性。

TonyHoare

在1969年提出的。每個程序都遵循某種形式化的公理定義。實(shí)證（Validation）:通過一系列測試數(shù)據(jù)的測試，展示程序滿足了其規(guī)范描述。驗(yàn)證（Verification）:根據(jù)程序結(jié)構(gòu)，通過形式化的討論，展示程序滿足了其規(guī)范描述。Validation一般認(rèn)為需要執(zhí)行程序，而verification不需要。41公理化驗(yàn)證用謂詞邏輯公式來刻畫程序的語義、用謂詞演算來驗(yàn)證程謂詞邏輯公理{P1}S{P2}表示如果P1為真，則在S執(zhí)行并終止后，P2將為真。

如果A為真，則B也為真。邏輯公理：組合

順序1

順序2 {P}S1{Q},{Q}S2{R}[組合語句]{P}S1;S2{R}{P}S{R},RQ[增加后置條件]{P}S{Q} PR,{R}S{Q}[增加前置條件]{P}S{Q} 42謂詞邏輯公理{P1}S{P2}表示如果P1為真，則在語句類型的公理?xiàng)l件語句1 條件語句2While循環(huán)語句

賦值語句

{P^B}S{Q},P^not(B)Q{P}ifBthenS{Q} {P^B}S1{Q},{P^not(B)}S2{Q}{P}ifBthenS1elseS2{Q}{P^B}S{P}{P}whileBdoS{P^not(B)}，其中P為不變式

{P(e)}x:=e{P(x)}，P(x)為x的謂詞。43語句類型的公理?xiàng)l件語句1 {P^B}S{Q},P^not(公理化的程序證明給定程序：s1;s2;s3;s4;…sn及其規(guī)約：P和QP為前置條件Q為后置條件通過證明下列的謂詞來證明{P}s1;…sn{Q}：{P}s1{p1}{p1}s2{p2}…{pn-1}sn{Q}反復(fù)運(yùn)用組合公理，產(chǎn)生：{P}s1;…;sn{Q}44公理化的程序證明給定程序：s1;s2;s3;s4;…例子

{B>=0} 1 X:=B 2 Y:=0 3 whileX>0do 4 begin 5 Y:=Y+A 6 X:=X-1 7 end {Y=AB}即，給定非負(fù)的B，證明當(dāng)程序終止時，Y=A*B.45例子 {B>=0} 45證明過程概要一般通過回溯來進(jìn)行。首先，找到循環(huán)的不變式：Y為乘積的一部分，X為剩下的乘數(shù)因此，Y和X*A必須是所需的乘機(jī)，即不變式Y(jié)+X*A=A*B就是建議的不變式可以試著用(Y+X*A=A*BandX>=0)作為不變式46證明過程概要一般通過回溯來進(jìn)行。46證明賦值語句公理(6):{(Y+(X-1)A=A*BandX-1>=0)}X:=X-1{(Y+X*A=A*BandX>=0)} 賦值語句公理(5):{((Y+A)+(X-1)A=A*BandX-1>=0)}Y:=Y+A{(Y+(X-1)*A=A*BandX-1>=0)} 組合公理(5,6):{(Y+A)+(X-1)*A=A*BandX-1>=0)}Y:=Y+A;X:=X-1{(Y+X*A=A*BandX>=0)} 數(shù)學(xué)定理:Y+X*A=A*BandX>0

((Y+A)+(X-1)*A=A*BandX-1>=0) 順序語句公理:{Y+X*A=A*BandX>0}Y:=Y+A;X:=X-1{(Y+X*A=A*BandX>=0)} 數(shù)學(xué)定理:(Y+X*A=A*BandX>=0)and(X>0)Y+X*A=A*BandX>0 順序語句公理:{(Y+X*A=A*BandX>=0)and(X>0)}Y:=Y+A;X:=X-1{(Y+X*A=A*BandX>=0)}[用**來代替]While循環(huán)語句公理:** {Y+X*A=A*BandX>=0}whileX>0doY:=Y+A; X:=X-1{(Y+X*A=A*BandX>=0)andnot(X>0)}47證明賦值語句公理(6):{(Y+(X-1)A=A*Ban證明(續(xù))數(shù)學(xué)定理:(Y+X*A=A*BandX>=0)andnot(X>0)(Y+X*A=A*BandX=0)Y=AB 順序語句公理:{Y+X*A=A*BandX>=0}whileX>0doY:=Y+A;X:=X-1{Y+A*B} 賦值語句公理:{0+X*A=A*BandX>=0}Y:=0{Y+X*A=A*BandX>=0}賦值語句公理:{0+B*A=A*BandB>=0}X:=B{0+X*A=A*BandX>=0)} 組合公理:{0+B*A=A*BandB>=0}X:=B;Y:=0{Y+X*A=A*BandX>=0)} 數(shù)學(xué)定理:(B>=0)0+B*A=A*BandB>=0 順序語句公理:{B>=0}X:=B;Y:=0{Y+X*A=A*BandX>=0)} 組合公理:{B>=0}program{Y=A*B} 48證明(續(xù))數(shù)學(xué)定理:(Y+X*A=A*BandX>=公理化驗(yàn)證—小結(jié)需要為語言的所有特征建立公理，能否也為簡單數(shù)組、過程調(diào)用、參數(shù)等建立公理？即使是要證明小程序也很困難，要證明大型程序就更困難了。還不能很好地處理非數(shù)學(xué)方面的問題，處理起來極端困難。很難自動化，而手工又會導(dǎo)致大量錯誤。但是準(zhǔn)確，能夠清楚地區(qū)別“程序是什么”以及“程序是如何解決問題”

它是大多數(shù)其他驗(yàn)證方法的基礎(chǔ)，包括半形式化的規(guī)范表示法。對于關(guān)鍵應(yīng)用，付出的代價還是值得的。49公理化驗(yàn)證—小結(jié)需要為語言的所有特征建立公理，能否也為簡單數(shù)程序驗(yàn)證只有程序正確性的驗(yàn)證過程能夠自動化，程序驗(yàn)證才有實(shí)際意義但要證明那些沒有結(jié)構(gòu)化的程序、以及那些具有復(fù)雜結(jié)構(gòu)的程序的正確性，非常困難，基本上是不可能的。程序驗(yàn)證工作的研究成果通常用來指導(dǎo)程序設(shè)計語言的設(shè)計例如，在C++中加斷言等。50程序驗(yàn)證只有程序正確性的驗(yàn)證過程能夠自動化，程序驗(yàn)證才有實(shí)際ML概述ML(元語言)是一種函數(shù)式語言，其程序的形式與C或Pascal相似。

ML由RobinMilner于1970年代中期開發(fā)，是一種機(jī)器輔助形式化證明的機(jī)制。ML也可以作為一種通用符號操縱語言。1983，該語言中加入了模塊等概念，并經(jīng)過重新設(shè)計，形成了現(xiàn)在的標(biāo)準(zhǔn)ML。

ML是一種具有靜態(tài)類型、強(qiáng)類型、和函數(shù)式執(zhí)行的語言，但類型不必由程序員來指定。ML程序由若干個函數(shù)定義構(gòu)成。每個函數(shù)的類型是靜態(tài)的，函數(shù)可以返回任意類型的值。因?yàn)槭呛瘮?shù)型的語言，變量的存儲與C或Fortran語言的很不相同。ML可以通過其類型系統(tǒng)支持多態(tài)，還支持?jǐn)?shù)據(jù)抽象。51ML概述ML(元語言)是一種函數(shù)式語言，其程序的形式與ML程序例子

1fundigit(c:string):int=ord(c)-ord("0");

2(*Storevaluesasalistofcharacters*)3funSumNext(V)=ifV=[]then(print("\nSum=");0)4else(print(hd(V));5SumNext(tl(V))+digit(hd(V)));

6funSumValues(x:string):int=SumNext(explode(x));

7funProcessData()=8(letvalinfile=open_in("data.sml");9valcount=digit(input(infile,1))10in11print(SumValues(input(infile,count)))12end;13print("\n"));52ML程序例子1fundigit(c:stri把一個列表顛倒過來的函數(shù)datatypelist[a,b,c,d,e]hd(x)：列表的頭，或第一個元素tl(x)：列表的尾，或除第一個元素外的元素x::y表示頭為x，尾為y的列表x@y表示連接列表x和yfunreverse(L)=ifL=nilthennil elsereverse(tl(L))@[hd(L)];目標(biāo)：將顛倒列表變成一個更簡單的函數(shù)：列表要么是空的，否則，對表頭和表尾進(jìn)行處理將表尾顛倒，然后把表頭連到后頭。53把一個列表顛倒過來的函數(shù)datatypelist[a,ML模式匹配上面的函數(shù)也可以寫成： funreverse(x::y)=reverse(y)@[x] |reverse([])=[];在這個格式中，模式匹配就是尋找可以運(yùn)用的函數(shù)定義：如果列表不為空，則匹配x::y；否則，匹配[]。54ML模式匹配上面的函數(shù)也可以寫成：54ML的類型列表Lists:[a,b,c,d,e]所有的元素具有相同的類型元組Tuples:(“a”,1,2.3)

簡化的靜態(tài)記錄記錄Records:{1=“a”,2=1,3=2.3}

給出了選擇子的名字構(gòu)造動態(tài)的任意結(jié)構(gòu)：datatypemoney=penny|nickel|dime;valx=penny;

為常量設(shè)定值零錢的記錄： datatypechange=coinsofmoney*int; coins(penny,3)

類型為change的對象構(gòu)造函數(shù)處理零錢： funNumPennies(coins(penny,x))=x; valx=coins(penny,5); NumPennies(x); valit=5:int;55ML的類型列表Lists:[a,b,c,d,eML的結(jié)構(gòu)硬幣袋（Bagsofcoins）:datatypecoinbag=bagofcoinbag*coinbag |itemofchange|empty;funValuechange(coins(penny,X))=X |Valuechange(coins(nickel,X))=5*X |Valuechange(coins(dime,X))=10*X;funCountchange(bag(X,Y))=Countchange(X)+Countchange(Y) |Countchange(item(X))=Valuechange(X) |Countchange(Empty)=0;函數(shù)的使用： valx=bag(item(coins(dime,3)),item(coins(nickel,7))); Countchange(x); valit=65:int56ML的結(jié)構(gòu)硬幣袋（Bagsofcoins）:56演講完畢，謝謝觀看！演講完畢，謝謝觀看！第四章程序語言的性質(zhì)58第四章程序語言的性質(zhì)1語言的形式化模型BNF為描述程序設(shè)計語言的屬性提供了一種很好的手段，但并不是充分的手段。BNF回答了程序看起來象什么，但沒有回答程序是做什么的。形式化模型采用精確的數(shù)學(xué)模型來刻畫研究對象，為研究、分析和操縱研究對象提供嚴(yán)謹(jǐn)?shù)臄?shù)學(xué)工具和手段。本章將介紹下列形式化模型：形式文法：喬姆斯基文法分級語言的語義：屬性文法、指稱語義程序的驗(yàn)證59語言的形式化模型BNF為描述程序設(shè)計語言的屬性提供了一種很好4.1語言的形式化性質(zhì)喬姆斯基分級文法語言的能力604.1語言的形式化性質(zhì)喬姆斯基分級文法3喬姆斯基分級文法文法由非終結(jié)符、終結(jié)符、開始（非終結(jié)）符、及產(chǎn)生式構(gòu)成文法的類別3型文法：正則文法，定義詞法的模型2型文法：BNF文法，上下文無關(guān)文法1型文法：上下文有關(guān)文法0型文法：61喬姆斯基分級文法文法43型文法：正則文法為詞法分析器提供模型。這類文法的大多數(shù)性質(zhì)都是可判定的如，能產(chǎn)生什么樣的串、給定串是否屬于文法規(guī)定的語言、語言中的串是否有限等正則文法可以產(chǎn)生形如an的串，其中a為有限字符序列正則文法只能計數(shù)有限數(shù)常用于關(guān)鍵字或單詞掃描623型文法：正則文法為詞法分析器提供模型。52型文法—上下文無關(guān)文法產(chǎn)生式的形式為：X,其中可以是終結(jié)符和非終結(jié)符的任意序列同樣，這類文法的大多數(shù)性質(zhì)都是可判定的如，能產(chǎn)生什么樣的串、給定串是否屬于文法規(guī)定的語言、語言是否為空等可用來計數(shù)和比較兩個項(xiàng)，產(chǎn)生形如ancbn的串可以用堆棧來實(shí)現(xiàn)可用來自動產(chǎn)生程序的語法分析樹2型和3型文法的相關(guān)問題都已基本上得到解決632型文法—上下文無關(guān)文法產(chǎn)生式的形式為：X,其中1型文法—上下文有關(guān)文法產(chǎn)生式的形式為：,其中任意非終結(jié)符串，是終結(jié)符和非終結(jié)符的任意序列，但中的符號個數(shù)應(yīng)不多于的符號個數(shù)從開始符開始導(dǎo)出的串的長度是遞增的在生成串時，需要使用固定數(shù)量的存儲空間，例如識別上下文無關(guān)文法無法識別的串a(chǎn)ncnbn上下文有關(guān)文法太復(fù)雜，很難用于程序設(shè)計語言人們對上下文有關(guān)文法的很多特征還不太清楚641型文法—上下文有關(guān)文法產(chǎn)生式的形式為：,其中0型文法—非限定型文法對產(chǎn)生式的形式?jīng)]有任何限制可用來識別任意可計算的函數(shù)其大多數(shù)性質(zhì)都是不可判定的返回650型文法—非限定型文法對產(chǎn)生式的形式?jīng)]有任何限制返不可判定性不同類型的文法越來越復(fù)雜，產(chǎn)生的語言也越來越復(fù)雜，但是否說明計算機(jī)解決問題的能力可以越來越強(qiáng)，沒有限制？例如：能否編寫一個C語言程序來判斷另一個C語言程序能否結(jié)束？但這基本上是不可能的，這不是編程人員的問題，而是因?yàn)橛嬎銠C(jī)所基于的數(shù)學(xué)模型本身的局限性而導(dǎo)致的。66不可判定性不同類型的文法越來越復(fù)雜，產(chǎn)生的語言也越來越復(fù)雜，圖靈機(jī)一般來說，用一種語言編寫的程序也可以用其他另一種語言來實(shí)現(xiàn)。那么是否存在某個程序，只能用某種語言來實(shí)現(xiàn)，而用其他語言就無法實(shí)現(xiàn)？如果沒有，那么有哪些程序是其它程序設(shè)計語言無法表示的，為什么還需要那么多種不同的語言？如果我們將能夠表示所有計算的語言都稱為通用語言，那么是不是所有語言都是通用語言？如果是，是否存在更簡單的通用語言？67圖靈機(jī)一般來說，用一種語言編寫的程序也可以用其他另一種語言來圖靈機(jī)的結(jié)構(gòu)圖靈機(jī)是一種用來定義可計算函數(shù)的抽象計算機(jī)圖靈機(jī)只有一個單一的數(shù)據(jù)結(jié)構(gòu)，即一個稱為“帶子”的可變長線性數(shù)組帶子被分為很多格，每格上只包含一個字符圖靈機(jī)還有一個指針變量，稱為“讀出頭”，它總是指向帶子上的某個格。68圖靈機(jī)的結(jié)構(gòu)圖靈機(jī)是一種用來定義可計算函數(shù)的抽象計算機(jī)11圖靈機(jī)的操作圖靈機(jī)只提供幾個簡單的操作：讀出頭所指定位置的字符可以被讀出或被修改。程序可以根據(jù)讀出的值進(jìn)行轉(zhuǎn)移。讀出頭可以左右移動。如果讀出頭移動到帶子的最末端，則自動在帶子上加上一格，并賦予一個空字符作為初始值。69圖靈機(jī)的操作圖靈機(jī)只提供幾個簡單的操作：12圖靈機(jī)的運(yùn)行圖靈機(jī)開始運(yùn)行時，帶子上存放輸入數(shù)據(jù)，讀出頭指向輸入數(shù)據(jù)的最左端的字符；圖靈機(jī)根據(jù)預(yù)先編好的操作序列讀寫帶子上的數(shù)據(jù)、或移動讀出頭；如果最終能夠停機(jī)，則帶子上的內(nèi)容就是最后的輸出結(jié)果。70圖靈機(jī)的運(yùn)行圖靈機(jī)開始運(yùn)行時，帶子上存放輸入數(shù)據(jù)，讀出頭指向圖靈機(jī)的能力任意可計算函數(shù)都可以用圖靈機(jī)計算出來（Church論題）圖靈機(jī)等價于0型文法確定型圖靈機(jī)等價于非確定型圖靈機(jī)。71圖靈機(jī)的能力任意可計算函數(shù)都可以用圖靈機(jī)計算出來（Churc停機(jī)問題是否存在某個通用的算法，它能夠斷定任意給定的圖靈機(jī)在任意的輸入下能否停機(jī)？停機(jī)問題是不可判斷的，即不存在這樣的通用算法。任意一個不可判斷的問題，都等價于停機(jī)問題。結(jié)論：任何一種程序設(shè)計語言都可能代替其它語言程序設(shè)計語言不存在質(zhì)的區(qū)別，只有量的區(qū)別，如是否優(yōu)美、易用、高效等任何一種程序設(shè)計語言都有它存在的理由返回72停機(jī)問題是否存在某個通用的算法，它能夠斷定任意給定的圖靈機(jī)在4.2語言的語義程序設(shè)計語言基本上都是以上下文無關(guān)文法(特別是LR(k)文法)的核心設(shè)計的。但語法分析已經(jīng)不再是人們感興趣的研究問題了。現(xiàn)在的問題是如何確定程序的含義（即語義）。734.2語言的語義程序設(shè)計語言基本上都是以上下文無關(guān)文法(特語言的語義語言的手冊必須定義語言中每個結(jié)構(gòu)的含義，包括單獨(dú)結(jié)構(gòu)的含義以及和其他結(jié)構(gòu)組合時的含義。語言提供了不同結(jié)構(gòu)，用戶（為了寫正確的程序，預(yù)測語句的執(zhí)行效果）和實(shí)現(xiàn)者（正確地實(shí)現(xiàn)語言）需要這些結(jié)構(gòu)的精確定義。大多數(shù)語言中，形式文法用于定義語法，一段文字或例子用于定義語義，但定義是不精確的，有二義性，不同作者可能有不同理解。語義定義問題還是理論研究的目標(biāo)，但至今沒有令人滿意的解答。已有各種形式方法用于語義定義。74語言的語義語言的手冊必須定義語言中每個結(jié)構(gòu)的含義，包括單獨(dú)結(jié)語義建模（1）—文法模型對定義語言的BNF文法進(jìn)行擴(kuò)展，給出程序的語法分析樹，從樹中抽取出附加信息。屬性文法便是抽取附加信息的一種方式。75語義建模（1）—文法模型對定義語言的BNF文法進(jìn)行擴(kuò)展，給出語義建模（2）—命令或操作模型定義程序如何在某虛擬機(jī)上執(zhí)行。通常描述為一自動機(jī)，但比語法用的簡單自動機(jī)遠(yuǎn)為復(fù)雜。自動機(jī)有內(nèi)部狀態(tài)——對應(yīng)程序執(zhí)行時的內(nèi)部狀態(tài)，包括所有變量的值、執(zhí)行程序本身、以及各種系統(tǒng)定義的數(shù)據(jù)結(jié)構(gòu)。76語義建模（2）—命令或操作模型定義程序如何在某虛擬機(jī)上執(zhí)行。語義建模（2）—命令或操作模型一組形式定義的操作用于刻劃自動機(jī)內(nèi)部狀態(tài)如何改變。此外還需定義程序文本如何翻譯成自動機(jī)的初始狀態(tài)。語言的操作定義對語言如何實(shí)際執(zhí)行給出了相當(dāng)直接的抽象。也可能提出一個更抽象的模型，作為語言的軟件解釋的基礎(chǔ)。70年代的VDL（ViennaDefinitionLanguage）是一個操作方法。它擴(kuò)展語法分析樹已包含機(jī)器解釋器。計算的狀態(tài)是程序樹加上描述機(jī)器中所有數(shù)據(jù)的樹。每條語句的執(zhí)行使樹的狀態(tài)發(fā)生變化。77語義建模（2）—命令或操作模型一組形式定義的操作用于刻劃自動語義建模（3）—作用型模型試圖直接構(gòu)造每個程序的函數(shù)的定義，采用層次式的構(gòu)造方式。程序中每個基本的或程序員定義的操作代表一個數(shù)學(xué)函數(shù)。語言的程序控制結(jié)構(gòu)用于將這些函數(shù)復(fù)合為更大的序列，代表表達(dá)式和語言。語句序列和條件分叉表示為個體函數(shù)構(gòu)造而成的函數(shù)。循環(huán)通常表示為遞歸函數(shù)。最終，為整個程序?qū)С鲆粋€完整的函數(shù)模型，指稱語義歸于此類。78語義建模（3）—作用型模型試圖直接構(gòu)造每個程序的函數(shù)的定義，語義建模（4）—公理模型使用謂詞演算，每個語法結(jié)構(gòu)的語義被描述為公理或推導(dǎo)規(guī)則，用于導(dǎo)出結(jié)構(gòu)的執(zhí)行效果。從一個初始假設(shè)開始，假設(shè)輸入變量滿足一定的約束，在程序語句執(zhí)行后，使用公理和推導(dǎo)規(guī)則來推導(dǎo)其他變量值需滿足的限制，最終，程序的結(jié)果被證明滿足希望的約束（描述了它們的值和輸入值的關(guān)系）。如Hoare的公理語義。79語義建模（4）—公理模型使用謂詞演算，每個語法結(jié)構(gòu)的語義被描語義建模（5）—規(guī)約模型描述實(shí)現(xiàn)程序的各個函數(shù)的關(guān)系，只要我們可以證明一個實(shí)現(xiàn)符合了所有的函數(shù)間的關(guān)系，則稱實(shí)現(xiàn)相對于規(guī)約是正確的。代數(shù)數(shù)據(jù)類型是形式規(guī)約的一種形式。例如：實(shí)現(xiàn)棧的程序，S表示棧，則有公理，pop(push(S,x))=S任何一個實(shí)現(xiàn)如果能保持這種關(guān)系，則稱是棧的正確實(shí)現(xiàn)。80語義建模（5）—規(guī)約模型描述實(shí)現(xiàn)程序的各個函數(shù)的關(guān)系，只要我語義模型—小結(jié)上述各種形式語義模型各有優(yōu)點(diǎn)，但均不能稱為完全實(shí)用的和適用的，各有其適合范圍。操作語義為語言的實(shí)現(xiàn)提供了一種形式模型，但對用戶來說太細(xì)節(jié)公理語義易于理解，但很難用來定義復(fù)雜的程序設(shè)計語言，且缺乏對語言實(shí)現(xiàn)的支持返回81語義模型—小結(jié)上述各種形式語義模型各有優(yōu)點(diǎn)，但均不能稱為完全語義建模—屬性文法這是最早的開發(fā)語義模型的工作之一。其思想是對分析樹中的每個結(jié)點(diǎn)關(guān)聯(lián)一個函數(shù)，從而給出結(jié)點(diǎn)的語義內(nèi)容。屬性文法的創(chuàng)建過程是為文法中的每一條規(guī)則都定義相關(guān)的語義函數(shù)。繼承屬性是一個函數(shù)，它將樹中非終結(jié)符值和樹中更高層的非終結(jié)符值相關(guān)聯(lián)。換言之，任何規(guī)則右端的非終結(jié)符的函數(shù)值是左端非終結(jié)符的函數(shù)。綜合屬性是一個函數(shù)，它將左端非終結(jié)符和右端非終結(jié)符的值相關(guān)聯(lián)，這些屬性在樹中向上傳遞信息，即從樹中下層信息進(jìn)行“綜合”。82語義建模—屬性文法這是最早的開發(fā)語義模型的工作之一。25屬性文法例：考慮算術(shù)表達(dá)式的簡單文法。

E→T|E+T T→P|T×P P→I|(E)其語義通過文法中非終結(jié)符間的關(guān)系集合定義。如：下面函數(shù)生成該文法生成的任意表達(dá)式的值： 產(chǎn)生式 屬性

E→E+T Value(E1)=V(E2)+V(T) E→T V(E)=V(T) T→T×P V(T1)=V(T2)×V(P) T→P V(T)=V(P) P→I V(P)=數(shù)I的值

P→(E) V（P）=V（E）83屬性文法例：考慮算術(shù)表達(dá)式的簡單文法。26屬性文法下圖是一個屬性樹，它給出了表達(dá)式2+4×(1+2)值84屬性文法下圖是一個屬性樹，它給出了表達(dá)式2+4×(1+2)值屬性文法屬性文法可用于在語法樹中傳遞語義信息。例如，聲明信息可以通過語言的聲明產(chǎn)生式收集。沿樹向下傳的符號表信息可用于生成表達(dá)式代碼。下面屬性可加到非終結(jié)符<decl>和<declaration>來創(chuàng)建一個程序中聲明的名字集合。 產(chǎn)生式 屬性<declaration>::=<decl><declaration> decl_set(declaration1)=declaname(decl) ∪decl_set(declaration2)<declaration>::=<decl> decl_set(declaration)=decl-name(decl)<decl>::=declarex decl-name(decl)=x(decl)::=declarey decl-name(decl)=y(decl)::=declarez decl-name(decl)=z這是綜合屬性，包含程序中聲明的名字集合。該屬性可以沿樹向下傳遞，成為繼承屬性，用于正確地生成數(shù)據(jù)的代碼。85屬性文法屬性文法可用于在語法樹中傳遞語義信息。例如，聲明信息屬性文法的使用首先創(chuàng)建語法分析樹。屬性文法假設(shè)你已經(jīng)知道表達(dá)式是如何推導(dǎo)出來的，它并不關(guān)心是如何分析推導(dǎo)出來的。定義屬性的函數(shù)可以是任意給定的，因此定義屬性的過程完全是手工完成的。如果只有綜合屬性，并且文法是LR(k)，那么，屬性文法可以用來在語法分析時自動產(chǎn)程中間代碼。這就是YACC如何工作的，它利用屬性文法來計算所有非終結(jié)符的值。在構(gòu)造分析樹時，非終結(jié)符的信息逐層向上傳遞給分析樹上層的非終結(jié)符。語法分析完畢，所有屬性的值將計算出來。返回86屬性文法的使用首先創(chuàng)建語法分析樹。屬性文法假設(shè)你已經(jīng)知道表達(dá)指稱語義指稱語義是一種用來描述程序設(shè)計語言的語義的作用型語義模型指稱語義基于-演算87指稱語義指稱語義是一種用來描述程序設(shè)計語言的語義的作用型語義-演算-演算是一種和圖靈機(jī)的計算能力相當(dāng)?shù)睦碚撚嬎隳Ｐ?演算可以作為程序設(shè)計語言的函數(shù)調(diào)用的模型Algol和Lisp都采用來-演算的函數(shù)調(diào)用語義指稱語義是對-演算的擴(kuò)充，它將-演算擴(kuò)充為一種通用的數(shù)據(jù)類型理論88-演算-演算是一種和圖靈機(jī)的計算能力相當(dāng)?shù)睦碚撚嬎隳Ｐ?-演算的表達(dá)式-表達(dá)式可以遞歸地定義如下：變量名為-表達(dá)式如果M為一個-表達(dá)式，則x.M也是一個-表達(dá)式如果F和A都是-表達(dá)式，則(FA)也是-表達(dá)式，其中F為操作符，A為操作數(shù)。形式語法： -expr::=id|id.-expr|(-expr-expr)x相當(dāng)于申明參數(shù)變量x，沒有申明的變量為自由變量，否則為約束變量。x.M相當(dāng)于函數(shù)申明，其中x相當(dāng)于M的參數(shù)。例如： xx.xx.(xy)x.y(x.xy.y)89-演算的表達(dá)式-表達(dá)式可以遞歸地定義如下：32-表達(dá)式的操作-表達(dá)式只有一種操作：約簡(FA)約簡相當(dāng)于將A作為實(shí)際參數(shù)，替換F的形式參數(shù)的所有出現(xiàn)(x.MA)M’，相當(dāng)于用A替換M中x的所有自由出現(xiàn)。例如：(x.xy)y(x.(xy)x.x)

x.xyy注意：約簡并不一定能簡化原來的表達(dá)式(x.(xx)x.(xx))(x.(xx)x.(xx))……90-表達(dá)式的操作-表達(dá)式只有一種操作：約簡33指稱語義指稱語義的基本思想是定義一個語義函數(shù)（指稱函數(shù)），把程序的意義映射到某種意義清晰的數(shù)學(xué)對象（就像用中文解釋英文）作為被指的數(shù)學(xué)對象可以根據(jù)需要選擇對于簡單的程序語言，一種很自然的選擇是把程序的語義定義為（指稱為）從狀態(tài)到狀態(tài)的函數(shù)。定義語義就是定義好每個程序?qū)?yīng)的函數(shù)。程序的狀態(tài)由標(biāo)識符到值的映射集合構(gòu)成

S={id|value,…}91指稱語義指稱語義的基本思想是定義一個語義函數(shù)（指稱函數(shù)），把指稱語義表達(dá)式的語義[e]Sval語句的語義[s]SS程序的語義[m]valval92指稱語義表達(dá)式的語義35指稱語義設(shè)為程序的當(dāng)前狀態(tài)表達(dá)式的語義常數(shù)：[n]=n變量：[x]=(x)算術(shù)表達(dá)式：[e1+e2]=[e1]+[e2]語句的語義賦值語句：[x=e]=

{x|[e]}復(fù)合語句：[s1;s2]=[s2]([s1])條件語句：[ifbthens1elses2]= if[b]then[s1]else[s2]程序的語義[m]valval返回93指稱語義設(shè)為程序的當(dāng)前狀態(tài)返回36程序驗(yàn)證在編程時，人們越來越關(guān)心程序的正確性和可靠性。人們在設(shè)計程序設(shè)計語言時，也希望通過增加新的特征來增強(qiáng)程序的正確性和可靠性。我們可以用程序語義，按以下方式來探討程序的正確性問題：給定程序P，其含義是什么？即，它的規(guī)范描述S是什么？給定規(guī)范描述S，開發(fā)實(shí)現(xiàn)了該規(guī)范描述的程序P規(guī)范描述S和程序P是否完成了相同的功能（執(zhí)行了相同的函數(shù)）？相當(dāng)于語義建模問題軟件工程的核心問題程序驗(yàn)證的核心問題94程序驗(yàn)證在編程時，人們越來越關(guān)心程序的正確性和可靠性。人們在程序驗(yàn)證測試不能保證程序的正確性如果能找到不依賴于測試的保證程序正確性的方法，產(chǎn)生的程序就能更加可靠：程序計算了一個函數(shù)如果能給出該函數(shù)的規(guī)范描述，并且能夠根據(jù)程序知道它到底計算了一個什么樣的函數(shù)，那么，如果能夠證明程序所計算的函數(shù)與給定的函數(shù)等價或相同，就能證明程序的正確性，而不需再測試。95程序驗(yàn)證測試不能保證程序的正確性38形式化的規(guī)范描述任一程序都可以表示成流程圖基調(diào)：函數(shù)名：定義域

值域fun1:S1andP1S3fun2:S1andnot(P1)S3fun3:S3andnot(P3)S4fun4:S3andP3S4S2andP2=S4S2andnot(P2)=S3P1P2P3

Fcn1Fcn4Fcn3Fcn2S1S2S3S496形式化的規(guī)范描述任一程序都可以表示成流程圖P1P2P3Fcn形式化的規(guī)范描述（續(xù)）這樣，程序可以看成是一個定義在其基本成分上的復(fù)雜函數(shù)： C(fun1,fun2,fun3,fun4,p1,p2,p3):

S1

S4如果我們能夠形式化地推導(dǎo)出上述關(guān)系，那么我們就能夠從數(shù)學(xué)上證明，給定S1,程序?qū)⒔K止于狀態(tài)S4。但是：證明非常困難。另外，在證明時，我們總是想證明程序和某個給定的形式化規(guī)范等價，但問題是，如果沒有給出規(guī)范描述，“程序是否正確？”可能就沒有了意義。97形式化的規(guī)范描述（續(xù)）這樣，程序可以看成是一個定義在其基本成公理化驗(yàn)證用謂詞邏輯公式來刻畫程序的語義、用謂詞演算來驗(yàn)證程序的正確性。

TonyHoare

在1969年提出的。每個程序都遵循某種形式化的公理定義。實(shí)證（Validation）:通過一系列測試數(shù)據(jù)的測試，展示程序滿足了其規(guī)范描述。驗(yàn)證（Verification）:根據(jù)程序結(jié)構(gòu)，通過形式化的討論，展示程序滿足了其規(guī)范描述。Validation一般認(rèn)為需要執(zhí)行程序，而verification不需要。98公理化驗(yàn)證用謂詞邏輯公式來刻畫程序的語義、用謂詞演算來驗(yàn)證程謂詞邏輯公理{P1}S{P2}表示如果P1為真，則在S執(zhí)行并終止后，P2將為真。

如果A為真，則B也為真。邏輯公理：組合

順序1

順序2 {P}S1{Q},{Q}S2{R}[組合語句]{P}S1;S2{R}{P}S{R},RQ[增加后置條件]{P}S{Q} PR,{R}S{Q}[增加前置條件]{P}S{Q} 99謂詞邏輯公理{P1}S{P2}表示如果P1為真，則在語句類型的公理?xiàng)l件語句1 條件語句2While循環(huán)語句

賦值語句

{P^B}S{Q},P^not(B)Q{P}ifBthenS{Q} {P^B}S1{Q},{P^not(B)}S2{Q}{P}ifBthenS1elseS2{Q}{P^B}S{P}{P}whileBdoS{P^not(B)}，其中P為不變式

{P(e)}x:=e{P(x)}，P(x)為x的謂詞。100語句類型的公理?xiàng)l件語句1 {P^B}S{Q},P^not(公理化的程序證明給定程序：s1;s2;s3;s4;…sn及其規(guī)約：P和QP為前置條件Q為后置條件通過證明下列的謂詞來證明{P}s1;…sn{Q}：{P}s1{p1}{p1}s2{p2}…{pn-1}sn{Q}反復(fù)運(yùn)用組合公理，產(chǎn)生：{P}s1;…;sn{Q}101公理化的程序證明給定程序：s1;s2;s3;s4;…例子

{B>=0} 1 X:=B 2 Y:=0 3 whileX>0do 4 begin 5 Y:=Y+A 6 X:=X-1 7 end {Y=AB}即，給定非負(fù)的B，證明當(dāng)程序終止時，Y=A*B.102例子 {B>=0} 45證明過程概要一般通過回溯來進(jìn)行。首先，找到循環(huán)的不變式：Y為乘積的一部分，X為剩下的乘數(shù)因此，Y和X*A必須是所需的乘機(jī)，即不變式Y(jié)+X*A=A*B就是建議的不變式可以試著用(Y+X*A=A*BandX>=0)作為不變式103證明過程概要一般通過回溯來進(jìn)行。46證明賦值語句公理(6):{(Y+(X-1)A=A*BandX-1>=0)}X:=X-1{(Y+X*A=A*BandX>=0)} 賦值語句公理(5):{((Y+A)+(X-1)A=A*BandX-1>=0)}Y:=Y+A{(Y+(X-1)*A=A*BandX-1>=0)} 組合公理(5,6):{(Y+A)+(X-1)*A=A*BandX-1>=0)}Y:=Y+A;X:=X-1{(Y+X*A=A*BandX>=0)} 數(shù)學(xué)定理:Y+X*A=A*BandX>0

((Y+A)+(X-1)*A=A*BandX-1>=0) 順序語句公理:{Y+X*A=A*BandX>0}Y:=Y+A;X:=X-1{(Y+X*A=A*BandX>=0)} 數(shù)學(xué)定理:(Y+X*A=A*BandX>=0)and(X>0)Y+X*A=A*BandX>0 順序語句公理:{(Y+X*A=A*BandX>=0)and(X>0)}Y:=Y+A;X:=X-1{(Y+X*A=A*BandX>=0)}[用**來代替]While循環(huán)語句公理:** {Y+X*A=A*BandX>=0}whileX>0doY:=Y+A; X:=X-1{(Y+X*A=A*BandX>=0)andnot(X>0)}104證明賦值語句公理(6):{(Y+(X-1)A=A*Ban證明(續(xù))數(shù)學(xué)定理:(Y+X*A=A*BandX>=0)andnot(X>0)(Y+X*A=A*BandX=0)Y=AB 順序語句公理:{Y+X*A=A*BandX>=0}whileX>0doY:=Y+A;X:=X-1{Y+A*B} 賦值語句公理:{0+X*A=A*BandX>=0}Y:=0{Y+X*A=A*BandX>=0}賦值語句公理:{0+B*A=A*BandB>=0}X:=B{0+X*A=A*BandX>=0)} 組合公理:{0+B*A=A*BandB>=0}X:=B;Y:=0{Y+X*A=A*BandX>=0)} 數(shù)學(xué)定理:(B>=0)0+B*A=A*BandB>=0 順序語句公理:{B>=0}X:=B;Y:=0{Y+X*A=A*BandX>=0)} 組合公理:{B>=0}program{Y=A*B} 105證明(續(xù))數(shù)學(xué)定理:(Y+X*A=A*BandX>=公理化驗(yàn)證—小結(jié)需要為語言的所有特征建立公理，能否也為簡單數(shù)組、過程調(diào)用、參數(shù)等建立公理？即使是要證明小程序也很困難，要證明大型程序就更困難了。還不能很好地處理非數(shù)學(xué)方面的問題，處理起來極端困難。很難自動化，而手工又會導(dǎo)致大量錯誤。但是準(zhǔn)確，能夠清楚地區(qū)別“程序是什么”以及“程序是如何解決問題”

它是大多數(shù)其他驗(yàn)證方法的基礎(chǔ)，包括半形式化的規(guī)范表示法。對于關(guān)鍵應(yīng)用，付出的代價還是值得的