北航研究生课程_程序语言设计原理教程_第17章

第16章第367页第16章指称语义的原理与应用指称语义学是ChristopherStrachey和DanaScott在1970年提出的。在形式化语义学的早期，人们都把注意力放在操作语义上，而Strachey和Scott则在纯数学的基础上进行语义学研究。这种方法最初也被称为数学语义学。它的优点是:不需要在计算机上实际运行程序，就能预测程序的行为，了解程序设计语言全部的涵义。另一个潜在的优点是:能够对程序进行推理，如证明两个程序等价。指称语义学的一个显著特征是:程序中的每一个短语(表达式、命令、声明等)都有其意义。而且，每个短语的意义是由它的子短语来定义的。这就对语义加上了结构，它是与语言的语法结构平行的。每个短语的语义函数就是短语的指称意义。其现代名称为指称语义学。本章先给出指称语义的基本概念，接下来研究用指称语义说明程序设计语言的基本概念，如:束定、存储、抽象与参数、基本类型与复合类型。接着讨论怎样将这些技术应用到一完整语言中，最后讨论指称语义的其它应用。16.1指称语义原理从数学的观点，一个程序可以看作是从输入到输出的映射P(I)→O，即输入域(domain)上的值，经过程序P变为输出域(range)的值。沿用这个办法，我们将程序短语集P中的某个短语p，映射为数学域上的值d。φ〖p〗→d(p∈P，d∈D)。φ为短语p的语义函数，D为语义域。当然，一个短语p可以有多个语义函数φ，ψ,ξ……同一语义函数也可以输入不同的短语p，p1，p2，……我们把语义域D中的数学实体d,或以辅助函数表达的复杂数学实体d'，称为该短语的数学指称物，即短语在语义函数下的指称语义。这样，程序的行为可以完全以数学实体表达。所以，指称语义最早称为数学语义。指称语义描述的是语义函数映射的后果，不反映如何映射的过程，更没有过程的时间性。而程序设计语言的时间性只能反映到值所表达的状态上。因此，如何把存储、环境、状态抽象为数学表达是指称语义关心的事。本节以简单的命令式语言演示如何用指称语义描述程序语义。16.1.1语义函数和辅助函数语义函数的变元是语法中的短语(当然可以是代表整个程序的短语，如PROGRAM)，其映射指称物即语义。第16章第368页例16-1描述二进制数的语义二进制数的语法:Numeral::=0(16.1-a)｜1(16.1-b)｜Numeral0(16.1-c)｜Numeral1(16.1-d)我们给出求值的语义函数:将Numeral集合中的对象映射为自然数:valuation:Numeral→Natural(16.2)这样，通过语义函数valuation，任何二进制符号串都可以得到自然数的指称解释。因此，按语法的产生式，我们给出以下语义函数:valuation〖0〗=0空心括号中的0是语法符号，后面‘0’的自然数。valuation〖1〗=1valuation〖N0〗=2×valuation〖N〗∥N∈Numeralvaluation〖N1〗=2×valuation〖N〗+1这样，对任一二进制数，如1101，返复用以上四个公式:valuation〖1101〗=2×valuatioin〖110〗+1=2×(2×valuation〖11〗)+1=2×(2×(2×valuation〖1〗+1))+1=2×(2×(2×1+1))+1=13即得到‘1101’的值的语义解释,为自然数13。对于最简单命令式语言我们再举一例。例16-2计算器命令的语义描述计算器命令的抽象语法：Com::=Expr=(16.3)Expr::=Num(16.4-a)｜Expr+Expr(16.4-b)｜Expr-Exp(16.4-c)｜Expr*Expr(16.4-d)Num::=Digit｜NumDigit(16.5)Digit::=0｜1｜2｜3｜4｜5｜6｜7｜8｜9(16.6)每条命令的执行都可以得到一整数，语义函数是:execute:Com→lnteger(16.7)第16章第369页每一表达式的求值可得到一整数，则有:evaluate:Expr→lnteger(16.8)每一个数都对应一个自然数:vlauation:Num→Natuarl(16.9)这样我们就有了三个语义函数。为了细化表达式的四种定义，则增加以下辅助函数:sum:Integer×Integer→Integer(16.10)difference:Integer×Integer→Integer(16.11)product:Integer×Integer→Integer(16.12)以下定义每个短语的语义函数:execute〖C〗=execute〖E=〗=evaluate〖E〗其中C∈Com，E∈Expr。意即每条命令执行都要对E求值。再定义Expr的四个表达式:evaluate〖N〗=valuation〖N〗(N∈Num)evaluate〖E1+E2〗=sum(evaluate〖E1〗，evaluate〖E2〗)evaluate〖E1-E2〗=difference(evaluate〖E1〗，evaluate〖E2〗)evaluate〖E1*E2〗=product(evaluate〖E1〗,evaluate〖E2〗)再定义Num的两个表达式:valuation〖D〗=D’(D∈Digit,D’∈Natural)valuation〖ND〗=10×valuation〖N〗+D’其中E1，E2∈Expr。D’是以D表示的自然数域的值。这样，对任一命令的执行其语义函数可立即得出，例如:execute〖40-3*9=〗=evaluate〖40-3*9〗=product(evaluate〖40-3〗，evaluate〖9〗)=product(difference(evaluate〖40〗，evaluate〖3〗)，evaluate〖9〗)=product(difference(valuation〖40〗，valuation〖3〗)，valuation〖9〗)=product(difference(40，3)，9)=333我们把定义短语指称的式子叫做语义方程。等号左边是某个短语的语义函数，等号的右边是子短语的语义函数和辅助函数组合的定义函数，如上述。定义函数如同普通数学函数定义，可引入新变量，如:lets=0.5×(a+b+c)insqrt(s×(s-a)×(s-b)×(s-c))还可以引入新函数，如:第16章第370页letsuccn=n+1inifn≥0thensqrt(succn)else0.0定义函数也可以引入多个参数，如上式中的a，b，c。也可以如前所述多层嵌套块的局部定义。有时引入无名函数(即λ表达式)更方便。16.1.2语义域无论作为指称物，还是辅助函数的变元和结果值都要研究域(domain)。域是具有相同性质元素值的集合。（1）基本域本书前述的基本域即最简单的域，它们是:·Character:域元素取自某字符集。·lnteger:域元素为整数。·Natural:域元素为正整数。·Truth-Value:域元素只有‘true’‘false’值。·Unit:域元素仅有一空元组()。用户可定义枚举域:Weeks=mon，tue，wed，thu，fri，sat，sun或偶数域：Even=…-2，0，2，4，6，8，…以及以基本域构造的复合域。前已讲过的:(2)笛卡儿积域D×D'元素为对偶(x，x')其中x∈D，x'∈D'。D1×D2×…Dn元素为n元组(x1，x2，…，xn)，其中xi∈Di。(3)不相交的联合域D+D'元素为对偶(leftx，rightx')其中x∈D，x'∈D'。更加复杂一些，可以定义复合域。每个子域上都可以是元组。复合域是不相交的n维域D1+D2+…Dn。例如定义形状域:shape=rectangle(Real×Real)+circleReal+point其中point是pointUnit的简写。请注意，矩形和圆都借助Real描述值，由于有标记rectangle和circle它们是不同的且不相交的域。(4)函数域D→D'元素为将D域值映射为D'域的值的函数或映射。例如lnteger→Even。第16章第371页如果D域中每个元素的映射为D'域中的元素，我们称全函数。如果域D中有的元素不能映射为D'域中的元素，我们称部分函数或偏函数。为了表达的一致性，我们假定每个域中都包含一特殊元素fail，记为⊥，则有:f(v)→⊥偏函数，v∈Vf(⊥)→⊥严格的偏函数f(⊥)→v非严格函数引入偏函数，偏函数域上元素间具有偏序关系，偏序关系‘≤’的性质是:·D域若具偏序性质，它必须包含唯一的底元素，记为⊥，且⊥≤d，d为D中任一元素。通俗解释是d得到的定义比⊥多。⊥是不对应任何值的‘值’。·若x，y∈D，x≤y此二元素具有偏序关系‘≤’，即y得到的定义比x多。这一般就复合元素而言，即x中包含的⊥比y多。·若x，y，z∈D，则偏序关系‘≤’必须是:[i]自反的，即有x≤x;[ii]反对称的，即若x≤y，y≤x，必然有x=y;[iii]传递的，即若x≤y，y≤z，必然有x≤z。偏函数对研究程序语义是极为有用的。因为任何程序运行的语义都可写成:run:Prgram→(lnput→Output)(16.13)如果递归不收敛或停机得不出输出则:run:P(Input)→⊥(16.14)此函数即偏函数。推而广之，我们在指称语义中讨论的域均具有偏序性质。(5)序列域序列域D*中的元素是零个或多个选自域D中的元素有限序列，即同构序列元素。或为nil元素，或为x·s的序列，其中元素x∈D，序列s∈D*，‘·’为连接符。例如:String=D*是序列域。它可以有以下元素:nil∥一般写法是“”‘a’·nil∥一般写法是“a”‘B’·‘u’·‘s’·‘y’·nil∥一般写法是“Busy”16.1.3命令式语言的特殊域有了以上基本域和复合域，我们可写出表达式求值和简单命令执行的语义，但还不足以描述命令式小语言，因为变量的行为是和环境，存储密切相关的。我们先讨论两个特殊的域。赋值语句总是改变变量中的值。前文已经说过这在纯数学中找不到对应。指称语义是数学语义，因此，必需为储存变量的存储和影响变量值的上下文环境作出模型。当然，有的理论为第16章第372页这两者的作用结果建立状态模型。本书是前者。(1)存储域一个抽象定义的存储器，由存储单元(槽)的集合组成，其中放可存储值。槽中的值随赋值而变。如果设想某一时刻存储槽中的值是一个存储(状态)，那么我们可以把所有存储(状态)的集合称之为Store域，其中每一元素sto就是一帧存储槽集合的快照。有一些已存入可存储值;有一些已分配了但未存入值(未定义);有一些未分配(未使用)。例如，以下图示了Store的一个快照sto。37??stoloc1loc2...............loc8图16-1存储快照sto的示意图其中1，2单元(以loc1，loc2指示)已赋了可存储值，即3，7。loc3，loc5分配了未定义。其余阴影槽未使用。我们把Location称(存储)单元域(相当于地址)，其元素为loci。把Storable称可存储值域。其元素为stble。于是，存储快照集合即为每次将存储单元映射为其状态State。为了避免混乱不设State域，则直接写:Store=Location→(storedStorable+undefined+unused)(16.15)括号内即为状态域，若设状态变量state它可取上述三种值。为了刻划存储快照，引入以下辅助函数:empty_store:Store(16.16)allocate:Store→Store×Location(16.17)deallocate:Store×Location→Store(16.18)update:Store×Location×Storable→Store(16.19)fetch:Store×Location→Storable(16.20)它们的意义是明显的。empty-store是所有单元都映射为unused的S