6、?ndoq:=contq+1;r:=contr–n;od5.2Kernel語言5.2.2表達(dá)式的解釋在文法中，M和B分別代表val和bool表達(dá)式P::=x:=M
7、P;P
8、ifBthenPelseP
9、whileBdoPod不深入表達(dá)式的內(nèi)部細(xì)節(jié)為方便起見，把val看作nat允許普通的數(shù)值和布爾運(yùn)算5.2Kernel語言用4類別代數(shù)A來建立Kernel的抽象機(jī)器模型作為介紹操作語義和指稱語義的共同基礎(chǔ)便于比較操作語義和指稱語義本小節(jié)先介紹相應(yīng)代數(shù)規(guī)范的三個(gè)類別基調(diào)?包含3類別val、bool和loc僅關(guān)心loc類別有一個(gè)取存儲(chǔ)單元內(nèi)容的函數(shù)符號(hào)cont:loc?val環(huán)
10、境?把變量從?loc??val??bool映射到A的元素?loc：程序中的變量；?val和?bool：程序中的常量Abool的解釋是布爾值集合{true,false}5.2Kernel語言5.2.3程序狀態(tài)操作語義和指稱語義都涉及“狀態(tài)”數(shù)據(jù)結(jié)構(gòu)名字存儲(chǔ)單元狀態(tài)值環(huán)境從名字到值的兩步映射5.2Kernel語言基調(diào)?的第4個(gè)類別stateinit:stateupdate:state?loc?val?statelookup:state?loc?val代數(shù)公理lookup(updatesl?v)l=(lookup)ifEq?ll?thenvelse(lookupsl)upd
11、atesl(lookupsl)=s(update)1update(updateslu)l?v=ifEq?ll?(update)2thenupdateslvelseupdate(updatesl?v)lu5.2Kernel語言四類別代數(shù)AAloc是任意的可數(shù)集合，Astate是從Aloc到Aval的所有函數(shù)的集合initA是任意的常函數(shù)lookupA(s,l)=s(l)updateA(s,l,v)是函數(shù)s?，除了s?(l)=v以外，s?等同于s為了記號(hào)上的方便，下面用init，lookup和update代替initA，lookupA和updateA5.2Kernel語言
12、兩個(gè)問題為什么不在前三個(gè)類別的基礎(chǔ)上引入作為狀態(tài)的函數(shù)state=loc?val，而要引入第4個(gè)類別state若那樣，則lookup和update成了高階的函數(shù)符號(hào)為什么不用一個(gè)函數(shù)直接從變量映射到值，而要分離出環(huán)境和狀態(tài)直觀上講，環(huán)境和狀態(tài)在概念上有區(qū)別，它們分別對(duì)應(yīng)到實(shí)際語言實(shí)現(xiàn)的不同機(jī)制從技術(shù)角度說，Kernel沒有提供聲明常量的值的方式，只能將程序中常量的取值交給環(huán)境來確定5.3操作語義5.3.1表達(dá)式的求值操作語義分成兩部分表達(dá)式的計(jì)算語句的執(zhí)行表達(dá)式的語義表達(dá)式、環(huán)境、狀態(tài)和表達(dá)式的語義值之間的一個(gè)四元關(guān)系：?M,s???evalv環(huán)境下標(biāo)在下面將省略?e
13、val由一個(gè)證明系統(tǒng)來給出5.3操作語義?eval公理?x,s??eval?(x)?c,s??evalcA?eval推理規(guī)則fA(v1,…,vk)=vlookupA(s,l)=v?M1,s??evalv1…?Mk,s??evalvk?fM1…Mk,s??evalv?x,s??evall?contx,s??evalv5.3操作語義5.3.2命令的執(zhí)行命令的執(zhí)行可以用關(guān)系?exec來刻畫updateA(s,?(x),v)=s??M,s??evalv?x:=M,s??execs??P1,s??execs??P2,s???execs???P1;P2,s??e
