Z语言规格说明实例-操作系统例子.pptxVIP

规格说明实例 目录 简介 操作系统存储管理实例 系统状态描述 请求分配操作 释放操作 请求分配连续存储块 一、简介 Z是一个规格说明的语言，或者说是一种表示方法。 在Z的表示中，有两种互补的语言： 模式语言：公理定义、模式、通用模式等 数学语言：一阶逻辑、集合论、类型、关系、函数、序列和包 简介（续） 模式语言能把一个规格说明中的共同部分抽取出来，并把类似的结构间的差别表示出来。 而数学语言描述能力足够强大，但是数学表示的枯燥会使可读性大大降低。 为此，引入一种模式结构来描述规格说明。 二、存储分配管理 2.1系统状态描述 在操作系统中，存储块分配管理程序有两个功能：分配和释放存储块。 设存储块的集合为B，它含有n个连续的自然数来标记的块，其公理定义如下： 存储分配管理 用户集合是U，它是一个给定类型。声明如下：[U]. 目录dir：记录哪个用户使用哪些存储块。 性质： 一个块只能由一个用户占用 一个用户可以占用多个块 某些块可能没有占用 某些用户没有占用任何块 存储分配管理 dir可以定义为一个B到U的函数， dir是一个函数符 dir不必是一个入射函数（一对一） dir可以是一个部分函数 dir不必是一个满射函数 dir：B—U 存储分配管理 空闲块定义： free：P B 也可以说明为： free=B\(dom dir) 把它看成是状态不变式的一部分，总为真 加上dir和free构成模式SM： 存储分配管理 存储分配管理 初始状态模式： 必须保证这样的一个状态存在，可以检查： free’=B=B\{}=B\{dom dir’} 存储分配管理 2.2请求分配空闲块 输入用户：u？ 输出:存储块b！和回答r！ 定义回答Report为枚举类型： Report::=‘OK’|’Fail’|’BlockFree’|’NotOwner’ 存储分配管理 操作前需要满足： free≠{}和b! ∈free 操作后需要满足: free’=free\{b!}和dir’=dirU{b! u?} 存储分配管理 命名模式Request0描述该操作: 存储分配管理 为了肯定该操作可行,计算其前置条件模式PreReque0: 存储分配管理 由于存在错误情况,定义模式Request0Err: 那么完整的请求分配操作可以定义为: Request0 Request0Err 存储分配管理 2.3释放存储块 输入:用户名u?和占有的b? 输出:r! 操作前满足:(b? u?) dir 操作后满足：free’=freeU{b?} dir’={b?} dir 存储分配管理 以Release0描述该操作: 对应前置条件模式: 存储分配管理 出错情况: (1)要释放的块已经是空闲块 (2)释放的块被其他用户占有 分别由RelFreeErr和RelOwnerErr模式描述： 存储分配管理 与之对应的前置条件模式： 释放存储块的完整操作应该是： Release0 RelFreeErr RelOwnerErr 存储分配管理 2.4请求分配连续存储块 连续的特性描述：如果l和h分别是一个数的集合S中最小数和最大数，并且l和h之间的每一个数都在S中，则称S是连续相邻的。可以描述为： 由于要求S是一个由中缀关系所确定的函数（_.._）所构造的集合，可以简明定义为： 存储分配管理 输入：用户u?和请求分配块数n? 输出：存储块集合b！ 满足条件：#b！=n？ b！ ran(_.._) b! free dir’=dirU(b! ×{u?}) free’=free\b! 存储分配管理 模式ReqStore来描述该操作： 存储分配管理 分配策略（首次适应法） 满足所请求的n个连续的相邻块的集合起始点位置所组成的集合S可以定义为： 首次适应法策略选择相邻块是以S中最小的值为起始位置，并且连续的n个块。 b! = (min S) .. (min S) + n?-1 存储分配管理 使用模式FirstFir来描述： 最后使用ReqStore0和FirstFit的合取来表示首次适应法分配策略。 谢谢大家！