/*本文參考部落格：http://xxxx.sina.com.cn/s/blog_49633a46010008r3.html */

指稱語義:把語言成分對映為數學物件，然後用定義在物件上的運算所表達出的語言的語義。

指稱語義方法定義語言的語義基本思想是：先確定指稱物，然後給出語言成分至指稱物的語義映象。這個映象要求滿足：

(1)每個成分都對應有指稱物；

(2)複合成分的指稱只依賴於它的子成分的指稱。

    下面以算術表示式和賦值語句及順序語句為例給以簡要說明。

    算術表示式的效果就是根據程式變數當前值計算表示式的值。程式變數的當前值可以用一個數值向量來表示。如果有k個程式變數,,…,，則k維數值向量(,,…,)表示的值為,的值為,…，的值為。程式變數的一種取值稱為程式的一個狀態。狀態的全體集合稱為狀態空間，記作State。算術表示式的值的範圍記作Num。算術表示式的指稱物就是State至Num的一個映象，也就是根據State中的任意一個元素(即程式變數的一組取值)可求得Num中對應的一個元素(即表示式在變數的這組取值下的值)。數學中的映象只反映集合間元素的對應，用映象作為語言成分的指稱物在語義的定義中就避免了涉及語言成分的執行過程。State至Num的全體映象，即全體表達式的指稱物，記作State→Num。不同表示式的指稱物是不同的，對算術表示式的語義下定義，就是要對每個算術表示式至其指稱物的一個對應下定義，故也可表示為一種映象。

    用Exp表示算術表示式的全體，那麼Exp的語義，就是Exp至指稱物集合(State,Num)的映象，記作Exp→(State→Num)常量n是一種算術表示式，變數x本身也是一種算術表示式，兩個算術表示式的和及積等也是算術表示式，故算術表示式Exp的抽象語法可用巴科斯正規化(BNF)表示：

E∷=n|x|e+e|e×e|…

指稱語義映象D可定義如下：

    第一個公式表示，無論程式處於何種狀態S，常量n的值不變，為數學中相應的量n。為了區分元語言和程式設計語言，指稱語義定義中將程式設計語言中的成分用[ |及| ]及括起來。第二個公式表示，變數在狀態S時的值為數值向量S的第i個分量。

    第三、四個公式表示，表示式(+)和×在狀態S時的值分別為子表示式和在狀態S時的值的和與積。

    表示式的抽象語法規定如何用最簡單的表示式常量和變數構成其他表示式。而表示式的語義定義也是先給出最簡單的表示式的語義，然後按照語法的構造過程去定義其他表示式的語義，使得複合成分的語義由各成分語義複合而成。這種定義語義的方法叫作結構式方法，或叫語法引導方法。指稱語義學就是一種結構式形式語義學。執行程式設計語言中的語句導致程式狀態的改變(即程式變數取值的改變)，故語句的指稱物應是State至State的映象：State→State。定義語句的語義就相當於定義映象D：

   這表示順序執行語句和，即先執行，並將執行後形成的新狀態，作為當前狀態再執行。

    實際的程式設計語言非常複雜，所定義的語義映象比之上文列舉的遠為複雜。為了允許同名變數在不同過程體中表示的值不同，指稱語義中引進環境的概念；為了刻畫程式控制的轉移又引進後續的概念，這些概念在描述和簡化語義定義中有重要的作用。

以下是在《程式設計語言概念和結構》中的敘述。

[ 指稱語義綜合產生程式結構的意義 ]

術語 " 指稱的 "(denotational) 來自其同根的動詞 " 指示 "(denote ) 。在指稱方法 中語言的結構指稱 ( 或者說表示 ) 了有關的意義 , 而這種意義通常是一些函式。表示式 a +b的意義就是一個從環境到值的函式 。

    一個指稱語義由兩部分組成 :

1) 域 , 有些像型別。它們標識出與一個語言相關的語法和語義物件。對字首表示式語言而言 , 語義物件就是值和環境 ; 語法物件則是表示式、變數、常量以及運算子等。

2) 語義規則 , 從結構成分的語義綜合產生出該結構的語義。

在指稱語義方面奠基性的貢獻是有關域和語義規則的嚴格的數學基礎。

    我們現在就來設計有關 let 表示式的語義規則。

表示式 E 的語義 , 記作[|E|], 是一個從環境到值的函式（一般來說 , 相對一個結構可以存在多種與之關聯的意義。如表示式有型別 , 也可以有值。草草 的前面加一個類似 vaI 或 type 的標記 , 就可以標識出該結構的各種不同語義類別 , 例如 var [|E|]，type[|E|] 等等）。函式應用的方式就是將函式的引數寫在函式右邊。進而令 f a b 等價於 (fa)b,f a 在b 上的應用。因此 , 表示式 E 在環境 env下的值為

       [|E|] env

在這種記述方式下 , 變數 x 在環境 env 裡的值就是

[|x|] env =lookup(x env) 這個規則可以讀作 : “ 將表示式的 x 的意義 ( 作為函式 ) 應用於環境 env, 我們將得到值 lookup(x,env) 。”

    有關求和、乘積的語義規則為

       [| plus E1 E2 |] env=[| E1|] env+[| E2|] env

       [|times E1 E2|] env=[| E1|] env*[| E2|] env

在這兩種情形下 , 表示式和它的子表示式使用的都是同一個環境。

    在有關 1et 表示式的規則裡 , 應該注意的是 , 表示式 El 用的是環境 env, 而表示式 E2則使用一個修改過的環境 ( 不同於 env):

[|let x=E1 in E2|] env=[|E2|] bind (x,[|E1|]env,env)

一個let表示式在環境 env 裡的值就是其子表示式在一個新環境裡的值 , 新環境中將 x 約束到表示式E1環境env裡的值 [|E1|]env。

指稱語義與程式驗證（來自vision.pku.edu.cn） 

指稱語義學認為，程式設計語言的語義是由其語言成份的語義決定的，而程式設計語言成份的語義應該是其本身固有的，與程式設計語言的個體實現無關。指稱語義的出發點是語言成份執行的最終結果，而不是其執行過程。這種執行結果是由語言成份形式後面隱藏的所指物決定的，故這種方式也稱為指稱語義。

指稱語義的指稱物均為數學物件，如整數、集合和對映等。指稱物的集合稱為論域。一個語言的指稱語義就是確定該語言的相關論域，並給出語法成份到論域上的語義對映。一個抽象的程式設計語言程式的語義就是指稱語義所指的數學物件在論域上的數學運算，其正確性證明就是指稱語義相應的數學運算公式的特性（遞迴型別語言成份的數學運算公式特徵就是其不動點的特徵），這些性質是可嚴格推理和證明的。