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