指稱語(yǔ)義簡(jiǎn)介 西安電子

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

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

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

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

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

語(yǔ)法與語(yǔ)義的關(guān)系：語(yǔ)義是依附于語(yǔ)法的；語(yǔ)義是獨(dú)立于語(yǔ)法的，反映語(yǔ)言的真實(shí)含意；語(yǔ)法、語(yǔ)義是多對(duì)多的映射?；仡檶傩晕姆ǎ簩傩裕ㄈ?type、.val等）語(yǔ)義規(guī)則4例1語(yǔ)法與語(yǔ)義的關(guān)系考慮二進(jìn)制數(shù)，如"110"和"10101"。數(shù)字"110"欲表示數(shù)值6，而數(shù)字"10101"欲表示數(shù)值21。

數(shù)字是一個(gè)語(yǔ)法實(shí)體，而數(shù)值是一個(gè)語(yǔ)義實(shí)體。數(shù)值是一個(gè)抽象概念，它不依賴于任何特別的語(yǔ)法表示。數(shù)字"110"：數(shù)值：6、110等數(shù)值6：數(shù)字："110"、"6"、"Ⅵ"、"六"、"陸"等數(shù)值110：數(shù)字："110"、"6E"、"壹佰壹拾"等5例2二進(jìn)制數(shù)的語(yǔ)法與語(yǔ)義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語(yǔ)法：域：語(yǔ)義函數(shù)：語(yǔ)義方程：計(jì)算：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一個(gè)計(jì)算器的語(yǔ)法與語(yǔ)義文法：域：語(yǔ)義函數(shù)：輔助函數(shù)：語(yǔ)義方程：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一個(gè)計(jì)算器的語(yǔ)法與語(yǔ)義（續(xù)）語(yǔ)義方程：計(jì)算：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)先級(jí)高于乘法：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每個(gè)短語(yǔ)p的意義被規(guī)定為一個(gè)在某域中的值d。稱d是短語(yǔ)p的指稱?；蛘哒f(shuō)短語(yǔ)p由d來(lái)指稱；規(guī)定域D作為短語(yǔ)類(lèi)P的指稱，并且引入一個(gè)語(yǔ)義函數(shù)f，它把P中的每個(gè)短語(yǔ)映射到它在D中的域。記為：f:P→D；通過(guò)若干語(yǔ)義方程來(lái)定義語(yǔ)義函數(shù)，每個(gè)函數(shù)對(duì)應(yīng)P中的一個(gè)可區(qū)分的短語(yǔ)。如果P中的一個(gè)短語(yǔ)有子短語(yǔ)Q和R，則相應(yīng)的語(yǔ)義方程式就類(lèi)似如下表示：

f[...Q...R...]=...f'Q...f''R...此處f'和f''分別是Q和R的語(yǔ)義函數(shù)。 ■換句話說(shuō)，每個(gè)短語(yǔ)的指稱（僅）由它們子短語(yǔ)的指稱定義，從而使得整個(gè)程序的意義自下而上得以完整定義。91.2函數(shù)定義的符號(hào)表示使用符號(hào)“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í)際意義。用匿名函數(shù)λn.n+1表示n→n+1，則下述均可表示為匿名函數(shù)：

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

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

Character

－元素來(lái)自字符集合

Integer

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

Natural

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

Truth-Value

－元素是真值false和trueUnit

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

Denomination={dollars,cents}或者：Denomination={元、角、分}等121.3域（Domains）（續(xù)1）a.迪卡爾積域D1×D2×...×Dn的元素是有序n元組，(x1,x2,...,xn)，其中xi∈Di。當(dāng)n=2時(shí)，域中元素是有序?qū)?。b.元組的構(gòu)造與分解 用letx=(...)in...構(gòu)造元組； 用let(...)=xin...分解元組。例2構(gòu)造一個(gè)money類(lèi)型的元組：letpay=(payrate×hours，dollars)in...例3將money類(lèi)型分解為兩個(gè)分量的乘積：

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由三個(gè)獨(dú)立的公式定義141.3域（Domains）（續(xù)3）a.函數(shù)域的元素是函數(shù)或映射。每個(gè)函數(shù)域D→D'的元素是一個(gè)函數(shù)，它把D中的元素映射到D'中的元素。例1

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

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

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

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

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

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

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

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

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

簡(jiǎn)單存儲(chǔ)模型是若干配置（location）的集合，每個(gè)配置有一個(gè)狀態(tài)：①未使用（unused），沒(méi)有被分配給任何變量。②未定義（undefined），已經(jīng)被分配，但是沒(méi)有值。③含有一個(gè)值（storedstorable）。可存儲(chǔ)在配置中的值被稱為可存儲(chǔ)值（storable）。某一時(shí)刻存儲(chǔ)的全體被稱為存儲(chǔ)瞬象（storagesnapshots），用術(shù)語(yǔ)存貯（store）表示。 ■

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

稱配置域?yàn)長(zhǎng)ocation，可存儲(chǔ)域?yàn)镾torable，存貯域?yàn)镾tore。則存儲(chǔ)特性可表示為下述映射：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給出一個(gè)存貯，其中每一個(gè)配置都是未使用。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里的可存儲(chǔ)值，如果loc未定義或者是未使用，給出值fail。

25輔助函數(shù)的符號(hào)表示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)不變）

找到任何一個(gè)“未使用”的配置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因?yàn)榭梢裕篴llocate(deallocate(3?$$，loc2))≠3?$$一個(gè)具有四個(gè)配置loc1，loc2，loc3，loc4（從左到右）的存貯，其中數(shù)字、‘？’和‘＄’分別表示配置的值、未定義和未使用狀態(tài)。271.2存儲(chǔ)模型實(shí)例－無(wú)存儲(chǔ)的計(jì)算器文法：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語(yǔ)義函數(shù)：

execute:Command→int(6.6)

evaluate:E→int(6.7)

valuation:Numeral→Natural(6.8)語(yǔ)義方程：計(jì)算：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存儲(chǔ)模型實(shí)例－有存儲(chǔ)的計(jì)算器將計(jì)算器擴(kuò)充為具有存儲(chǔ)功能，它包括兩個(gè)寄存器（cells）x和y?？梢枣I入如下形式的命令序列：

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

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

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

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

location:R→Location (6.29)

（寄存器的指稱是一個(gè)配置）③語(yǔ)義函數(shù)301.2存儲(chǔ)模型實(shí)例－有存儲(chǔ)的計(jì)算器（續(xù)2）b.表達(dá)式的計(jì)算（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中計(jì)算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中計(jì)算E得到的值int）exec[C1C2]sto= (6.31c)let(sto'，int)=execC1stoinexecC2sto'（在存貯sto中執(zhí)行C1，在改變了的存貯sto'中執(zhí)行C2）③語(yǔ)義方程下一頁(yè)下下頁(yè)311.2存儲(chǔ)模型實(shí)例－有存儲(chǔ)的計(jì)算器（續(xù)3）解：首先在sto中執(zhí)行命令3*37=x，得到一個(gè)值和一個(gè)改變了的sto'，然后在sto'中執(zhí)行命令9+x=，得到一個(gè)值且sto'保持不變。一開(kāi)始，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。用存儲(chǔ)模型給出命令序列3*37=x9+x=（C1C2）的解。321.2存儲(chǔ)模型實(shí)例－有存儲(chǔ)的計(jì)算器（續(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

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

按語(yǔ)法letDinE書(shū)寫(xiě)的表達(dá)式如下：

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

Environ=Identifier→(boundBindable+unbound)(6.37)③letvaln=1in④n+(letvaln=2in7*n)+n同樣，空環(huán)境中計(jì)算表達(dá)式③，建立環(huán)境{n→1}，在此環(huán)境中計(jì)算表達(dá)式④，④中有一個(gè)被嵌套的子表達(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)識(shí)符到實(shí)體的綁定。標(biāo)識(shí)符在一個(gè)作用域中最多有一個(gè)綁定，被綁定的實(shí)體稱為可綁定體。■例3

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

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

若令環(huán)境域?yàn)镋nviron，標(biāo)識(shí)符域?yàn)镮dentifier，可綁定體域?yàn)锽indable，則環(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

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

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

給出一個(gè)組合環(huán)境env和env’綁定的環(huán)境；若任何標(biāo)識(shí)符既被env也被env’綁定，則它在env’的綁定重置在env的綁定。find(env,Id)給出環(huán)境env中Id的可綁定體，若無(wú)就給出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ù)符號(hào)表示與存儲(chǔ)模型對(duì)應(yīng)：empty-store、allocate、update、fetch。問(wèn)題：

deallocate？empty-environ=λId.unbound(6.38)bind(Id，bdble)=()λId'.ifId'=Idthenboundbdbleelseunboudoverlay(env'，env)=(6.40)env'(Id)≠u(mài)nboundthenenv'(Id)elseenv(Id)find(env，Id)=(6.41)letbound-value(boundbdble)=bdblebound-value(unbound)=failinbound-value(env(Id))372.2環(huán)境模型實(shí)例－含有聲明的語(yǔ)言②域：Bindable=Integer (6.44)

③語(yǔ)義函數(shù)：evaluate:E→(Environ→Integer)(6.45)（表達(dá)式的指稱是一個(gè)從環(huán)境到整型數(shù)的映射；）elaborate:D→(Environ→Environ)(6.46)（聲明的指稱是一個(gè)環(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)境模型實(shí)例－含有聲明的語(yǔ)言（續(xù)1）

④語(yǔ)義方程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)計(jì)算env中數(shù)字N組成的表達(dá)式的結(jié)果就是N的值；計(jì)算env中表達(dá)式"E1+E2"的結(jié)果，是在各自env中計(jì)算E1和E2結(jié)果的和；計(jì)算env中引用標(biāo)識(shí)符Id的結(jié)果是Id綁定到env的值；計(jì)算在env中形如"letDinE"表達(dá)式的結(jié)果，是計(jì)算E在一個(gè)新環(huán)境中的結(jié)果。新環(huán)境是由在env中詳細(xì)描述D產(chǎn)生的綁定env'所覆蓋得到的；詳細(xì)描述在env中形如"valId=E"聲明的結(jié)果，是一個(gè)從Id到由計(jì)算env中E得到的值的綁定。392.2環(huán)境模型實(shí)例－含有聲明的語(yǔ)言（續(xù)2）⑤例：空環(huán)境env中計(jì)算：

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'(因?yàn)閑nv={},所以overlay(env',env)=env'={n→1})

402.2環(huán)境模型實(shí)例－含有聲明的語(yǔ)言（續(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)容回顧存儲(chǔ)模型Store=Location→(storedStorable+undefined+unused)(6.16)輔助函數(shù)的符號(hào)表示：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))舉例－帶存儲(chǔ)的計(jì)算器：文法的修改；域、語(yǔ)義函數(shù)、語(yǔ)義方程的設(shè)計(jì)42內(nèi)容回顧（續(xù)）環(huán)境模型Environ=Identifier→(boundBindable+unbound)(6.37)輔助函數(shù)的符號(hào)表示：empty-environ=λId.unbound (6.38)bind(Id，bdble)= ()λId'.ifId'=Idthenboundbdbleelseunboudoverlay(env'，env)= (6.40)env'(Id)≠u(mài)nboundthenenv'(Id)elseenv(Id)find(env，Id)= (6.41)letbound-value(boundbdble)=bdblebound-value(unbound)=failinbound-value(env(Id))環(huán)境強(qiáng)調(diào)作用域，離開(kāi)作用域，綁定自然消失，故沒(méi)有去綁定舉例－含有聲明的語(yǔ)言：文法的修改；域、語(yǔ)義函數(shù)、語(yǔ)義方程的設(shè)計(jì)43習(xí)題1.用帶寄存器的計(jì)算器的指稱語(yǔ)義（假設(shè)寄存器初值均為0）：(a)執(zhí)行命令“x+7=”；(b)執(zhí)行命令“x+7=yy*y=”。2*.拓廣計(jì)算器使得它有一個(gè)大存貯的寄存器，R0，R1，R2等（x和y鍵由單一的R鍵所代替）。3.使用帶聲明表達(dá)式的指稱語(yǔ)義：(a)計(jì)算環(huán)境{m→10，n→15}中的表達(dá)式“m+n”；(b)計(jì)算空環(huán)境中的表達(dá)式“l(fā)etvaln=1inn+(letvaln=2in7*n)+n”。44結(jié)束（2005年5月27日）45本節(jié)主要內(nèi)容抽象函數(shù)抽象過(guò)程抽象參數(shù)組合類(lèi)型失敗了解抽象的種類(lèi)，抽象的數(shù)學(xué)模型；參數(shù)的種類(lèi)，參數(shù)的數(shù)學(xué)模型；組合類(lèi)型的構(gòu)造，組合類(lèi)型的存??；失敗的數(shù)學(xué)模型，失敗的傳播。46一、抽象（Abstractions）

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

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

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

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

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

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