简介(定义 应用)

历史情况

基本方法(指称语义映象D可定义如下：)

简介

定义

指称语义学　（denotational semantics）

形式语义学的一个分支。人们用程序设计语言编制程序，命令计算机系统去加工数据。不同的计算机系统有不同的结构，因此对同一个命令的执行过程可以不同，但最终效果应该相同。指称语义学方法认为不应该将程序设计语言中各个成分的执行过程计入语言成分的语义中。语言成分的语义，应该是执行语言成分所要得到的最终效果。这是语言成分所要表达的含义，是语言成分本身所固有的，不因计算机系统的不同而改变。执行语言成分产生的最终效果被看作是语言成分的所指，称作为语言成分的指称物。这种语义学以语言成分的指称物作为语言成分的语义，故名为指称语义学。。

应用

指称语义学中用于定义语义的指称物多数是传统的数学对象，如整数、集合、映象等，故早期又称为数学语义学。这一名称容易使人误认为其他形式语义学分支是非数学的，后已不再使用。。

历史情况

指称语义学的主要思想是英国牛津大学C.斯特拉切于1964年前后提出的。美国D.斯高特创建的论域理论为指称语义学奠定了数学基础。论域理论是讨论各种语言成分指称物的数学结构，以及提供在这种数学结构上定义语言成分的语义和推导语言成分特性所必需的数学工具。。。。

IBM公司维也纳实验室在研究操作语义学方法VDL的基础上，于70年代初转向指称语义学的研究，发展了基于指称语义学方法的一整套开发软件的工程方法，称为维也纳开发方法（简称VDM）。

1976年英国一些学者发展了论域理论，提出幂论域理论，从而为定义非决定性程序的指称语义奠定了理论基础。

基本方法

1976年英国一些学者发展了论域理论，提出幂论域理论，从而为定义非确定性程序的指称语义奠定了理论基础。指称语义方法定义语言的语义基本思想是：先确定指称物，然后给出语言成分至指称物的语义映象。这个映象要求满足：

(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。。