第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