指称语义简介 西安电子

指称语义简介西安电子科技大学软件工程研究所

刘坚1形式化语义（动态语义）语义的形式化描述（形式化语义）对程序设计语言的设计与实现均具有重要意义；形式化语义从数学的角度(用数学的方法)研究程序设计语言的语义(最初也被称为数学语义)，使得：全面、准确了解(规定)程序设计语言的语义预测程序的行为对程序进行推理(如一程序与另一程序是否相等)形式化语义的应用语义设计程序验证程序自动生成(编译器自动构造)形式化描述语义的方法操作语义公理语义指称语义

2指称语义赋予程序的每个短语（如每个表达式、命令、声明等）意义，即将语言的语义结构强加给对应的语法结构；每个短语的意义由它的子短语来定义;每个短语的意义被称为指称，从而发展出指称语义。本章内容指称语义的基本概念；指称语义的基本技术：如何用指称语义描述程序设计语言的特性，如存贮、环境、抽象与参数、原子类型与组合类型、以及失败等。本节内容指称语义的基本概念：短语、指称、域、语义函数、函数定义的符号表示等。31.1语义函数

语义函数：用适当的数学实体表示每个短语的意义。实体被称为短语的指称（denotation）。通过将短语映射到其指称的函数，来规定程序设计语言的语义。这些函数被称为语义函数（semanticfunctions）。

语义函数：短语→指称

语法与语义的关系：语义是依附于语法的；语义是独立于语法的，反映语言的真实含意；语法、语义是多对多的映射。回顾属性文法：属性（如.type、.val等）语义规则4例1语法与语义的关系考虑二进制数，如"110"和"10101"。数字"110"欲表示数值6，而数字"10101"欲表示数值21。

数字是一个语法实体，而数值是一个语义实体。数值是一个抽象概念，它不依赖于任何特别的语法表示。数字"110"：数值：6、110等数值6：数字："110"、"6"、"Ⅵ"、"六"、"陆"等数值110：数字："110"、"6E"、"壹佰壹拾"等5例2二进制数的语法与语义Numeral::=0|1|N0|N1Natural={0,1,2,3,...}valuation:N→Naturalvalu[0]=0 valu[1]=1valu[N0]=2×valuN+0=2×valuNvalu[N1]=2×valuN+1语法：域：语义函数：语义方程：计算：valu[110]=2×valu[11]=2×(2×valu[1]＋1)=2×(2×1＋1)=6base进制：valu[i]=i (i=0,1,2...base-1) valu[Ni]=base×valu[N]+ivalu[110]=10×valu[11]=10×(10×valu[1]＋1)=10×(10×1＋1)=110N::=i|Ni(i=0,1,2...base-1)6例3一个计算器的语法与语义文法：域：语义函数：辅助函数：语义方程：Command::=Expr= (6.4)E ::=Numeral (6.5a)|E+E (6.5b)|E-E (6.5c)|E*E (6.5d)int={...,-3,-2,-1,0,1,2,3,...}execute:Command→int (6.6)evaluate:E→int (6.7)valuation:Numeral→Natural (6.8)sum:int×int→intdiff:int×int→intprod:int×int→intexec[E=]=evalE(6.9)eval[N]=valuN(6.10a)eval[E1+E2]=sum(evalE1,evalE2)(6.10b)eval[E1-E2]=diff(evalE1,evalE2)(6.10c)eval[E1*E2]=prod(evalE1,evalE2)(6.10d)7例3一个计算器的语法与语义（续）语义方程：计算：exec[E=]=evalE(6.9)eval[N]=valuN(6.10a)eval[E1+E2]=sum(evalE1,evalE2)(6.10b)eval[E1-E2]=diff(evalE1,evalE2)(6.10c)eval[E1*E2]=prod(evalE1,evalE2)(6.10d)执行命令“40-3*9=”，其中减法优先级高于乘法：exec[40-3*9=]=eval[40-3*9]by(6.9)=prod(eval[40-3],eval[9])by(6.10c)=prod(diff(eval[40],eval[3]),eval[9])by(6.10d)=prod(diff(valu[40],valu[3]),valu[9])by(6.10a)=prod(diff(40,3),9)=3338定义1.1每个短语p的意义被规定为一个在某域中的值d。称d是短语p的指称。或者说短语p由d来指称；规定域D作为短语类P的指称，并且引入一个语义函数f，它把P中的每个短语映射到它在D中的域。记为：f:P→D；通过若干语义方程来定义语义函数，每个函数对应P中的一个可区分的短语。如果P中的一个短语有子短语Q和R，则相应的语义方程式就类似如下表示：

f[...Q...R...]=...f'Q...f''R...此处f'和f''分别是Q和R的语义函数。 ■换句话说，每个短语的指称（仅）由它们子短语的指称定义，从而使得整个程序的意义自下而上得以完整定义。91.2函数定义的符号表示使用符号“let...in...”

引入新的（数学意义的）变量或函数，其含意可以非形式地解释为：“将…引入…”或“将…代入…”。例：lets=0.5*(a+b+c)insqrt(s*(s-a)*(s-b)*(s-c))letsuccn=n+1in…succm,…succ(succi))…

其中的s是变量，而succ是函数。使用函数的匿名表示忽略函数名而仅关注其实际意义。用匿名函数λn.n+1表示n→n+1，则下述均可表示为匿名函数：

succ=λn.n+1predodd=λn.true-value于是succ可以表示为：letsucc=λn.n+1in...

101.2函数定义的符号表示（续）例：lettriangle-area(a,b,c)= lets=0.5*(a+b+c)in ifs>0.0 thensqrt(s*(s-a)*(s-b)*(s-c))

elseintriangle-area(0.3,0.4,0.5)3.多个参数与let...in...结构的嵌套（或组合）。函数triangle-area的域是real×real×real→real，可以将triangle-area看作一个三元组的单一参数，a,b,c分别是它的三个分量。111.3域（Domains）<1>原子域（Primitivedomains）原子域是这样的域，它的元素是原子的值，而不是可以由更简单的值组合而来的值。原子域包括：

Character

－元素来自字符集合

Integer

－元素是零、正整数、负整数

Natural

－元素是非负整数

Truth-Value

－元素是真值false和trueUnit

－唯一元素是零元组，记为：0-tuple()域是一个值的集合，这些值被称为域的元素。指称语义中所使用的域结构有下述几种。也可以用枚举的方法来定义原子域，例如：

Denomination={dollars,cents}或者：Denomination={元、角、分}等121.3域（Domains）（续1）a.迪卡尔积域D1×D2×...×Dn的元素是有序n元组，(x1,x2,...,xn)，其中xi∈Di。当n=2时，域中元素是有序对。b.元组的构造与分解 用letx=(...)in...构造元组； 用let(...)=xin...分解元组。例2构造一个money类型的元组：letpay=(payrate×hours，dollars)in...例3将money类型分解为两个分量的乘积：

let(amount，denom)=payinamount×(ifdenom=dollarsthen100else1)

<2>迪卡尔积域（Cartesianproductdomains）例1

Money=Natural×Denomination的元素可以取： (1,dollars)、(2,cents)等。131.3域（Domains）（续2）a.异或域D1+D2+...+Dn的元素选自分量的域：x∈Di(i=1,2...n)。异或域的各分量域应被标记(命名)，以明确取自的分量。

例1异或域Shape=rectangle(Real×Real)+circleReal+point的元素：，0.4)、cirle或point(pointUnit)b.异或域分解也用let...in...，但需多重函数分情况定义例2

letsheet=rectangle(lgth,lgth/sqrt2.0)in --sheet:Shape...let area(rectangle(w，d)) =w*d --area:Shape→Real area(circler) =pi*(r*r)in...area(sheet)

<3>异或域(Disjointuniondomains)area由三个独立的公式定义141.3域（Domains）（续3）a.函数域的元素是函数或映射。每个函数域D→D'的元素是一个函数，它把D中的元素映射到D'中的元素。例1

域Integer→Truth-Value的元素，是把整型数映射到真值的函数，如odd，even，positive，negative，prime，composite等。

b.域D→D'上的一个偏（partial）函数是这样一个函数，它可以仅成功地作用于D中的部分参数。经常用偏函数来规定语义。例2若除法函数的参数对中的第二个数值是0，就不能成功地应用除法函数。假设每个域都包括一个特殊的元素fail，它可以用来作为偏函数的结果。<4>函数域（Functiondomains）回顾：151.3域（Domains）（续4）a.序列域D*中的每个元素是从D中选出的零个或多个元素的有限序列。每个序列或者是空序列nil，或者是把序列s∈D*加上前缀x∈D而得到。例1域String=Character*的元素是零个或若干个字符的序列，即任何长度的字符串。例如：

nil --习惯上写为“”

'a'.nil --习惯上写为“a”

'S'.'u'.'s'.'y'.nil --习惯上写为“Susy”b.使用由两个序列定义的函数来分解序列。例2letlength(nil)=0--length:D*→Integerlength(x.s)=1+lengthsin...<5>序列域（Sequencedomains）16本节主要内容1指称语义的基本概念：短语→指称2语义函数与指称语义的基本过程 ①语法（短语） ②域（指称） ③语义函数（短语→指称） ④语义方程与辅助函数3函数定义的符号表示 ①使用符号“let...in...”引入新的变量与函数; ②匿名函数λn.n+1 ③多个参数与let…in…结构的嵌套4域 ①原子域 ②迪卡尔积域 ③异或域 ④函数域 ⑤序列域17参考书目习题分别用二进制和十进制的指称语义，确定：(a)valuation[11]；(b)valuation[0110]；(c)valuation[10101]。为计算器增加一个求平方操作，在它的操作数之后键入“sq”键，如命令“7＋2sq=”(它的结果是81)。修改相应的指称语义。(a)

用head与tail定义串的组合与分解；(b)

如何定义substring、prefix、postfix等？DavidA.Watt“ProgrammingLanguageSyntaxandSemantics”,PrenticeHall,199118结束（2005年5月20日）19存储模型与环境模型西安电子科技大学软件工程研究所

刘坚20上节内容回顾指称语义的基本概念：将语言的意义施加于语言的结构语义函数与指称语义的基本过程 ①语法（短语） ②域（指称） ③语义函数（短语→指称） ④语义方程与辅助函数函数定义的符号表示 ①使用符号“let...in...”

引入新的变量与函数; ②匿名函数λn.n+1 ③多个参数与let…in…结构的嵌套域 ①原子域 ②迪卡尔积域 ③异或域 ④函数域 ⑤序列域21本节主要内容一、存储（Storage） 1.1存储模型 1.2存储模型举例掌握如何用指称语义描述存储与环境的动态特性和建立动态模型；如何用存储模型和环境模型描述具体的存储与环境。二、环境（Environment） 2.1环境模型 2.2环境模型举例22一、存储（Storage）存储是计算机的重要基础概念之一计算机模型：程序存储＋程序执行程序设计语言：内容可更改的变量x数学模型：内容可更改的配置（location或cell）第一类值(first-classvalues)：可以参与语言所有操作而不受限制的值(如赋值、参数传递等)，简称为值(Value)。231.1存储模型定义可以用一个公式表示为：Store=Location→(storedStorable+undefined+unused)(6.16)可以通过命令来改变存贮，如n:=13将sto映射到sto’。二者的区别是sto’中含有了值13。定义

简单存储模型是若干配置（location）的集合，每个配置有一个状态：①未使用（unused），没有被分配给任何变量。②未定义（undefined），已经被分配，但是没有值。③含有一个值（storedstorable）。可存储在配置中的值被称为可存储值（storable）。某一时刻存储的全体被称为存储瞬象（storagesnapshots），用术语存贮（store）表示。 ■

24①描述存储基本特性的辅助函数

称配置域为Location，可存储域为Storable，存贮域为Store。则存储特性可表示为下述映射：empty-store:Store(6.11)allocate:Store→Store×Location(6.12)deallocate:Store×Location→Store(6.13)update:Store×Location×Storable→Store(6.14)fetch:Store×Location→Storable(6.15)empty-store给出一个存贮，其中每一个配置都是未使用。allocate(sto)=(sto'，loc)：sto'与sto相同，但是配置loc在sto中是未使用，而在sto'中是未定义。deallocate(sto，loc)=sto'意思是：sto'与sto相同，但是配置loc在sto'中未使用。update(sto，loc，stble)=sto'意思是：sto'与sto相同，但是sto'中的配置loc含有stble。fetch(sto，loc)给出存放在sto中配置loc里的可存储值，如果loc未定义或者是未使用，给出值fail。

25辅助函数的符号表示empty-store=λloc.unused(6.17)allocatesto=letloc=any-unused-location(sto)(6.18)in(sto[loc→undefined]，loc)（sto[loc→state]=λloc'.ifloc'=locthenstateelsesto(loc')即loc被修改为state，其它保持状态不变）

找到任何一个“未使用”的配置loc，将其置为“未定义”deallocate(sto，loc)=sto[loc→unused](6.19)update(sto，loc，stble)=sto[loc→storedstble](6.20)fetch(sto，loc)=(6.21)letstored-value(storedstble)=stblestored-value(undefined)=failstored-value(unused)=failinstored-value(sto(loc))26③

举例fetch(3?$$，loc1)=3fetch(3?$$，loc2)=failfetch(3?$$，loc3)=failupdate(3?$$，loc2，7)=37$$deallocate(3?$$，loc2)=3$$$allocate(3?$$)=(3??$，loc3)或者

(3?$?，loc4)可以看出：deallocate(allocatesto)=sto fetch(update(sto，loc，stble)，loc)=stble例如：deallocate(allocate(3?$$))=(3?$$)

fetch(update(3?$$，loc2，7)，loc2)=7但是：allocate(deallocate(sto,loc))≠sto因为可以：allocate(deallocate(3?$$，loc2))≠3?$$一个具有四个配置loc1，loc2，loc3，loc4（从左到右）的存贮，其中数字、‘？’和‘＄’分别表示配置的值、未定义和未使用状态。271.2存储模型实例－无存储的计算器文法：Command::=E= (6.4)E::=Numeral (6.5a)|E+E (6.5b)|E-E (6.5c)|E*E (6.5d)域：int={...,-2,-1,0,1,2,...}辅助函数： sum:int×int→int diff:int×int→int prod:int×int→int语义函数：

execute:Command→int(6.6)

evaluate:E→int(6.7)

valuation:Numeral→Natural(6.8)语义方程：计算：exec[E=]=evalE(6.9)eval[N]=valuN(6.10a)eval[E1+E2]=sum(evalE1,evalE2)(6.10b)eval[E1-E2]=diff(evalE1,evalE2)(6.10c)eval[E1*E2]=prod(evalE1,evalE2)(6.10d)exec[40-3*9=]=eval[40-3*9]by(6.9)=prod(eval[40-3],eval[9])by(6.10d)=prod(diff(eval[40],eval[3]),eval[9])by(6.10c)=prod(diff(valu[40],valu[3]),valu[9])by(6.10a)=prod(diff(40,3),9)=333281.2存储模型实例－有存储的计算器将计算器扩充为具有存储功能，它包括两个寄存器（cells）x和y。可以键入如下形式的命令序列：

“3*37=x” “9+x=”第一条命令计算3和37的乘积，显示结果，并把结果存放在寄存器x中。第二条命令计算9和x中内容的和，并显示结果。①文法Command::=Expression= (6.22a)|E=Register (6.22b)|CC (6.22c)E::=Numeral (6.23a)|E+E(......) (6.23b)|R (6.23e)R::=x (6.24a)|y (6.24b)Command::=E=(6.4)E::=Numeral (6.5a)|E+E(6.5b)|E-E(6.5c)|E*E(6.5d)291.2存储模型实例－有存储的计算器（续1）a.命令的执行：

execute:C→(Store→Store×Integer) (6.28)（命令的指称是一个把存贮映射到存贮和整型数的函数）②域 Storable=Integer (6.25) Location={loc1，loc2} (6.26)

b.表达式的计算：

evaluate:E→(Store→Integer) (6.27)（表达式的指称是一个把存贮映射到整型数的函数（结果依赖于存贮））c.寄存器的定位：

location:R→Location (6.29)

（寄存器的指称是一个配置）③语义函数301.2存储模型实例－有存储的计算器（续2）b.表达式的计算（E→(Store→Integer)）eval[N]sto=valuN (6.30a)eval[E1+E2]sto=sum(evalE1sto，evalE2sto) (6.30b)eval[R]sto=fetch(sto，locaR) (6.30e)c.命令的执行exec[E=]sto=letint=evalEstoin(sto，int)(6.31a)（在不变的存贮sto中计算E得到的值int）a.寄存器的定位：

loca[x]=loc1(6.32a)loca[y]=loc2 (6.32b)exec[E=R]sto=letint=evalEstoin (6.31b)letsto'=update(sto，locaR，int)in(sto'，int)（给出改变了的存贮sto'和在sto中计算E得到的值int）exec[C1C2]sto= (6.31c)let(sto'，int)=execC1stoinexecC2sto'（在存贮sto中执行C1，在改变了的存贮sto'中执行C2）③语义方程下一页下下页311.2存储模型实例－有存储的计算器（续3）解：首先在sto中执行命令3*37=x，得到一个值和一个改变了的sto'，然后在sto'中执行命令9+x=，得到一个值且sto'保持不变。一开始，sto=(loc1，loc2)=(未使用，未使用)

exec[3*37=x]sto=letint=eval[3*37]stoinletsto'=update(sto,locax,int)in(sto',int)(by6.31b)=letint=prod(eval[3]sto,eval[37]sto)inletsto'=update(sto,locax,int)in(sto',int)=letint=111inletsto'=update(sto,locax,int)in(sto',int)=letsto'=update(sto,locax,111)in(sto',111)=letsto'=update(sto,loc1,111)in(sto',111)(by6.32a)=((111,未使用),111) (by6.20)即执行3*37=x之后，sto'=(111,未使用)，x获得值111且屏幕显示值111。用存储模型给出命令序列3*37=x9+x=（C1C2）的解。321.2存储模型实例－有存储的计算器（续4）

exec[9+x=]sto'=letint=eval[9+x]sto'in(sto',int) (by6.31a)=letint=sum(eval[9]sto',eval[x]sto')in(sto',int)=letint=sum(9,fetch(sto',locax))in(sto',int) (by6.30e)=letint=sum(9,fetch(sto',loc1))in(sto',int) (by6.32a)=letint=sum(9,111)in(sto',int)(by6.32a) (by6.21)=letint=120in(sto',int)=(sto',120)=((111,未使用),120)最终结果是x中获得值111，屏幕显示值120。

■

然后在sto'=(111,未使用)中执行9+x=：33二、环境（Environment）例1

开发环境：{Computer→PC，OS→Unix,PL→C++,DBMS→Oracle}例2

按语法letDinE书写的表达式如下：

①letvalm=10in②letvaln=m*minm+n假设在空环境{}中计算表达式①，第一个声明建立绑定m→10，它的作用域是表达式②。然后在环境{m→10}中计算②的子表达式"m*m"，得到结果100，因为m的每个应用出现都指称10。第二个声明建立绑定n→100，它的作用域是表达式"m+n"。于是m+n在环境{m→10，n→100}中计算并得到110。声明建立标识符和某种实体之间的绑定（bindings）。每个绑定具有一个确定的作用域（scope），如含有建立绑定的声明的块（block）。通俗地讲，环境是在一定的作用域范围内的一组绑定。可以表示为：{A→B,...}。34二、环境（Environment）（续）可绑定体的简化：通常需要经过两步才能将名字映射到它所代表的值，此处简化为一步，并且仅有integer是可绑定体。定义可表示为公式：

Environ=Identifier→(boundBindable+unbound)(6.37)③letvaln=1in④n+(letvaln=2in7*n)+n同样，空环境中计算表达式③，建立环境{n→1}，在此环境中计算表达式④，④中有一个被嵌套的子表达式letvaln=2in7*n，其中声明将环境改变为{n→2}。因此7*n=7*2=14，而：

n+(letvaln=2in7*n)+n=1+14+1=16■定义

环境是一组与作用域有关的标识符到实体的绑定。标识符在一个作用域中最多有一个绑定，被绑定的实体称为可绑定体。■例3

作用域的嵌套：352.1环境模型

①描述环境基本特性的辅助函数

若令环境域为Environ，标识符域为Identifier，可绑定体域为Bindable，则环境特性可表示为下述映射：

empty-environ:Environ (6.33)bind:Identifier×Bindable→Environ (6.34)overlay:Environ×Environ→Environ (6.35)find:Environ×Identifier→Bindable (6.36)

empty-environ

给出一个空环境{}。bind(Id，bdble)

给出由单一绑定组成的环境{Id→bdble}。overlay(env’，env)

给出一个组合环境env和env’绑定的环境；若任何标识符既被env也被env’绑定，则它在env’的绑定重置在env的绑定。find(env,Id)给出环境env中Id的可绑定体，若无就给出fail。例如：设env={i→1，j→2}，则： bind(k，3)={k→3} overlay({j→3，k→4}，env)={i→1，j→3，k→4} find(env，j)=2，而find(env，k)=fail36②辅助函数符号表示与存储模型对应：empty-store、allocate、update、fetch。问题：

deallocate？empty-environ=λId.unbound(6.38)bind(Id，bdble)=()λId'.ifId'=Idthenboundbdbleelseunboudoverlay(env'，env)=(6.40)env'(Id)≠unboundthenenv'(Id)elseenv(Id)find(env，Id)=(6.41)letbound-value(boundbdble)=bdblebound-value(unbound)=failinbound-value(env(Id))372.2环境模型实例－含有声明的语言②域：Bindable=Integer (6.44)

③语义函数：evaluate:E→(Environ→Integer)(6.45)（表达式的指称是一个从环境到整型数的映射；）elaborate:D→(Environ→Environ)(6.46)（声明的指称是一个环境到环境的映射。）①文法E::=N (6.42a)|E+E (6.42b)|...|Id (6.42c)|letDeclarationinE (6.42d)D::=valId=E (6.43)

382.2环境模型实例－含有声明的语言（续1）

④语义方程eval[N]env=valuN(6.47a)eval[E1+E2]env=sum(evalE1env，evalE2env)(6.47b)eval[Id]env=find(env，Id)(6.47c)eval[letDinE]env=()letenv'=elabDenvinevalE(overlay(env'，env))elab[valId=E]env=bind(Id，evalEenv)(6.48)计算env中数字N组成的表达式的结果就是N的值；计算env中表达式"E1+E2"的结果，是在各自env中计算E1和E2结果的和；计算env中引用标识符Id的结果是Id绑定到env的值；计算在env中形如"letDinE"表达式的结果，是计算E在一个新环境中的结果。新环境是由在env中详细描述D产生的绑定env'所覆盖得到的；详细描述在env中形如"valId=E"声明的结果，是一个从Id到由计算env中E得到的值的绑定。392.2环境模型实例－含有声明的语言（续2）⑤例：空环境env中计算：

letvaln=1inn+(letvaln=2in7*n)+n解：

eval[letvaln=1inn+(letvaln=2in7*n)+n]env=letenv'=elab[valn=1]env (by6.47d)ineval[n+(letvaln=2in7*n)+n]overlay(env',env)=letenv'=bind(n,eval[1]env) (by6.48)ineval[n+(letvaln=2in7*n)+n]overlay(env',env)=letenv'=bind(n,1)ineval[n+(letvaln=2in7*n)+n]overlay(env',env)=letenv'={n→1} (by6.39)ineval[n+(letvaln=2in7*n)+n]overlay(env',env)=eval[n+(letvaln=2in7*n)+n]env'(因为env={},所以overlay(env',env)=env'={n→1})

402.2环境模型实例－含有声明的语言（续3）=sum(eval[n+(letvaln=2in7*n)]env',eval[n]env')=sum(sum(eval[n]env',eval[letvaln=2in7*n]env'),eval[n]env')=sum(sum(find(n,env'),letenv''=elab[valn=2]env'ineval[7*n]overlay(env'',env'),find(n,env')) (by，6.47d)=sum(sum(1,letenv''=bind(n,eval[2]env') (by6.48)ineval[7*n]overlay(env'',env'),1)=sum(sum(1,letenv''=bind(n,2)eval[7*n]overlay(env'',env'),1)=sum(sum(1,letenv''={n→2}eval[7*n]overlay(env'',env'),1)=sum(sum(1,eval[7*n]overlay(env'',env'),1)=sum(sum(1,eval[7*n]env'',1)(overlay(env'',env')={n→2}=env'')=sum(sum(1,prod(eval[7]env'',eval[n]env'')),1)=...=sum(sum(1,14),1)=sum(15,1)=16 ■41内容回顾存储模型Store=Location→(storedStorable+undefined+unused)(6.16)辅助函数的符号表示：empty-store=λloc.unused(6.17)allocatesto=letloc=any-unused-location(sto)(6.18)in(sto[loc→undefined]，loc)deallocate(sto，loc)=sto[loc→unused](6.19)update(sto，loc，stble)=sto[loc→storedstble](6.20)fetch(sto，loc)=(6.21)letstored-value(storedstble)=stblestored-value(undefined)=failstored-value(unused)=failinstored-value(sto(loc))举例－带存储的计算器：文法的修改；域、语义函数、语义方程的设计42内容回顾（续）环境模型Environ=Identifier→(boundBindable+unbound)(6.37)辅助函数的符号表示：empty-environ=λId.unbound (6.38)bind(Id，bdble)= ()λId'.ifId'=Idthenboundbdbleelseunboudoverlay(env'，env)= (6.40)env'(Id)≠unboundthenenv'(Id)elseenv(Id)find(env，Id)= (6.41)letbound-value(boundbdble)=bdblebound-value(unbound)=failinbound-value(env(Id))环境强调作用域，离开作用域，绑定自然消失，故没有去绑定举例－含有声明的语言：文法的修改；域、语义函数、语义方程的设计43习题1.用带寄存器的计算器的指称语义（假设寄存器初值均为0）：(a)执行命令“x+7=”；(b)执行命令“x+7=yy*y=”。2*.拓广计算器使得它有一个大存贮的寄存器，R0，R1，R2等（x和y键由单一的R键所代替）。3.使用带声明表达式的指称语义：(a)计算环境{m→10，n→15}中的表达式“m+n”；(b)计算空环境中的表达式“letvaln=1inn+(letvaln=2in7*n)+n”。44结束（2005年5月27日）45本节主要内容抽象函数抽象过程抽象参数组合类型失败了解抽象的种类，抽象的数学模型；参数的种类，参数的数学模型；组合类型的构造，组合类型的存取；失败的数学模型，失败的传播。46一、抽象（Abstractions）

抽象是一个体现了计算的值(如函数抽象或过程抽象)。用户称计算为抽象，因为他们只能“看到”计算的结果(如有函数抽象所产生的值，或由过程的作用所改变的存储等)，而不是计算结果的方法。我们首先分别考察函数和过程抽象的语义。为简单起见，假设每个抽象具有单一(常量)参数。然后再详细地考察参数。471.1函数抽象(Functionabstractions)(不改变存储的抽象)函数抽象的使用者提供一个实参，并且只能“看到”结果值。因此函数抽象的意义应该是从实参到结果值的映射。更一般地，在规定的语言中，令Argument是实参域，Value是第一类值域。则有：Function=Argument→Value (6.62)

<1>语法扩展语法，加入函数调用（）和函数声明（）：Expression::=...|Identifier(Actual-Parameter) (6.63)Declaration::=...|funId(Formal-Parameter)=E (6.64)FP::=Id:Type-denoter (6.65)AP::=E (6.66)481.1函数抽象（续1）<2>指称假设有上下文限制：标识符必须已被声明为一个函数，并且实参必须与对应形参具有相同类型。在算术表达式中，只有整型数可以作为参数传递，并且只有整型数可以作为函数结果返回： Argument=Integer (6.67) Function=Argument→Integer (6.68)值声明绑定一个标识符到一个整型数，而函数声明绑定一个标识符到一个函数抽象。因此整型数和函数抽象均是可绑定体： Bindable=integerInteger+functionFunction (6.69)标记域491.1函数抽象（续2）<3>语义函数evaluate:E→(Environ→Integer) (3.45)elaborate:Dec→(Environ→Environ) (3.46)bind-parameter:FP→(Argument→Environ) (6.70)give-argument:AP→(Environ→Argument) (6.71)函数调用的指称和实参的指称，均象表达式一样，是一个环境到整型数的映射；函数的声明是一个绑定的集合，即环境到环境的映射；形参的指称是一个从实参到环境的函数。501.1函数抽象（续3）形参语义方程：bind-parameter[I:T]arg=bind(I，arg) (6.72)函数体内可以得到形参标识符I到实参arg（一个整型数）的绑定。实参语义方程：give-argument[E]env=evaluateEenv (6.73)函数调用的语义方程：eval[I(AP)]env= (6.74)

letfunctionfunc=find(env，I)inletarg=give-aAPenvinfuncarg<4>语义方程计算一个形如“I(AP)”表达式的结果，是函数func作用于一个实参arg。func是在环境env中绑定到I的函数抽象，arg是计算env中AP所产生的实参（假设I确实已被声明为一个函数）。511.1函数抽象（续4）函数声明的语义方程：elaborate[funI(FP)=E]env=(6.75)letfuncarg=letparenv=bind-pFParginevalE(overlay(parenv，env))inbind(I，functionfunc)详细描述形如“funcI(FP)=E”声明的结果就是一个I到func的绑定。后者是一个函数抽象，它取实参arg，绑定形参FP到arg，并且计算函数体E。计算E的环境就是函数声明的环境env，由参数绑定parenv所覆盖。521.2过程抽象(Procedureabstractions)(改变存储的抽象)一个函数体既访问其存储也访问其实参，并且两者都可能影响函数结果。一个过程体既访问其存储也访问其实参，并且两者都可能影响函数结果。不同的是，过程的工作是修改存储中的变量，即它的结果是一个(改变了的)存贮。<1>语法（例）Command::=...|Identifier(AP) (6.78)Expression::=...|Id(AP) (6.79)Declaration::=...|funcId(FP)~E (6.80a)|procId(FP)~C (6.80b)FP::=constId:Type-denoter (6.81)AP::=E (6.82)531.2过程抽象（续1）Argument=Value(6.83)Function=Argument→Store→Value(6.76)Procedure=Argument→Store→Store(6.77)Bindable=valueValue+variableLocation(6.84)+functionFunction+procedureProcedure<2>指称注意，函数体可以访问的是在调用时刻的存贮。因此，该存贮的行为就象函数体的另一个实参。所有第一类值均可作为实参；一个函数抽象映射一个实参和一个存贮到一个第一类值；一个过程抽象映射一个实参和一个存贮到一个存贮；第一类值、配置、以及函数和过程抽象，均是可绑定体；541.2过程抽象（续2）<3>语义函数exec:C→(Environ→Store→Store) (6.56)eval:E→(Environ→Store→Value) (6.57)elab:Dec→(Environ→Store→Environ×Store) (6.58)

实参和形参的语义函数：bind-p:FP→(Argument→Environ) (6.85)give-a:AP→(Environ→Store→Argument) (6.86)<4>语义方程函数调用的语义方程从（）调整而来：eval[I(AP)]envsto= (6.87)letfunctionfunc=find(env，I)inletarg=give-aAPenvstoinfuncargsto函数func作用于实参arg和调用时的存贮sto。551.2过程抽象（续3）过程调用的语义方程类似于：exec[I(AP)]envsto= (6.88)letprocedureproc=find(env，I)inletarg=give-aAPenvstoinprocargsto函数声明的语义方程与(6.75)类似，但被修改为考虑存储：elab[funcI(FP)~E]envsto=(6.89a)letfuncargsto'=letparenv=bind-pFParginevalE(overlay(parenv，env))sto'in(bind(I，functionfunc)，sto)函数体E在调用时的存贮sto'中计算(描述函数声明时的存贮没有任何影响)。过程声明的语义方程类似于：elab[procI(FP)~C]envsto= (6.89b)letprocargsto'=letparenv=bind-pFParginexecC(overlay(parenv，env))sto'in(bind(I，procedureproc)，sto)561.3参数(Parameters)为简单起见，到目前为止均假设每个函数和过程抽象具有单一的(常量)参数。下边讨论程序设计语言中所使用的、更重要的参数机制的语义。1.3.1定义性参数机制(Definitionalparametermechanisms)定义性参数机制是：在其中形式参数标识符只是在调用时绑定到相应的实参。定义性参数例子包括：常量参数（Constantparameters）变量参数（Variableparameters）过程参数（Proceduralparameters）函数参数（Functionalparameters）571.3.1定义性参数机制（续1）FP::=constId:Type-denoter (6.90a)|varId:Type-denoter (6.90b)AP::=E (6.91a)|varId (6.91b)规则（a-b）分别定义了对应于常量和变量形参的实参的语法，注意，一个变量实参由记号var所标记：因此过程调用“p(x)”无二义地传递x的值作为实参，而过程调用“p(varx)”无二义地传递对变量x的引用作为实参。<1>语法（例）<2>指称当前，一个实参可以是第一类值或者是一个配置：Argument=valueValue+variableLocation(6.92)581.3.1定义性参数机制（续2）详细描述形参的效果就是把它的标识符绑定到对应的实参。因此，一个形参的指称就是一个如（）所示的、从实参到环境的函数；实参(actual-parameter)的指称产生一个实参(argument)。bind-p:FP→(Argument→Environ) (6.93)give-a:AP→(Environ→Store→Argument) (6.94)<3>语义函数591.3.1定义性参数机制（续3）形参的语义方程如下所示：bind-p[constI:T](valueval)=bind(I，valueval) (6.95a)bind-p[varI:T](variableloc)=bind(I，variableloc) (6.95b)语义方程十分相似，唯一的区别是所希望的实参或者是第一类值，或者是一个配置。实参的语义方程如下所示：give-a[E]envsto=value(evalEenvsto) (6.96a)give-a[varI]envsto= (6.96b)letvariableloc=find(env，I)invariableloc如方程（a-b）所示，，定义性参数机制具有特别简单的语义，并且它们之间非常相似。同样地，过程和函数参数也很简单和相似（这里没有说明）。<4>语义方程601.3.2拷贝参数机制(Copyparametermechanisms)拷贝参数机制的特点是对值的拷贝。形参标识符指称过程的一个本地变量。值在进入该抽象时被拷贝进此变量，并且/或者在返回时拷贝出去。拷贝参数机制的例子如下所示：值参数（Valueparameters）结果参数（Resultparameters）值－结果参数（Value-resultparameters）<1>语法（例）FP::=valueId:Type-denoter (6.97a)|resultId:Type-denoter (6.97b)AP::=E (6.98a)|varId (6.98b)规则(a-b)分别定义了相对于值和结果形参的实参语法。当前，实参可以是如()所示的第一类值或者一个配置。611.3.2拷贝参数机制（续1）<2>指称实参可以是第一类值或者是一个配置：Argument=valueValue+variableLocation(6.92)<3>语义函数在过程的入口，一个值参数被如下处理：分配一个配置并且用实参对它初始化（第一类值），形参标识符被绑定到此配置。对结果参数的处理类似，但被分配配置的状态是未定义。在两种情况中，存贮均被修改。因此给形参一个指称，它是一个从实参和存储到环境和该存储的一个函数：copy-in:FP→(Argument→Store→Environ×Store) (6.99)

621.3.2拷贝参数机制（续2）copy-in的语义方程定义如下：copy-in[valueI:T](valueval)sto= (6.100a)let(sto'，local)=allocatestoin(bind(I，variablelocal)，update(sto'，local，val))copy-in[resultI:T](variableloc)sto=(6.100b)let(sto',local)=allocatestoin(bind(I,variablelocal)，sto')从过程返回时，值参数不产生任何影响。但是在结果参数的情况下，实参的配置被形参配置中的值所修改。因此需要给形参第二个语义函数：copy-out:FP→(Environ→Argument→Store→Store) (6.101)

copy-out的语义函数定义如下：copy-out[valueI:T]env(valueval)sto=sto )copy-out[resultI:T]env(variableloc)sto= (6.102b)letvariablelocal=find(env，I)inupdate(sto，loc，fetch(sto，local))这里env只在决定本地变量绑定到哪一个I时才需要。<4>语义方程631.3.2拷贝参数机制（续3）最后必须把过程声明的语义方程修改如下：elab[procI(FP)~C]envsto (6.103)letprocargsto'=let(parenv，sto'')=copy-inFPargsto'inletsto'''=execC(overlay(parenv，env))sto''incopy-outFPparenvargsto'''in(bind(I，procedureproc)，sto)这里，sto'是调用时的存贮。处理入口时的参数（copy-in）产生一个绑定parenv，同时也把存贮改变为sto''。执行过程体C进一步把存贮改变为sto'''。处理返回时的参数（copy-out），可能产生更多的存储改变，从而完成过程调用。641.4组合类型（Compositetypes）一个原子变量占据一个单一配置；用辅助函数fetch检查原子变量的值；用辅助函数update修改原子变量。出于两个原因，组合类型变量更复杂一些。其一，组合变量所具有的值自身是组合的，如它们由几个值的分量组成。其二，组合变量可能被有选择地修改，通过一个命令修改一个分量，而其它分量不受干扰。下边讨论的存储模型假设一个配置是最小的存储单元。它的内容可以被查看或修改；但不假设所有配置含有相等量的信息(如具有固定字大小的计算机中)；因此不同配置可以包含真值、整型数等，甚至组合值；最基本的是配置中的内容绝对不能被有选择地修改。在支持组合变量、但是不允许有选择修改这种变量的语言中，一个组合变量可以占据一个单一配置。在这种情况下，组合值和变量的出现对语言的语义影响很小。特别的，赋值命令的语义根本不受影响。651.4组合类型（续1）假设扩充核心语言IMP（例），使其具有有序对。每个对有两个可以是任意类型的分量，称为字段（fields）。特别地，每个字段自身可以是一个有序对。有序对中的字段可以被独立选择。不允许对有序对中的字段单独赋值，但是一个有序对的值可以被赋给另一个有序对（在例中将放松对有选择修改的限制）。如下程序段说明了我们希望规定的结构：constz~(true，0);varp:(bool，int);varq:(int，int)...p:=z;q:=(5，sndp+1)常量z支持一个类型为（bool，int）的对。变量p含有一个相同类型的对，变量q含有一个整型数对。表达式“sndp”选择p的第二个字段（同样“fstp”选择第一个字段）。一个形如“(...，...)”的表达式构成一个对。上述的两个赋值命令修改所有对变量（但是，现在禁止有选择的修改，如“fstq:=5”）。661.4组合类型（续2）<1>语法（例给出一个简单的例子，禁止有选择的修改）E::=... |(E，E)