1、第四章 程序文語的性質言語的方式化模型BNF為描畫程序設計言語的屬性提供了一種很好的手段，但并不是充分的手段。BNF回答了程序看起來象什么，但沒有回答程序是做什么的。方式化模型采用準確的數學模型來描寫研討對象，為研討、分析和支配研討對象提供嚴謹的數學工具和手段。本章將引見以下方式化模型：方式文法：喬姆斯基文法分級言語的語義：屬性文法、指稱語義程序的驗證4.1 言語的方式化性質喬姆斯基分級文法言語的才干喬姆斯基分級文法文法由非終結符、終結符、開場非終結符、及產生式構成文法的類別3型文法：正那么文法，定義詞法的模型2型文法：BNF文法，上下文無關文法1型文法：上下文有關文法0型文法：3型文法：正那

2、么文法為詞法分析器提供模型。這類文法的大多數性質都是可斷定的如，能產生什么樣的串、給定串能否屬于文法規定的言語、言語中的串能否有限等正那么文法可以產生形如an的串，其中a為有限字符序列正那么文法只能計數有限數常用于關鍵字或單詞掃描2型文法上下文無關文法產生式的方式為：X , 其中可以是終結符和非終結符的恣意序列同樣，這類文法的大多數性質都是可斷定的如，能產生什么樣的串、給定串能否屬于文法規定的言語、言語能否為空等可用來計數和比較兩個項，產生形如ancbn的串可以用堆棧來實現可用來自動產生程序的語法分析樹2型和3型文法的相關問題都已根本上得到處理1型文法上下文有關文法產生式的方式為： , 其中恣

3、意非終結符串， 是終結符和非終結符的恣意序列，但中的符號個數應不多于的符號個數從開場符開場導出的串的長度是遞增的在生成串時，需求運用固定數量的存儲空間，例如識別上下文無關文法無法識別的串ancnbn上下文有關文法太復雜，很難用于程序設計言語人們對上下文有關文法的很多特征還不太清楚0型文法非限定型文法對產生式的方式 沒有任何限制可用來識別恣意可計算的函數其大多數性質都是不可斷定的前往不可斷定性不同類型的文法越來越復雜，產生的言語也越來越復雜，但能否闡明計算機處理問題的才干可以越來越強，沒有限制？例如：能否編寫一個C言語程序來判別另一個C言語程序能否終了？但這根本上是不能夠的，這不是編程人員的問題

4、，而是由于計算機所基于的數學模型本身的局限性而導致的。圖靈機普通來說，用一種言語編寫的程序也可以用其他另一種言語來實現。那么能否存在某個程序，只能用某種言語來實現，而用其他言語就無法實現？假設沒有，那么有哪些程序是其它程序設計言語無法表示的，為什么還需求那么多種不同的言語？假設我們將可以表示一切計算的言語都稱為通用言語，那么是不是一切言語都是通用言語？假設是，能否存在更簡單的通用言語？圖靈機的構造圖靈機是一種用來定義可計算函數的籠統計算機圖靈機只需一個單一的數據構造，即一個稱為“帶子的可變長線性數組帶子被分為很多格，每格上只包含一個字符圖靈機還有一個指針變量，稱為“讀出頭，它總是指向帶子上的某

5、個格。圖靈機的操作圖靈機只提供幾個簡單的操作：讀出頭所指定位置的字符可以被讀出或被修正。程序可以根據讀出的值進展轉移。讀出頭可以左右挪動。假設讀出頭挪動到帶子的最末端，那么自動在帶子上加上一格，并賦予一個空字符作為初始值。圖靈機的運轉圖靈機開場運轉時，帶子上存放輸入數據，讀出頭指向輸入數據的最左端的字符；圖靈機根據預先編好的操作序列讀寫帶子上的數據、或挪動讀出頭；假設最終可以停機，那么帶子上的內容就是最后的輸出結果。圖靈機的才干恣意可計算函數都可以用圖靈機計算出來Church論題圖靈機等價于0型文法確定型圖靈機等價于非確定型圖靈機。停機問題能否存在某個通用的算法，它可以斷定恣意給定的圖靈機在恣

6、意的輸入下能否停機？停機問題是不可判別的，即不存在這樣的通用算法。恣意一個不可判別的問題，都等價于停機問題。結論：任何一種程序設計言語都能夠替代其它言語程序設計言語不存在質的區別，只需量的區別，如能否優美、易用、高效等任何一種程序設計言語都有它存在的理由前往4.2 言語的語義程序設計言語根本上都是以上下文無關文法(特別是 LR(k) 文法)的中心設計的。但語法分析曾經不再是人們感興趣的研討問題了。如今的問題是如何確定程序的含義即語義。言語的語義言語的手冊必需定義言語中每個構造的含義，包括單獨構造的含義以及和其他構造組合時的含義。言語提供了不同構造，用戶為了寫正確的程序，預測語句的執行效果和實現

7、者正確地實現言語需求這些構造的準確定義。大多數言語中，方式文法用于定義語法，一段文字或例子用于定義語義，但定義是不準確的，有二義性，不同作者能夠有不同了解。語義定義問題還是實際研討的目的，但至今沒有令人稱心的解答。已有各種方式方法用于語義定義。語義建模1文法模型對定義言語的BNF文法進展擴展，給出程序的語法分析樹，從樹中抽取出附加信息。屬性文法便是抽取附加信息的一種方式。語義建模2命令或操作模型定義程序如何在某虛擬機上執行。通常描畫為一自動機，但比語法用的簡單自動機遠為復雜。自動機有內部形狀對應程序執行時的內部形狀，包括一切變量的值、執行程序本身、以及各種系統定義的數據構造。語義建模2命令或操

8、作模型一組方式定義的操作用于刻劃自動機內部形狀如何改動。此外還需定義程序文本如何翻譯成自動機的初始形狀。言語的操作定義對言語如何實踐執行給出了相當直接的籠統。也能夠提出一個更籠統的模型，作為言語的軟件解釋的根底。70年代的VDLVienna Definition Language是一個操作方法。它擴展語法分析樹已包含機器解釋器。計算的形狀是程序樹加上描畫機器中一切數據的樹。每條語句的執行使樹的形狀發生變化。語義建模3作用型模型試圖直接構造每個程序的函數的定義，采用層次式的構造方式。程序中每個根本的或程序員定義的操作代表一個數學函數。言語的程序控制構造用于將這些函數復合為更大的序列，代表表達式和

9、言語。語句序列和條件分叉表示為個體函數構造而成的函數。循環通常表示為遞歸函數。最終，為整個程序導出一個完好的函數模型，指稱語義歸于此類。語義建模4公理模型運用謂詞演算，每個語法構造的語義被描畫為公理或推導規那么，用于導出構造的執行效果。從一個初始假設開場，假設輸入變量滿足一定的約束，在程序語句執行后，運用公理和推導規那么來推導其他變量值需滿足的限制，最終，程序的結果被證明滿足希望的約束描畫了它們的值和輸入值的關系。如Hoare的公理語義。 語義建模5規約模型描畫實現程序的各個函數的關系，只需我們可以證明一個實現符合了一切的函數間的關系，那么稱實現相對于規約是正確的。代數數據類型是方式規約的一種

10、方式。例如：實現棧的程序，S表示棧，那么有公理，pop(push(S,x)=S任何一個實現假設能堅持這種關系，那么稱是棧的正確實現。語義模型小結上述各種方式語義模型各有優點，但均不能稱為完全適用的和適用的，各有其適宜范圍。操作語義為言語的實現提供了一種方式模型，但對用戶來說太細節公理語義易于了解，但很難用來定義復雜的程序設計言語，且缺乏對言語實現的支持前往語義建模屬性文法這是最早的開發語義模型的任務之一。其思想是對分析樹中的每個結點關聯一個函數，從而給出結點的語義內容。屬性文法的創建過程是為文法中的每一條規那么都定義相關的語義函數。承繼屬性是一個函數，它將樹中非終結符值和樹中更高層的非終結符值

11、相關聯。換言之，任何規那么右端的非終結符的函數值是左端非終結符的函數。綜合屬性是一個函數，它將左端非終結符和右端非終結符的值相關聯，這些屬性在樹中向上傳送信息，即從樹中下層信息進展“綜合。 屬性文法例：思索算術表達式的簡單文法。ET|E+TTP|TPPI|(E)其語義經過文法中非終結符間的關系集合定義。如：下面函數生成該文法生成的恣意表達式的值：產生式屬性EE+TValue(E1)=V(E2)+V(T)ETV(E)=V(T)TTPV(T1)=V(T2)V(P)TPV(T)=V(P)PIV(P)=數I的值P(E)VP=VE 屬性文法以下圖是一個屬性樹，它給出了表達式2+4(1+2)值 屬性文法屬

12、性文法可用于在語法樹中傳送語義信息。例如，聲明信息可以經過言語的聲明產生式搜集。沿樹向下傳的符號表信息可用于生成表達式代碼。下面屬性可加到非終結符和來創建一個程序中聲明的名字集合。產生式屬性:= decl_set(declaration1)=declaname(decl) decl_set(declaration2):=decl_set(declaration)=decl-name(decl):=declare xdecl-name(decl)=x(decl):=declare ydecl-name(decl)=y(decl):=declare zdecl-name(decl)=z這是綜合屬性

13、，包含程序中聲明的名字集合。該屬性可以沿樹向下傳送，成為承繼屬性，用于正確地生成數據的代碼。屬性文法的運用首先創建語法分析樹。屬性文法假設他曾經知道表達式是如何推導出來的，它并不關懷是如何分析推導出來的。定義屬性的函數可以是恣意給定的，因此定義屬性的過程完全是手工完成的。假設只需綜合屬性，并且文法是 LR(k)，那么，屬性文法可以用來在語法分析時自動產程中間代碼。這就是 YACC 如何任務的，它利用屬性文法來計算一切非終結符的值。在構造分析樹時，非終結符的信息逐層向上傳送給分析樹上層的非終結符。語法分析終了，一切屬性的值將計算出來。前往指稱語義指稱語義是一種用來描畫程序設計言語的語義的作用型語

14、義模型指稱語義基于-演算-演算-演算是一種和圖靈機的計算才干相當的實際計算模型-演算可以作為程序設計言語的函數調用的模型Algol和Lisp都采用來-演算的函數調用語義指稱語義是對-演算的擴展，它將-演算擴展為一種通用的數據類型實際-演算的表達式-表達式可以遞歸地定義如下：變量名為-表達式假設M為一個-表達式，那么x.M也是一個-表達式假設F和A都是-表達式，那么(F A)也是-表達式，其中F為操作符，A為操作數。方式語法：-expr := id | id.-expr | (-expr -expr)x相當于聲明參數變量x，沒有聲明的變量為自在變量，否那么為約束變量。x.M相當于函數聲明，其中x

15、相當于M的參數。例如：x x.x x.(xy) x.y (x.x y.y)-表達式的操作-表達式只需一種操作：約簡(F A)約簡相當于將A作為實踐參數，交換F的方式參數的一切出現(x.M A) M，相當于用A交換M中x的一切自在出現。例如：(x.x y) y(x.(xy) x.x) x.x y y留意：約簡并不一定能簡化原來的表達式(x.(xx) x.(xx) (x.(xx) x.(xx) 指稱語義指稱語義的根本思想是定義一個語義函數指稱函數，把程序的意義映射到某種意義明晰的數學對象就像用中文解釋英文作為被指的數學對象可以根據需求選擇對于簡單的程序文語，一種很自然的選擇是把程序的語義定義為指稱

16、為從形狀到形狀的函數。定義語義就是定義好每個程序對應的函數。程序的形狀由標識符到值的映射集合構成S = id | value, 指稱語義表達式的語義e S val語句的語義s S S程序的語義m val val指稱語義設為程序的當前形狀表達式的語義常數：n = n變量：x = (x)算術表達式：e1 + e2 = e1 + e2語句的語義賦值語句：x = e = x | e復合語句：s1; s2 = s2(s1)條件語句：if b then s1 else s2 = if b then s1 else s2程序的語義m val val前往程序驗證在編程時，人們越來越關懷程序的正確性和可靠性。人

17、們在設計程序設計言語時，也希望經過添加新的特征來加強程序的正確性和可靠性。我們可以用程序語義，按以下方式來討論程序的正確性問題：給定程序P，其含義是什么？即，它的規范描畫S是什么？給定規范描畫S，開發實現了該規范描畫的程序P規范描畫S和程序P能否完成了一樣的功能執行了一樣的函數？相當于語義建模問題軟件工程的中心問題程序驗證的中心問題程序驗證測試不能保證程序的正確性假設能找到不依賴于測試的保證程序正確性的方法，產生的程序就能更加可靠：程序計算了一個函數假設能給出該函數的規范描畫，并且可以根據程序知道它究竟計算了一個什么樣的函數，那么，假設可以證明程序所計算的函數與給定的函數等價或一樣，就能證明程

18、序的正確性，而不需再測試。方式化的規范描畫任一程序都可以表示成流程圖基調：函數名：定義域 值域 fun1: S1 and P1 S3 fun2: S1 and not(P1) S3 fun3: S3 and not(P3) S4 fun4: S3 and P3 S4 S2 and P2 = S4 S2 and not(P2) = S3P1P2P3 Fcn1Fcn4Fcn3Fcn2S1S2S3S4方式化的規范描畫續這樣，程序可以看成是一個定義在其根本成分上的復雜函數：C(fun1, fun2, fun3, fun4, p1, p2, p3): S1 S4假設我們可以方式化地推導出上述關系，那么我

19、們就可以從數學上證明，給定S1, 程序將終止于形狀 S4。但是：證明非常困難。另外，在證明時，我們總是想證明程序和某個給定的方式化規范等價，但問題是，假設沒有給出規范描畫，“程序能否正確？能夠就沒有了意義。公理化驗證用謂詞邏輯公式來描寫程序的語義、用謂詞演算來驗證程序的正確性。 Tony Hoare 在1969年提出的。每個程序都遵照某種方式化的公理定義。實證Validation: 經過一系列測試數據的測試，展現程序滿足了其規范描畫。驗證Verification: 根據程序構造，經過方式化的討論，展現程序滿足了其規范描畫。Validation普通以為需求執行程序，而 verification不

20、需求。謂詞邏輯公理P1SP2 表示假設 P1 為真，那么在 S 執行并終止后，P2 將為真。假設 A 為真，那么 B 也為真。邏輯公理：組合順序1順序2PS1Q,QS2R 組合語句PS1;S2RPSR, RQ 添加后置條件PSQPR, RSQ 添加前置條件 PSQ語句類型的公理條件語句1條件語句2While循環語句賦值語句PBSQ, Pnot(B)Q Pif B then SQPBS1Q,Pnot(B)S2Q Pif B then S1 else S2QPBSPPwhile B do SP not(B)，其中 P 為不變式P(e)x:=eP(x)，P(x) 為 x 的謂詞。公理化的程序證明給定

21、程序：s1; s2; s3; s4; sn 及其規約：P 和 QP 為前置條件Q 為后置條件經過證明以下的謂詞來證明 Ps1;snQ：Ps1p1p1s2p2 pn-1snQ反復運用組合公理，產生：Ps1; ; snQ例子B=01X:=B2Y:=03while X0 do4 begin5 Y:= Y+A6 X:= X-17 endY=AB即，給定非負的 B，證明當程序終止時， Y=A*B.證明過程概要普統統過回溯來進展。首先，找到循環的不變式：Y 為乘積的一部分，X 為剩下的乘數因此，Y 和 X*A 必需是所需的乘機，即不變式Y+X*A = A*B 就是建議的不變式可以試著用 (Y+X*A=A*

22、B and X=0)作為不變式 證明賦值語句公理(6): (Y+(X-1)A=A*B and X-1=0) X:=X-1 (Y+X*A=A*B and X=0)賦值語句公理(5): (Y+A)+(X-1)A=A*B and X-1=0) Y:=Y+A (Y+(X-1)*A=A*B and X-1=0) 組合公理 (5,6): (Y+A)+(X-1)*A=A*B and X-1=0) Y:=Y+A; X:=X-1 (Y+X*A=A*B and X=0)數學定理: Y+X*A=A*B and X0 (Y+A)+(X-1)*A=A*B and X-1=0)順序語句公理: Y+X*A=A*B and

23、X0 Y:=Y+A; X:=X-1 (Y+X*A=A*B and X=0)數學定理: (Y+X*A=A*B and X=0) and (X0) Y+X*A=A*B and X0順序語句公理: (Y+X*A=A*B and X=0)and (X0) Y:=Y+A; X:=X-1 (Y+X*A=A*B and X=0) 用 * 來替代While循環語句公理: * Y+X*A=A*B and X=0while X0 do Y:=Y+A; X:=X-1 (Y+X*A=A*B and X=0) and not(X0)證明 (續)數學定理: (Y+X*A=A*B and X=0) and not(X0)

24、(Y+X*A=A*B and X=0) Y=AB順序語句公理: Y+X*A=A*B and X=0while X0 do Y:=Y+A; X:=X-1 Y+A*B賦值語句公理: 0+X*A=A*B and X=0 Y:=0 Y+X*A=A*B and X=0賦值語句公理: 0+B*A=A*B and B=0 X:=B 0+X*A=A*B and X=0) 組合公理: 0+B*A=A*B and B=0 X:=B; Y:=0 Y+X*A=A*B and X=0)數學定理: (B=0) 0+B*A=A*B and B=0順序語句公理: B=0 X:=B; Y:=0Y+X*A=A*B and X=0

25、)組合公理: B=0 program Y=A*B公理化驗證小結需求為言語的一切特征建立公理，能否也為簡單數組、過程調用、參數等建立公理？即使是要證明小程序也很困難，要證明大型程序就更困難了。還不能很好地處置非數學方面的問題，處置起來極端困難。很難自動化，而手工又會導致大量錯誤。但是準確，可以清楚地域別“程序是什么以及“程序是如何處理問題 它是大多數其他驗證方法的根底，包括半方式化的規范表示法。對于關鍵運用，付出的代價還是值得的。程序驗證只需程序正確性的驗證過程可以自動化，程序驗證才有實踐意義但要證明那些沒有構造化的程序、以及那些具有復雜構造的程序的正確性，非常困難，根本上是不能夠的。程序驗證任

26、務的研討成果通常用來指點程序設計言語的設計例如，在C+中加斷言等。ML 概述ML (元言語) 是一種函數式言語，其程序的方式與 C 或 Pascal 類似。 ML 由 Robin Milner 于1970年代中期開發，是一種機器輔助方式化證明的機制。ML 也可以作為一種通用符號支配言語。1983，該言語中參與了模塊等概念，并經過重新設計，構成了如今的規范ML。 ML 是一種具有靜態類型、強類型、和函數式執行的言語，但類型不用由程序員來指定。ML 程序由假設干個函數定義構成。每個函數的類型是靜態的，函數可以前往恣意類型的值。由于是函數型的言語，變量的存儲與C或Fortran言語的很不一樣。ML

27、可以經過其類型系統支持多態，還支持數據籠統。ML 程序例子 1 fun digit(c:string):int = ord(c)-ord(0); 2 (* Store values as a list of characters *) 3 fun SumNext(V) = if V= then (print(n Sum=); 0) 4 else (print(hd(V); 5 SumNext(tl(V)+digit(hd(V); 6 fun SumValues(x:string):int= SumNext(explode(x); 7 fun ProcessData() = 8 (let val infile = open_in(data.sml); 9 val count = digit(input(infile,1) 10 in 11 print(SumValues(input(infile,count) 12 end; 13 print(n);把一個列表顛倒過來的函數datatype list a, b, c, d, ehd(x)：列表的頭，或第一個元素tl(x)：列表的尾，或除第一個元素外的元素x:y 表示頭為 x，尾為 y 的列表xy 表示銜接列表 x 和 yfun reverse(L) = if L = nil then nilelse reverse(tl(L) h