指稱語義簡介 西安電子

指稱語義簡介西安電子科技大學(xué)軟件工程研究所

劉堅1形式化語義（動態(tài)語義）語義的形式化描述（形式化語義）對程序設(shè)計語言的設(shè)計與實現(xiàn)均具有重要意義；形式化語義從數(shù)學(xué)的角度(用數(shù)學(xué)的方法)研究程序設(shè)計語言的語義(最初也被稱為數(shù)學(xué)語義)，使得：全面、準(zhǔn)確了解(規(guī)定)程序設(shè)計語言的語義預(yù)測程序的行為對程序進(jìn)行推理(如一程序與另一程序是否相等)形式化語義的應(yīng)用語義設(shè)計程序驗證程序自動生成(編譯器自動構(gòu)造)形式化描述語義的方法操作語義公理語義指稱語義

2指稱語義賦予程序的每個短語（如每個表達(dá)式、命令、聲明等）意義，即將語言的語義結(jié)構(gòu)強(qiáng)加給對應(yīng)的語法結(jié)構(gòu)；每個短語的意義由它的子短語來定義;每個短語的意義被稱為指稱，從而發(fā)展出指稱語義。本章內(nèi)容指稱語義的基本概念；指稱語義的基本技術(shù)：如何用指稱語義描述程序設(shè)計語言的特性，如存貯、環(huán)境、抽象與參數(shù)、原子類型與組合類型、以及失敗等。本節(jié)內(nèi)容指稱語義的基本概念：短語、指稱、域、語義函數(shù)、函數(shù)定義的符號表示等。31.1語義函數(shù)

語義函數(shù)：用適當(dāng)?shù)臄?shù)學(xué)實體表示每個短語的意義。實體被稱為短語的指稱（denotation）。通過將短語映射到其指稱的函數(shù)，來規(guī)定程序設(shè)計語言的語義。這些函數(shù)被稱為語義函數(shù)（semanticfunctions）。

語義函數(shù)：短語→指稱

語法與語義的關(guān)系：語義是依附于語法的；語義是獨(dú)立于語法的，反映語言的真實含意；語法、語義是多對多的映射。回顧屬性文法：屬性（如.type、.val等）語義規(guī)則4例1語法與語義的關(guān)系考慮二進(jìn)制數(shù)，如"110"和"10101"。數(shù)字"110"欲表示數(shù)值6，而數(shù)字"10101"欲表示數(shù)值21。

數(shù)字是一個語法實體，而數(shù)值是一個語義實體。數(shù)值是一個抽象概念，它不依賴于任何特別的語法表示。數(shù)字"110"：數(shù)值：6、110等數(shù)值6：數(shù)字："110"、"6"、"Ⅵ"、"六"、"陸"等數(shù)值110：數(shù)字："110"、"6E"、"壹佰壹拾"等5例2二進(jìn)制數(shù)的語法與語義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語法：域：語義函數(shù)：語義方程：計算：valu[110]=2×valu[11]=2×(2×valu[1]＋1)=2×(2×1＋1)=6base進(jìn)制：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一個計算器的語法與語義文法：域：語義函數(shù)：輔助函數(shù)：語義方程：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一個計算器的語法與語義（續(xù)）語義方程：計算：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)執(zhí)行命令“40-3*9=”，其中減法優(yōu)先級高于乘法：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的意義被規(guī)定為一個在某域中的值d。稱d是短語p的指稱。或者說短語p由d來指稱；規(guī)定域D作為短語類P的指稱，并且引入一個語義函數(shù)f，它把P中的每個短語映射到它在D中的域。記為：f:P→D；通過若干語義方程來定義語義函數(shù)，每個函數(shù)對應(yīng)P中的一個可區(qū)分的短語。如果P中的一個短語有子短語Q和R，則相應(yīng)的語義方程式就類似如下表示：

f[...Q...R...]=...f'Q...f''R...此處f'和f''分別是Q和R的語義函數(shù)。 ■換句話說，每個短語的指稱（僅）由它們子短語的指稱定義，從而使得整個程序的意義自下而上得以完整定義。91.2函數(shù)定義的符號表示使用符號“l(fā)et...in...”

引入新的（數(shù)學(xué)意義的）變量或函數(shù)，其含意可以非形式地解釋為：“將…引入…”或“將…代入…”。例：lets=0.5*(a+b+c)insqrt(s*(s-a)*(s-b)*(s-c))letsuccn=n+1in…succm,…succ(succi))…

其中的s是變量，而succ是函數(shù)。使用函數(shù)的匿名表示忽略函數(shù)名而僅關(guān)注其實際意義。用匿名函數(shù)λn.n+1表示n→n+1，則下述均可表示為匿名函數(shù)：

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

101.2函數(shù)定義的符號表示（續(xù)）例：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.多個參數(shù)與let...in...結(jié)構(gòu)的嵌套（或組合）。函數(shù)triangle-area的域是real×real×real→real，可以將triangle-area看作一個三元組的單一參數(shù)，a,b,c分別是它的三個分量。111.3域（Domains）<1>原子域（Primitivedomains）原子域是這樣的域，它的元素是原子的值，而不是可以由更簡單的值組合而來的值。原子域包括：

Character

－元素來自字符集合

Integer

－元素是零、正整數(shù)、負(fù)整數(shù)

Natural

－元素是非負(fù)整數(shù)

Truth-Value

－元素是真值false和trueUnit

－唯一元素是零元組，記為：0-tuple()域是一個值的集合，這些值被稱為域的元素。指稱語義中所使用的域結(jié)構(gòu)有下述幾種。也可以用枚舉的方法來定義原子域，例如：

Denomination={dollars,cents}或者：Denomination={元、角、分}等121.3域（Domains）（續(xù)1）a.迪卡爾積域D1×D2×...×Dn的元素是有序n元組，(x1,x2,...,xn)，其中xi∈Di。當(dāng)n=2時，域中元素是有序?qū)Α.元組的構(gòu)造與分解 用letx=(...)in...構(gòu)造元組； 用let(...)=xin...分解元組。例2構(gòu)造一個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）（續(xù)2）a.異或域D1+D2+...+Dn的元素選自分量的域：x∈Di(i=1,2...n)。異或域的各分量域應(yīng)被標(biāo)記(命名)，以明確取自的分量。

例1異或域Shape=rectangle(Real×Real)+circleReal+point的元素：，0.4)、cirle或point(pointUnit)b.異或域分解也用let...in...，但需多重函數(shù)分情況定義例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由三個獨(dú)立的公式定義141.3域（Domains）（續(xù)3）a.函數(shù)域的元素是函數(shù)或映射。每個函數(shù)域D→D'的元素是一個函數(shù)，它把D中的元素映射到D'中的元素。例1

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

b.域D→D'上的一個偏（partial）函數(shù)是這樣一個函數(shù)，它可以僅成功地作用于D中的部分參數(shù)。經(jīng)常用偏函數(shù)來規(guī)定語義。例2若除法函數(shù)的參數(shù)對中的第二個數(shù)值是0，就不能成功地應(yīng)用除法函數(shù)。假設(shè)每個域都包括一個特殊的元素fail，它可以用來作為偏函數(shù)的結(jié)果。<4>函數(shù)域（Functiondomains）回顧：151.3域（Domains）（續(xù)4）a.序列域D*中的每個元素是從D中選出的零個或多個元素的有限序列。每個序列或者是空序列nil，或者是把序列s∈D*加上前綴x∈D而得到。例1域String=Character*的元素是零個或若干個字符的序列，即任何長度的字符串。例如：

nil --習(xí)慣上寫為“”

'a'.nil --習(xí)慣上寫為“a”

'S'.'u'.'s'.'y'.nil --習(xí)慣上寫為“Susy”b.使用由兩個序列定義的函數(shù)來分解序列。例2letlength(nil)=0--length:D*→Integerlength(x.s)=1+lengthsin...<5>序列域（Sequencedomains）16本節(jié)主要內(nèi)容1指稱語義的基本概念：短語→指稱2語義函數(shù)與指稱語義的基本過程 ①語法（短語） ②域（指稱） ③語義函數(shù)（短語→指稱） ④語義方程與輔助函數(shù)3函數(shù)定義的符號表示 ①使用符號“l(fā)et...in...”引入新的變量與函數(shù); ②匿名函數(shù)λn.n+1 ③多個參數(shù)與let…in…結(jié)構(gòu)的嵌套4域 ①原子域 ②迪卡爾積域 ③異或域 ④函數(shù)域 ⑤序列域17參考書目習(xí)題分別用二進(jìn)制和十進(jìn)制的指稱語義，確定：(a)valuation[11]；(b)valuation[0110]；(c)valuation[10101]。為計算器增加一個求平方操作，在它的操作數(shù)之后鍵入“sq”鍵，如命令“7＋2sq=”(它的結(jié)果是81)。修改相應(yīng)的指稱語義。(a)

用head與tail定義串的組合與分解；(b)

如何定義substring、prefix、postfix等？DavidA.Watt“ProgrammingLanguageSyntaxandSemantics”,PrenticeHall,199118結(jié)束（2005年5月20日）19存儲模型與環(huán)境模型西安電子科技大學(xué)軟件工程研究所

劉堅20上節(jié)內(nèi)容回顧指稱語義的基本概念：將語言的意義施加于語言的結(jié)構(gòu)語義函數(shù)與指稱語義的基本過程 ①語法（短語） ②域（指稱） ③語義函數(shù)（短語→指稱） ④語義方程與輔助函數(shù)函數(shù)定義的符號表示 ①使用符號“l(fā)et...in...”

引入新的變量與函數(shù); ②匿名函數(shù)λn.n+1 ③多個參數(shù)與let…in…結(jié)構(gòu)的嵌套域 ①原子域 ②迪卡爾積域 ③異或域 ④函數(shù)域 ⑤序列域21本節(jié)主要內(nèi)容一、存儲（Storage） 1.1存儲模型 1.2存儲模型舉例掌握如何用指稱語義描述存儲與環(huán)境的動態(tài)特性和建立動態(tài)模型；如何用存儲模型和環(huán)境模型描述具體的存儲與環(huán)境。二、環(huán)境（Environment） 2.1環(huán)境模型 2.2環(huán)境模型舉例22一、存儲（Storage）存儲是計算機(jī)的重要基礎(chǔ)概念之一計算機(jī)模型：程序存儲＋程序執(zhí)行程序設(shè)計語言：內(nèi)容可更改的變量x數(shù)學(xué)模型：內(nèi)容可更改的配置（location或cell）第一類值(first-classvalues)：可以參與語言所有操作而不受限制的值(如賦值、參數(shù)傳遞等)，簡稱為值(Value)。231.1存儲模型定義可以用一個公式表示為：Store=Location→(storedStorable+undefined+unused)(6.16)可以通過命令來改變存貯，如n:=13將sto映射到sto’。二者的區(qū)別是sto’中含有了值13。定義

簡單存儲模型是若干配置（location）的集合，每個配置有一個狀態(tài)：①未使用（unused），沒有被分配給任何變量。②未定義（undefined），已經(jīng)被分配，但是沒有值。③含有一個值（storedstorable）?？纱鎯υ谂渲弥械闹当环Q為可存儲值（storable）。某一時刻存儲的全體被稱為存儲瞬象（storagesnapshots），用術(shù)語存貯（store）表示。 ■

24①描述存儲基本特性的輔助函數(shù)

稱配置域為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輔助函數(shù)的符號表示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，其它保持狀態(tài)不變）

找到任何一個“未使用”的配置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（從左到右）的存貯，其中數(shù)字、‘？’和‘＄’分別表示配置的值、未定義和未使用狀態(tài)。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,...}輔助函數(shù)： sum:int×int→int diff:int×int→int prod:int×int→int語義函數(shù)：

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存儲模型實例－有存儲的計算器將計算器擴(kuò)充為具有存儲功能，它包括兩個寄存器（cells）x和y。可以鍵入如下形式的命令序列：

“3*37=x” “9+x=”第一條命令計算3和37的乘積，顯示結(jié)果，并把結(jié)果存放在寄存器x中。第二條命令計算9和x中內(nèi)容的和，并顯示結(jié)果。①文法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存儲模型實例－有存儲的計算器（續(xù)1）a.命令的執(zhí)行：

execute:C→(Store→Store×Integer) (6.28)（命令的指稱是一個把存貯映射到存貯和整型數(shù)的函數(shù)）②域 Storable=Integer (6.25) Location={loc1，loc2} (6.26)

b.表達(dá)式的計算：

evaluate:E→(Store→Integer) (6.27)（表達(dá)式的指稱是一個把存貯映射到整型數(shù)的函數(shù)（結(jié)果依賴于存貯））c.寄存器的定位：

location:R→Location (6.29)

（寄存器的指稱是一個配置）③語義函數(shù)301.2存儲模型實例－有存儲的計算器（續(xù)2）b.表達(dá)式的計算（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.命令的執(zhí)行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中執(zhí)行C1，在改變了的存貯sto'中執(zhí)行C2）③語義方程下一頁下下頁311.2存儲模型實例－有存儲的計算器（續(xù)3）解：首先在sto中執(zhí)行命令3*37=x，得到一個值和一個改變了的sto'，然后在sto'中執(zhí)行命令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)即執(zhí)行3*37=x之后，sto'=(111,未使用)，x獲得值111且屏幕顯示值111。用存儲模型給出命令序列3*37=x9+x=（C1C2）的解。321.2存儲模型實例－有存儲的計算器（續(xù)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)最終結(jié)果是x中獲得值111，屏幕顯示值120。

■

然后在sto'=(111,未使用)中執(zhí)行9+x=：33二、環(huán)境（Environment）例1

開發(fā)環(huán)境：{Computer→PC，OS→Unix,PL→C++,DBMS→Oracle}例2

按語法letDinE書寫的表達(dá)式如下：

①letvalm=10in②letvaln=m*minm+n假設(shè)在空環(huán)境{}中計算表達(dá)式①，第一個聲明建立綁定m→10，它的作用域是表達(dá)式②。然后在環(huán)境{m→10}中計算②的子表達(dá)式"m*m"，得到結(jié)果100，因為m的每個應(yīng)用出現(xiàn)都指稱10。第二個聲明建立綁定n→100，它的作用域是表達(dá)式"m+n"。于是m+n在環(huán)境{m→10，n→100}中計算并得到110。聲明建立標(biāo)識符和某種實體之間的綁定（bindings）。每個綁定具有一個確定的作用域（scope），如含有建立綁定的聲明的塊（block）。通俗地講，環(huán)境是在一定的作用域范圍內(nèi)的一組綁定?？梢员硎緸椋簕A→B,...}。34二、環(huán)境（Environment）（續(xù)）可綁定體的簡化：通常需要經(jīng)過兩步才能將名字映射到它所代表的值，此處簡化為一步，并且僅有integer是可綁定體。定義可表示為公式：

Environ=Identifier→(boundBindable+unbound)(6.37)③letvaln=1in④n+(letvaln=2in7*n)+n同樣，空環(huán)境中計算表達(dá)式③，建立環(huán)境{n→1}，在此環(huán)境中計算表達(dá)式④，④中有一個被嵌套的子表達(dá)式letvaln=2in7*n，其中聲明將環(huán)境改變?yōu)閧n→2}。因此7*n=7*2=14，而：

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

環(huán)境是一組與作用域有關(guān)的標(biāo)識符到實體的綁定。標(biāo)識符在一個作用域中最多有一個綁定，被綁定的實體稱為可綁定體?！隼?

作用域的嵌套：352.1環(huán)境模型

①描述環(huán)境基本特性的輔助函數(shù)

若令環(huán)境域為Environ，標(biāo)識符域為Identifier，可綁定體域為Bindable，則環(huán)境特性可表示為下述映射：

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

給出一個空環(huán)境{}。bind(Id，bdble)

給出由單一綁定組成的環(huán)境{Id→bdble}。overlay(env’，env)

給出一個組合環(huán)境env和env’綁定的環(huán)境；若任何標(biāo)識符既被env也被env’綁定，則它在env’的綁定重置在env的綁定。find(env,Id)給出環(huán)境env中Id的可綁定體，若無就給出fail。例如：設(shè)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②輔助函數(shù)符號表示與存儲模型對應(yīng)：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環(huán)境模型實例－含有聲明的語言②域：Bindable=Integer (6.44)

③語義函數(shù)：evaluate:E→(Environ→Integer)(6.45)（表達(dá)式的指稱是一個從環(huán)境到整型數(shù)的映射；）elaborate:D→(Environ→Environ)(6.46)（聲明的指稱是一個環(huán)境到環(huán)境的映射。）①文法E::=N (6.42a)|E+E (6.42b)|...|Id (6.42c)|letDeclarationinE (6.42d)D::=valId=E (6.43)

382.2環(huán)境模型實例－含有聲明的語言（續(xù)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中數(shù)字N組成的表達(dá)式的結(jié)果就是N的值；計算env中表達(dá)式"E1+E2"的結(jié)果，是在各自env中計算E1和E2結(jié)果的和；計算env中引用標(biāo)識符Id的結(jié)果是Id綁定到env的值；計算在env中形如"letDinE"表達(dá)式的結(jié)果，是計算E在一個新環(huán)境中的結(jié)果。新環(huán)境是由在env中詳細(xì)描述D產(chǎn)生的綁定env'所覆蓋得到的；詳細(xì)描述在env中形如"valId=E"聲明的結(jié)果，是一個從Id到由計算env中E得到的值的綁定。392.2環(huán)境模型實例－含有聲明的語言（續(xù)2）⑤例：空環(huán)境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環(huán)境模型實例－含有聲明的語言（續(xù)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內(nèi)容回顧存儲模型Store=Location→(storedStorable+undefined+unused)(6.16)輔助函數(shù)的符號表示：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))舉例－帶存儲的計算器：文法的修改；域、語義函數(shù)、語義方程的設(shè)計42內(nèi)容回顧（續(xù)）環(huán)境模型Environ=Identifier→(boundBindable+unbound)(6.37)輔助函數(shù)的符號表示：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))環(huán)境強(qiáng)調(diào)作用域，離開作用域，綁定自然消失，故沒有去綁定舉例－含有聲明的語言：文法的修改；域、語義函數(shù)、語義方程的設(shè)計43習(xí)題1.用帶寄存器的計算器的指稱語義（假設(shè)寄存器初值均為0）：(a)執(zhí)行命令“x+7=”；(b)執(zhí)行命令“x+7=yy*y=”。2*.拓廣計算器使得它有一個大存貯的寄存器，R0，R1，R2等（x和y鍵由單一的R鍵所代替）。3.使用帶聲明表達(dá)式的指稱語義：(a)計算環(huán)境{m→10，n→15}中的表達(dá)式“m+n”；(b)計算空環(huán)境中的表達(dá)式“l(fā)etvaln=1inn+(letvaln=2in7*n)+n”。44結(jié)束（2005年5月27日）45本節(jié)主要內(nèi)容抽象函數(shù)抽象過程抽象參數(shù)組合類型失敗了解抽象的種類，抽象的數(shù)學(xué)模型；參數(shù)的種類，參數(shù)的數(shù)學(xué)模型；組合類型的構(gòu)造，組合類型的存??；失敗的數(shù)學(xué)模型，失敗的傳播。46一、抽象（Abstractions）

抽象是一個體現(xiàn)了計算的值(如函數(shù)抽象或過程抽象)。用戶稱計算為抽象，因為他們只能“看到”計算的結(jié)果(如有函數(shù)抽象所產(chǎn)生的值，或由過程的作用所改變的存儲等)，而不是計算結(jié)果的方法。我們首先分別考察函數(shù)和過程抽象的語義。為簡單起見，假設(shè)每個抽象具有單一(常量)參數(shù)。然后再詳細(xì)地考察參數(shù)。471.1函數(shù)抽象(Functionabstractions)(不改變存儲的抽象)函數(shù)抽象的使用者提供一個實參，并且只能“看到”結(jié)果值。因此函數(shù)抽象的意義應(yīng)該是從實參到結(jié)果值的映射。更一般地，在規(guī)定的語言中，令A(yù)rgument是實參域，Value是第一類值域。則有：Function=Argument→Value (6.62)

<1>語法擴(kuò)展語法，加入函數(shù)調(diào)用（）和函數(shù)聲明（）：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函數(shù)抽象（續(xù)1）<2>指稱假設(shè)有上下文限制：標(biāo)識符必須已被聲明為一個函數(shù)，并且實參必須與對應(yīng)形參具有相同類型。在算術(shù)表達(dá)式中，只有整型數(shù)可以作為參數(shù)傳遞，并且只有整型數(shù)可以作為函數(shù)結(jié)果返回： Argument=Integer (6.67) Function=Argument→Integer (6.68)值聲明綁定一個標(biāo)識符到一個整型數(shù)，而函數(shù)聲明綁定一個標(biāo)識符到一個函數(shù)抽象。因此整型數(shù)和函數(shù)抽象均是可綁定體： Bindable=integerInteger+functionFunction (6.69)標(biāo)記域491.1函數(shù)抽象（續(xù)2）<3>語義函數(shù)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)函數(shù)調(diào)用的指稱和實參的指稱，均象表達(dá)式一樣，是一個環(huán)境到整型數(shù)的映射；函數(shù)的聲明是一個綁定的集合，即環(huán)境到環(huán)境的映射；形參的指稱是一個從實參到環(huán)境的函數(shù)。501.1函數(shù)抽象（續(xù)3）形參語義方程：bind-parameter[I:T]arg=bind(I，arg) (6.72)函數(shù)體內(nèi)可以得到形參標(biāo)識符I到實參arg（一個整型數(shù)）的綁定。實參語義方程：give-argument[E]env=evaluateEenv (6.73)函數(shù)調(diào)用的語義方程：eval[I(AP)]env= (6.74)

letfunctionfunc=find(env，I)inletarg=give-aAPenvinfuncarg<4>語義方程計算一個形如“I(AP)”表達(dá)式的結(jié)果，是函數(shù)func作用于一個實參arg。func是在環(huán)境env中綁定到I的函數(shù)抽象，arg是計算env中AP所產(chǎn)生的實參（假設(shè)I確實已被聲明為一個函數(shù)）。511.1函數(shù)抽象（續(xù)4）函數(shù)聲明的語義方程：elaborate[funI(FP)=E]env=(6.75)letfuncarg=letparenv=bind-pFParginevalE(overlay(parenv，env))inbind(I，functionfunc)詳細(xì)描述形如“funcI(FP)=E”聲明的結(jié)果就是一個I到func的綁定。后者是一個函數(shù)抽象，它取實參arg，綁定形參FP到arg，并且計算函數(shù)體E。計算E的環(huán)境就是函數(shù)聲明的環(huán)境env，由參數(shù)綁定parenv所覆蓋。521.2過程抽象(Procedureabstractions)(改變存儲的抽象)一個函數(shù)體既訪問其存儲也訪問其實參，并且兩者都可能影響函數(shù)結(jié)果。一個過程體既訪問其存儲也訪問其實參，并且兩者都可能影響函數(shù)結(jié)果。不同的是，過程的工作是修改存儲中的變量，即它的結(jié)果是一個(改變了的)存貯。<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過程抽象（續(xù)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>指稱注意，函數(shù)體可以訪問的是在調(diào)用時刻的存貯。因此，該存貯的行為就象函數(shù)體的另一個實參。所有第一類值均可作為實參；一個函數(shù)抽象映射一個實參和一個存貯到一個第一類值；一個過程抽象映射一個實參和一個存貯到一個存貯；第一類值、配置、以及函數(shù)和過程抽象，均是可綁定體；541.2過程抽象（續(xù)2）<3>語義函數(shù)exec:C→(Environ→Store→Store) (6.56)eval:E→(Environ→Store→Value) (6.57)elab:Dec→(Environ→Store→Environ×Store) (6.58)

實參和形參的語義函數(shù)：bind-p:FP→(Argument→Environ) (6.85)give-a:AP→(Environ→Store→Argument) (6.86)<4>語義方程函數(shù)調(diào)用的語義方程從（）調(diào)整而來：eval[I(AP)]envsto= (6.87)letfunctionfunc=find(env，I)inletarg=give-aAPenvstoinfuncargsto函數(shù)func作用于實參arg和調(diào)用時的存貯sto。551.2過程抽象（續(xù)3）過程調(diào)用的語義方程類似于：exec[I(AP)]envsto= (6.88)letprocedureproc=find(env，I)inletarg=give-aAPenvstoinprocargsto函數(shù)聲明的語義方程與(6.75)類似，但被修改為考慮存儲：elab[funcI(FP)~E]envsto=(6.89a)letfuncargsto'=letparenv=bind-pFParginevalE(overlay(parenv，env))sto'in(bind(I，functionfunc)，sto)函數(shù)體E在調(diào)用時的存貯sto'中計算(描述函數(shù)聲明時的存貯沒有任何影響)。過程聲明的語義方程類似于：elab[procI(FP)~C]envsto= (6.89b)letprocargsto'=letparenv=bind-pFParginexecC(overlay(parenv，env))sto'in(bind(I，procedureproc)，sto)561.3參數(shù)(Parameters)為簡單起見，到目前為止均假設(shè)每個函數(shù)和過程抽象具有單一的(常量)參數(shù)。下邊討論程序設(shè)計語言中所使用的、更重要的參數(shù)機(jī)制的語義。1.3.1定義性參數(shù)機(jī)制(Definitionalparametermechanisms)定義性參數(shù)機(jī)制是：在其中形式參數(shù)標(biāo)識符只是在調(diào)用時綁定到相應(yīng)的實參。定義性參數(shù)例子包括：常量參數(shù)（Constantparameters）變量參數(shù)（Variableparameters）過程參數(shù)（Proceduralparameters）函數(shù)參數(shù)（Functionalparameters）571.3.1定義性參數(shù)機(jī)制（續(xù)1）FP::=constId:Type-denoter (6.90a)|varId:Type-denoter (6.90b)AP::=E (6.91a)|varId (6.91b)規(guī)則（a-b）分別定義了對應(yīng)于常量和變量形參的實參的語法，注意，一個變量實參由記號var所標(biāo)記：因此過程調(diào)用“p(x)”無二義地傳遞x的值作為實參，而過程調(diào)用“p(varx)”無二義地傳遞對變量x的引用作為實參。<1>語法（例）<2>指稱當(dāng)前，一個實參可以是第一類值或者是一個配置：Argument=valueValue+variableLocation(6.92)581.3.1定義性參數(shù)機(jī)制（續(xù)2）詳細(xì)描述形參的效果就是把它的標(biāo)識符綁定到對應(yīng)的實參。因此，一個形參的指稱就是一個如（）所示的、從實參到環(huán)境的函數(shù)；實參(actual-parameter)的指稱產(chǎn)生一個實參(argument)。bind-p:FP→(Argument→Environ) (6.93)give-a:AP→(Environ→Store→Argument) (6.94)<3>語義函數(shù)591.3.1定義性參數(shù)機(jī)制（續(xù)3）形參的語義方程如下所示：bind-p[constI:T](valueval)=bind(I，valueval) (6.95a)bind-p[varI:T](variableloc)=bind(I，variableloc) (6.95b)語義方程十分相似，唯一的區(qū)別是所希望的實參或者是第一類值，或者是一個配置。實參的語義方程如下所示：give-a[E]envsto=value(evalEenvsto) (6.96a)give-a[varI]envsto= (6.96b)letvariableloc=find(env，I)invariableloc如方程（a-b）所示，，定義性參數(shù)機(jī)制具有特別簡單的語義，并且它們之間非常相似。同樣地，過程和函數(shù)參數(shù)也很簡單和相似（這里沒有說明）。<4>語義方程601.3.2拷貝參數(shù)機(jī)制(Copyparametermechanisms)拷貝參數(shù)機(jī)制的特點是對值的拷貝。形參標(biāo)識符指稱過程的一個本地變量。值在進(jìn)入該抽象時被拷貝進(jìn)此變量，并且/或者在返回時拷貝出去?？截悈?shù)機(jī)制的例子如下所示：值參數(shù)（Valueparameters）結(jié)果參數(shù)（Resultparameters）值－結(jié)果參數(shù)（Value-resultparameters）<1>語法（例）FP::=valueId:Type-denoter (6.97a)|resultId:Type-denoter (6.97b)AP::=E (6.98a)|varId (6.98b)規(guī)則(a-b)分別定義了相對于值和結(jié)果形參的實參語法。當(dāng)前，實參可以是如()所示的第一類值或者一個配置。611.3.2拷貝參數(shù)機(jī)制（續(xù)1）<2>指稱實參可以是第一類值或者是一個配置：Argument=valueValue+variableLocation(6.92)<3>語義函數(shù)在過程的入口，一個值參數(shù)被如下處理：分配一個配置并且用實參對它初始化（第一類值），形參標(biāo)識符被綁定到此配置。對結(jié)果參數(shù)的處理類似，但被分配配置的狀態(tài)是未定義。在兩種情況中，存貯均被修改。因此給形參一個指稱，它是一個從實參和存儲到環(huán)境和該存儲的一個函數(shù)：copy-in:FP→(Argument→Store→Environ×Store) (6.99)

621.3.2拷貝參數(shù)機(jī)制（續(xù)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')從過程返回時，值參數(shù)不產(chǎn)生任何影響。但是在結(jié)果參數(shù)的情況下，實參的配置被形參配置中的值所修改。因此需要給形參第二個語義函數(shù)：copy-out:FP→(Environ→Argument→Store→Store) (6.101)

copy-out的語義函數(shù)定義如下：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拷貝參數(shù)機(jī)制（續(xù)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'是調(diào)用時的存貯。處理入口時的參數(shù)（copy-in）產(chǎn)生一個綁定parenv，同時也把存貯改變?yōu)閟to''。執(zhí)行過程體C進(jìn)一步把存貯改變?yōu)閟to'''。處理返回時的參數(shù)（copy-out），可能產(chǎn)生更多的存儲改變，從而完成過程調(diào)用。641.4組合類型（Compositetypes）一個原子變量占據(jù)一個單一配置；用輔助函數(shù)fetch檢查原子變量的值；用輔助函數(shù)update修改原子變量。出于兩個原因，組合類型變量更復(fù)雜一些。其一，組合變量所具有的值自身是組合的，如它們由幾個值的分量組成。其二，組合變量可能被有選擇地修改，通過一個命令修改一個分量，而其它分量不受干擾。下邊討論的存儲模型假設(shè)一個配置是最小的存儲單元。它的內(nèi)容可以被查看或修改；但不假設(shè)所有配置含有相等量的信息(如具有固定字大小的計算機(jī)中)；因此不同配置可以包含真值、整型數(shù)等，甚至組合值；最基本的是配置中的內(nèi)容絕對不能被有選擇地修改。在支持組合變量、但是不允許有選擇修改這種變量的語言中，一個組合變量可以占據(jù)一個單一配置。在這種情況下，組合值和變量的出現(xiàn)對語言的語義影響很小。特別的，賦值命令的語義根本不受影響。651.4組合類型（續(xù)1）假設(shè)擴(kuò)充核心語言IMP（例），使其具有有序?qū)?。每個對有兩個可以是任意類型的分量，稱為字段（fields）。特別地，每個字段自身可以是一個有序?qū)?。有序?qū)χ械淖侄慰梢员华?dú)立選擇。不允許對有序?qū)χ械淖侄螁为?dú)賦值，但是一個有序?qū)Φ闹悼梢员毁x給另一個有序?qū)Γㄔ诶袑⒎潘蓪τ羞x擇修改的限制）。如下程序段說明了我們希望規(guī)定的結(jié)構(gòu)：constz~(true，0);varp:(bool，int);varq:(int，int)...p:=z;q:=(5，sndp+1)常量z支持一個類型為（bool，int）的對。變量p含有一個相同類型的對，變量q含有一個整型數(shù)對。表達(dá)式“sndp”選擇p的第二個字段（同樣“fstp”選擇第一個字段）。一個形如“(...，...)”的表達(dá)式構(gòu)成一個對。上述的兩個賦值命令修改所有對變量（但是，現(xiàn)在禁止有選擇的修改，如“fstq:=5”）。661.4組合類型（續(xù)2）<1>語法（例給出一個簡單的例子，禁止有選擇的修改）E::=... |(E，E)