第5章命令式程序的语义 函数式程序 不含赋值或其它形式的改变变量值的操作 命令式程序 -赋值语句是典型的构造 本章围绕一个叫做Kernel的简单的命令式语 言来讨论语义
第5章 命令式程序的语义 • 函数式程序 –不含赋值或其它形式的改变变量值的操作 • 命令式程序 –赋值语句是典型的构造 • 本章围绕一个叫做Kernel的简单的命令式语 言来讨论语义
5.1引言 ·Kerneli语言的结构由下面的文法概括 P::=x:=MP;P if B then P else P while B do P od -x和M都有适当的类型val -B的类型是boo1 -没有显式的输入、输出，也没有局部变量声明 ·例求对数 x=1;Jy=0; whilex<dox:=x+x;=y+1 od
5.1 引 言 • Kernel语言的结构由下面的文法概括 P ::= x:= M | P ; P | if B then P else P | while B do P od – x和M都有适当的类型val – B的类型是bool – 没有显式的输入、输出，也没有局部变量声明 • 例 求对数 x := 1; y := 0; while x < z do x := x + x; y := y + 1 od
5.1引 言 本章主要内容 围绕Kernel来讨论命令式语言的语义 基于一组重写规则的结构化操作语义 使用类型化入演算和论域(CPO)来表示的指 称语义 把Kernel程序翻译成类型化入演算的表达式 利用类型化入演算的指称语义 基于Floyd-.Hoare逻辑的公理语义
5.1 引 言 本章主要内容 围绕Kernel来讨论命令式语言的语义 • 基于一组重写规则的结构化操作语义 • 使用类型化演算和论域（CPO）来表示的指 称语义 – 把Kernel程序翻译成类型化演算的表达式 – 利用类型化演算的指称语义 • 基于Floyd-Hoare逻辑的公理语义
5.2 Kernel语言 5.2.1存储单元 Kernel的变量可赋值 -与函数式语言let子句引入的变量有很大区别 一可赋值变量指称存储单元 变量的左值和右值 -左值是变量的存储单元的地址 -右值是该存储单元存放的内容 为方便讨论，修改语言 显式区分左值和右值，例x和contx
5.2 Kernel语言 5.2.1 存储单元 • Kernel的变量可赋值 – 与函数式语言let子句引入的变量有很大区别 – 可赋值变量指称存储单元 • 变量的左值和右值 – 左值是变量的存储单元的地址 – 右值是该存储单元存放的内容 • 为方便讨论，修改语言 – 显式区分左值和右值，例x和cont x
5.2 Kerneli语言 ·例1求对数 x=1;y=0; while contx<z do x:=contx+contx;y:=conty+1 od 。例2：计算m除以n的商g和余数r q:=0;r:=n while cont r≥ndo q :cont q+1;r:=contr-n; od
5.2 Kernel语言 • 例1 求对数 x := 1; y :=0; while cont x < z do x := cont x + cont x; y := cont y + 1 od • 例2：计算m除以n的商q和余数r q := 0; r := m; while cont r n do q := cont q +1; r := cont r – n; od
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