5.2 Kerneli语言 5.2.2表达式的解释 在文法中，M和B分别代表val和bool表达式 P::=x:=M P;P if B then P else P while B do P od 不深入表达式的内部细节 -为方便起见，把val看作nat 一允许普通的数值和布尔运算
5.2 Kernel语言 5.2.2 表达式的解释 • 在文法中，M和B分别代表val和bool表达式 P ::= x := M | P ; P | if B then P else P | while B do P od • 不深入表达式的内部细节 – 为方便起见，把val看作nat – 允许普通的数值和布尔运算
5.2 Kerneli语言 ,用4类别代数A来建立Kernel的抽象机器模型 作为介绍操作语义和指称语义的共同基础 一便于比较操作语义和指称语义 本小节先介绍相应代数规范的三个类别 基调Σ包含3类别val、bool和loC -仅关心0c类别有一个取存储单元内容的函数符号 cont:loc→val 环境n把变量从Ttoe UTval Tbool映射到A的元素 Toc:程序中的变量；Tva和Tbool:程序中的常量 -Abool的解释是布尔值集合{true,false
5.2 Kernel语言 • 用4类别代数A来建立Kernel的抽象机器模型 – 作为介绍操作语义和指称语义的共同基础 – 便于比较操作语义和指称语义 • 本小节先介绍相应代数规范的三个类别 – 基调包含3类别val、bool和loc – 仅关心loc类别有一个取存储单元内容的函数符号 cont : loc → val – 环境把变量从 loc val bool映射到A的元素 loc：程序中的变量； val和bool ：程序中的常量 – Abool的解释是布尔值集合{true, false}
5.2 Kerneli语言 5.2.3程序状态 操作语义和指称语义都涉及“状态”数据结 构 环境 状态 名字 存储单元 值 从名字到值的两步映射
5.2 Kernel语言 5.2.3 程序状态 • 操作语义和指称语义都涉及“状态”数据结 构 名字 存储单元 状态 值 环境 从名字到值的两步映射
5.2 Kerneli语言 基调Σ的第4个类别state init state update state x loc x val -state lookup state x loc -val 代数公理 lookup (update s I v)1 (lookup) if Eg?II then y else (lookup s l) update s l (lookup s I)s (update) update (update s l u)I y if Eg?IP (update)2 then update s l v else update (update s l'v)l u
5.2 Kernel语言 基调的第4个类别state init : state update : state loc val → state lookup : state loc → val 代数公理 lookup (update s l v) l = (lookup) if Eq? l l then v else (lookup s l) update s l (lookup s l) = s (update)1 update (update s l u) l v = if Eq? l l (update)2 then update s l v else update (update s l v) l u
5.2 Kerneli语言 ·四类别代数A Aloc是任意的可数集合，sae是从Aoc到Aml的所 有函数的集合 ini是任意的常函数 lookupA(s,1)s(I) - updater(s,l,y)是函数s',除了sU=v以外，s'等同 于s - 为了记号上的方便，下面用init,lookup和update 代替iniA,lookupAi和updater
5.2 Kernel语言 • 四类别代数A – Aloc是任意的可数集合，Astate是从Aloc到Aval的所 有函数的集合 – initA是任意的常函数 – lookupA(s, l) = s(l) – updateA(s, l, v)是函数s ，除了s(l) = v以外，s等同 于s – 为了记号上的方便，下面用init，lookup和update 代替initA ，lookupA和updateA