水蒸汽噴射真空泵
[拼音]:zhicheng yuyixue
[英文]:denotational semantics
形式語義學的一個分支。人們用程式設計語言編制程式,命令計算機系統去加工資料。不同的計算機系統有不同的結構,因此對同一個命令的執行過程可以不同,但最終效果應該相同。指稱語義學方法認為不應該將程式設計語言中各個成分的執行過程計入語言成分的語義中。語言成分的語義,應該是執行語言成分所要得到的最終效果。這是語言成分所要表達的含義,是語言成分本身所固有的,不因計算機系統的不同而改變。執行語言成分產生的最終效果被看作是語言成分的所指,稱作為語言成分的指稱物。這種語義學以語言成分的指稱物作為語言成分的語義,故名為指稱語義學。
指稱語義學中用於定義語義的指稱物多數是傳統的數學物件,如整數、集合、映象等,故早期又稱為數學語義學。這一名稱容易使人誤認為其他形式語義學分支是非數學的,後已不再使用。
歷史情況
指稱語義學的主要思想是英國牛津大學C.斯特拉切於1964年前後提出的。美國D.斯高特建立的論域理論為指稱語義學奠定了數學基礎。論域理論是討論各種語言成分指稱物的數學結構,以及提供在這種數學結構上定義語言成分的語義和推導語言成分特性所必需的數學工具。
IBM公司維也納實驗室在研究操作語義學方法VDL的基礎上,於70年代初轉向指稱語義學的研究,發展了基於指稱語義學方法的一整套開發軟體的工程方法,稱為維也納開發方法(簡稱VDM)。
1976年英國一些學者發展了論域理論,提出冪論域理論,從而為定義非決定性程式的指稱語義奠定了理論基礎。
基本方法
算術表示式的效果就是根據程式變數當前值計算出表示式的值。程式變數的當前值可以用一個數值向量來表示。如有k個程式變數x1x2…xk,則k維數值向量(
n
1,n
2,…,n
k)表示x1的值為n
1,x2的值為n
2,xk的值為n
k。程式變數的一種取值稱為程式的一個狀態。狀態的全體集合稱為狀態空間,記作State。算術表示式的值的範圍記作Num。算術表示式的指稱物就是State至Num的一個映象,也就是根據State中的任意一個元素(即程式變數的一組取值)可求得Num中對應的一個元素(即表示式在變數的這組取值下的值)。數學中的映象只反映集合間元素的對應,用映象作為語言成分的指稱物在語義的定義中就避免了涉及語言成分的執行過程。State至Num的全體映象,即全體表達式的指稱物,記作State→Num。不同的表示式的指稱物是不同的,對算術表示式的語義下定義,就是要對每個算術表示式至其指稱物的一個對應下定義,故也可表示為一種映象。用Exp表示算術表示式的全體,那麼Exp的語義定義,就是Exp至指稱物集合(State-Num)的映象,記作Exp→(State→Num)
常量n是一種算術表示式,變數x本身也是一種算術表示式,兩個算術表示式的和及積等也是算術表示式,故算術表示式Exp的抽象語法可用巴科斯-瑙爾正規化表示:
指稱語義映象
可定義如下:
第一個公式表示,無論程式處於何種狀態S,常量n的值不變,為數學中相應的量
n
。用黑體表示元語言中的符號,為了區分元語言和程式設計語言,指稱語義定義中將程式設計語言中的成分用[│及│]括起來。第二個公式表示,變數xi在狀態S時的值為數值向量S的第i個分量Si。
第三、四個公式表示,表示式(e1+e2)和(e1*e2)在狀態S時的值分別為子表示式e1和e2在狀態S 時的值的和與積。
表示式的抽象語法規定如何用最簡單的表示式常量和變數構成其他表示式。而表示式的語義定義也是先給出最簡單的表示式的語義,然後按照語法的構造過程去定義其他表示式的語義,使得複合成分的語義由各成分語義複合而成。這種定義語義的方法叫作結構式方法,或叫語法引導方法。指稱語義學就是一種結構式形式語義學。
執行程式設計語言中的語句,導致程式狀態的改變(即程式變數取值的改變),故語句的指稱物應是State至State的映象:State→State。定義語句的語義就相當於定義映象
:
:Sts→(State→State),
Sts表示所有語句的集合。如
表示賦值語句(xi:=e)的語義即改變狀態S 為
。
表示將S 中的第i個分量(即xi的值)改變為表示式e在狀態S 時所取的值(即[
|e|](s))。
這表示順序執行語句S1和S2,就是先執行S1,並將執行S1後形成的新狀態
作為當前狀態再執行S2。
實際的程式設計語言非常複雜,所定義的語義映象比之上文例舉的遠為複雜。為了允許同名變數在不同的過程體中表示的值不同,指稱語義中引進環境的概念;為了刻劃程式控制的轉移又引進後續的概念,這些概念在描述和簡化語義定義中有重要的作用。
程式設計語言的指稱語義獨立於語言的實施,便於語言設計者用來規定語言的語義。但已有的程式設計語言因受限於早期計算機的速度和容量,在設計階段就著重考慮實施的效率,故絕大多數的語言在設計時都從語言的實施角度來規定語言的語義,也就是用操作語義方法來規定語言的語義。新一代計算機系統不僅在速度和容量上是已有的系統所不能比擬的,而且將具有更高的智慧。這類系統中的程式設計語言是用來告訴系統要做什麼,而不必詳述如何去做。指稱語義學在未來的程式設計語言中將發揮更大的作用 。