Z语言形式方法规格说明语言-期末试卷

第1页(共3页)上海大学2016～2017学年秋季学期试卷课程名：软件规格说明技术课程号：08306042学分：3应试人声明：我保证遵守《上海大学学生手册》中的《上海大学考场规则》，如有考试违纪、作弊行为，愿意接受《上海大学学生考试违纪、作弊行为界定及处分规定》的纪律处分。应试人应试人学号应试人所在院系题号一二三四五六七得分一、（20分，每个选项2分）从供选择的答案中选出应填入下列叙述中处的正确答案，把编号写在每小题下提供的“答案”处。1.形式方法基于数学方法来描述目标软件系统。它描述了A。形式方法一般需要形式规格说明语言的支持。形式规格说明语言用于描述B。抽象是一种很重要的技术，软件规格说明有两种抽象：C。Z语言是一种基于一阶谓词逻辑和集合论的D。设一个命题公式G含有n个命题变元，则对这n个命题变元的一组真值赋值称为G的一个解释，公式G有E个解释。供选择的答案：A：①由什么人开发软件②怎么做软件③软件做什么④为什么要开发软件B：①程序代码②用户需求③测试文档④数据结构C：①过程抽象和数据抽象②图形抽象和数据抽象③过程抽象和逻辑抽象④图形抽象和逻辑抽象D：①程序模块语言②形式语言③规格说明语言④形式规格说明语言E:①2n②n③2n④2n2答案：A:B:C:D:E:2.设Q是一个集合，由Q的所有子集所组成的集合，称为集合Q的幂集，记作Q。如果WQ，则有A。设有X和Y两个集合，则X和Y的笛卡尔积XY是B。关系可关联定义域中的一个元素到值域中的多个元素，又可关联定义域中的多个元素到值域中的一个元素，是一个多对多的映射。一个X和Y上的关系是X和Y笛卡尔积的C。函数是一种特殊的关系，一个函数映射了定义域中的每一个元素到值域中D。在Z中，序列是一种类型。在一个序列中，E。供选择的答案：A：①W=Q②WQ③QW④WQB：①X和Y的所有关系组成的集合②X和Y的子集组成的集合③X和Y所有元素组成的序偶集合④X和Y的并集C：①空集②幂集③子集④子序列D：①最多一个元素②至少一个元素③任意多个元素④至少两个元素E:①元素出现的次序不重要②每个元素只出现一次③元素的出现有次序，又可出现多次④每个元素出现的次数也不重要答案：A:B:C:D:E:二（10分，每小题5分）1.利用-elim和-int定律：证明pqpq2．请写出模式A和B的模式复合AB的过程。成绩第2页(共3页)三、（16分）1．请完成下述变量声明和谓词表示(1)（2分）使用基本类型写一个整数maxval和minval的声明；(2)（2分）使用基本类型写一个叫做values的整数集合的声明；(3)（2分）写出表示以下叙述的谓词：maxval至少和minval一样大；(4)（2分）写出表示以下叙述的谓词：没有一个values的元素大于maxval或小于minval2．使用扩充表示法描述如下集合表达式，尽可能简单。（1）(2分)一个集合S中的不同元素的序偶的集合。（2）(3分)国际象棋棋盘上的另一条对角线。（3）(3分)集合中每一个元素乘以3所组成的集合。四、(10分)1．(4分)给出集合关系的符号的通用式定义。要求表示的是：如果S是T的一个子集，那么S中的任何一个元素也是T中的一个元素，但至少存在一个元素，该元素不是S中的一个元素，但是T中的一个元素。2.完成如下和关系与函数相关的形式定义：(1)(3分)对任何类型为XY的关系R，设S是定义域类型X的一个集合，则SR=={x：X；y：YABxy}解答A：B:(2)(3分)对任何集合X和Y，X到Y的部分函数是唯一地映射定义域中的元素到值域中元素的所有关系。XY=={R：A(x:X;y,z:Y(xy)R(xz)RB)}解答A：B:五、（12分）1．给定以下函数：f=={a1,b2,c1,e4}g=={b1,c2,d3}(1)（3分）求出fg（2）（3分）求出gf2.(6分，每小题3分)以更熟悉的集合表示描述下述函数：(1)（3分）i,j:ℕi+j(2)（3分）i:ℕ;S:ℙℕ|iSS{i}六、（12分，每个填空项2分）1.给定如下关于序列操作head和tail的不完整的定义，请写出应填入空缺处的合适的表示，使它们成为完整的定义。第3页(共3页)给定如下关于包操作⊎和⊌函数的不完整的定义，请写出应填入空缺处的合适的表示，使它们成为完整的定义。七、(20分)考虑操作系统中一个可由用户访问的自由存储块的管理程序。设用户的集合为U,系统中有n个连续的编了号的存储块,系统中的所有自由存储块的集合以B来表示，n和B为全程变量。存储管理程序中含有一个目录，它记录了哪个用户使用着哪些存储块。可称这个目录结构为dir,并希望它有如下性质。每一个块只能由一个用户占用一个用户可以占用多个存储块某些块可能还未被占用某些用户没有占用任何块可将dir表示为一个B到U的函数，并以它来形式地描述上述性质。请完成如下工作：1.(2分)给出类型U的定义;2.(3分)以公理描述来定义全程变量B;3.(7分，分别为3分、2分、2分)写出状态模式SM,SM和SM;4.(8分)用操作模式定义完整的“请求分配一个存储块”Request的操作。