結構化操作語義

50年代是計算機語言興起的年代，這一階段的早期，計算機語言的設計往往要強調其"方便"的一面，而比較忽略其"嚴格"的一面，因而對語言的語義，甚至語法，未下嚴格的定義，從語言設計者和語言使用者對同一語言的語義缺乏共同的理解，造成一定程度的混亂。后來，在50年代和60年代間，面向語法的編譯自動化理論研究得到了很大發展，使語法形式化研究的成果達到了實用化的地步。

????語法形式化問題基本解決以后，熱門逐漸把注意力集中到語義形式化方面。60年代可以說是計算機語言形式語義學正式誕生的10年，形式語義學的四大流派皆淵源于這一時期。其中1964年被認為是操作語義學和指稱語義學的誕生年代，Landin關于操作語義奠基性文章"表達式的機械化處理"和Strachey關于指稱語義的奠基性文章"關于形式語義學"都問世與這一年。

????操作語義的基本思想是用抽象的方法描述語言中每一成分的執行效果，以免所描述的語義依賴于該語言實現時所用的具體計算機。通常地做法是設計一個抽象機，定義一組抽象狀態，把語言的語法表示成抽象的形式。這種語義方法與語言實現道德關系比較緊密，但是很難用數學方法處理，而且對語義描述者個人使用的實現方法依賴很大。

????抽象機是操作語義的核心，它既是現實生活中具體計算機的抽象化，又是理論研究中自動機的高級化——向著直接反映高級語言語義的方向靠近。人們希望抽象機結構簡單合理，便于驗證語義。人們又希望抽象機功能足夠強大，便于描述高級語言的語義。由此產生了兩個兩個復雜度，一個是抽象機本身的復雜度MC，一個是（從高級語言到抽象機語言的）翻譯復雜度TC。如何恰當地組合這一對矛盾的復雜度，決定了抽象機設計的好壞。

????1981年，Plotkin提出了一種新的操作語義描述方法，稱為結構化的操作語義。Plotkin的基本思想是：復合成分的操作語義應該可以歸結為它的各個組成部分的操作語義。這樣，在證明語義正確定性時就可以使用結構化歸納法，因此，結構化操作語義的本質是把公理化方法引入操作引入操作語義之中。

????一個語言的結構化操作語義由三部組成。第一部分是語法范疇，也即在語義描述中所用到的基本語法成分；例如，一個簡單語言的語法范疇可以包括一組變量，一組常量，一組函數標識符等等。第二部分是語法規則，由于這里包括上下文有關的語法，所以也叫靜態語義。一般用 s 表示s是一個合法的語言成分，用表示：若s是一個合法的語言成分，則t也是一個合法的語言成分。典型例子如：

?

第三部分是動態語義，由一組規則（或稱公理）組成，具體描述執行一個語言成分后狀態起什么變化。規則的基本元素時組態，常用表示，意思是：當前狀態為，待執行的程序是s。因此，例如，執行一個賦值語句的語義可以描述為

?

表示執行語句x:=e后，原來狀態起了變化，其中x原來的值被表達式e的值代替。

????更多的規則取推理形式，例如，

????

????表示：若運行程序s的結果使s變為，狀態變為，則運行程序s;t 的結果是使s;t 變為, 狀態也是由變為。

????結構化操作語義簡稱為SOS（Structured Operational Semantics）。為了給出一個程序設計語言的SOS描述，應該同時列出三部分數據（或公式），包括：語法范疇，語言規則（含靜態語義）及動態語義，以后我們簡稱第二部分為靜態語義。

????語法范疇指的是該語言使用的所有語法符號。語法規則（靜態語義）給出所有合法的語句結構，其中基本規則以公理形式給出，輔助規則以推理形式給出。動態語義以轉換三元組的形式給出。

????定義1：以s表示任意語句，表示狀態（此處狀態可以理解為，例如，由全體（變量，值）偶構成的集合），則對偶稱為一個組態，表示當前狀態為，待執行語句為s，此外也稱為一個組態，表示當前狀態為，但是無語句可以執行。

????定義2：以e表示任意表達式，表示狀態，則表示在狀態之下計算表達式所得的值。

????定義3：

是一個規則，其中a為值；

是一個規則，表示從組態出發，執行一定的語句后，到達組態。當為空語句時，上式右端為;

有限多個隊則的并和交仍是規則；

若和 是規則，則

?

也是規則。表示若成立，則亦成立；

在一個具體的SOS中，若某規則r恒成立，且不為上式的形式，則r稱為公理。若有類如上式的規則成立，則稱為推理。

定義4：三元組<C,T,R>稱為一個轉換三元組，其中C是全體可能的組態的集合，T是全體終結組態的集合，R是全體公里和推理的結合，簡稱公理集合。

????終結組態是指形式為的組態，或這樣的組態，對它們不存在，使得

?

成立，并且 。

BNF是描述編程語言的文法。自然語言存在不同程度的二義性。這種模糊，不確定的方式無法精確定義一門程序設計語言。必須設計一種準確無誤地描述程序設計語言的語法結構，這種嚴謹、簡潔、易讀的形式規則描述的語言結構模型稱為文法。最著名的文法描述形式是由Backus定義Algol60語言時提出的Backus-Naur范式（Backus-Naur Form,BNF）及其擴展EBNF。BNF能一種簡潔，靈活的方式描述語言的語法。BNF范式是一種用遞歸地思想來表述計算機語言符號集的定義規范，具有如下的法則：

• ::=表示定義
• " "雙引號里的內容表示字符
• < >尖括號里的內容表示必選內容
• | 豎線兩邊的是可選內容，相當于or

現在以微型語言SL為例，說明如何用SOS來描述。下面是SL語法的BNF形式，一切細節均已略去。

<語句>::= <賦值>|<條件>|<循環>|skip|<語句>;<語句>

<賦值>::= <變量>:=<A表達式>

<條件>::= if<B 表達式> then <語句> else <語句> fi

<循環>::= while<B 表達式> do <語句> od

????下面給出它的各部分SOS描述。

語法范疇

變量集V，元素為x,y,z;

A表達式集 E,元素為

B表達式集，元素為 ;

語句集S，元素為s,t,u,v;

靜態語義（語法規則）

?

?

?

?

動態語義（轉換規則）

?

?

?

?

?

?

?

?

?

下面以一種稍微復雜的語言IMP（一種簡單的命令式語言）進行說明

IMP語言的語法范疇：

N,數集，包括正整數、負整數和零，帶符號位的正負十進制數的集合

T,真值集，T={true,false}

Loc,存儲單元集，字母開頭的字母數字串

Aexp,算術表達式集

Bexp,邏輯表達式集

Com,命令集

語法成分的元變量（約定）：

n.m表示數集N中的元素

x,y表示存儲單元集Loc中的元素

a表示算法表達式集Aexp中的元素

b表示邏輯表達式集Bexp中的元素

c表示命令集Com中的元素

轉載于:https://www.cnblogs.com/kexinxin/p/10147201.html

總結

以上是生活随笔為你收集整理的结构化操作语义的全部內容，希望文章能夠幫你解決所遇到的問題。

如果覺得生活随笔網站內容還不錯，歡迎將生活随笔推薦給好友。