形式方法规格化说明语言Z语言期末试题A卷

第1页(共3页)上海大学2013～2014学年秋季学期试卷课程名：软件规格说明技术课程号：08306042600学分：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.利用定律：pqqp(CS)、qTxpTxqpTx:::(Q7)证明):():(:pTxqTxqpTx2．请写出模式复合的步骤。成绩第2页(共3页)三、（12分，每小题6分）1．完成下述变量声明和谓词表示（1）（1分）使用基本类型写一个整数maxval和minval的声明;（2）（1分）使用基本类型写一个叫做values的整数集合的声明;(3)（2分）写出表示以下叙述的谓词：maxval至少和minval一样大。(4)（2分）写出表示以下叙述的谓词：没有一个values的元素大于maxval或小于minval。2．定义：diagonal=={i:|1i8(i,i)}(1)（3分）使用{Decs|Pred}的形式来写；(2)（3分）使用{DecsExpr}的形式来写。四(18分，每小题6分)1.(6分，分别为4分、1分、1分)使用通用式定义来定义抽象集合X上的关系contains。xcontainsy当且仅当x是一个含有元素y的集合，并写出domcontains与X之间的约束和rancontains与X之间的约束。2．设S是包括1和15在内的从1到15的整数集合，设R是一个类型为S到S的中缀关系：x关联到y当且仅当y大于x的平方并且小于x+1的平方。(1)（3分）使用声明和谓词写出R的定义；(2)（3分）写出表示这个关系的序偶集合。3.请填写如下关于关系的定义域和关系映象的定义(1)（3分）设R和S是两个已经定义的关系：R：XY；S：YZ则它们的复合RS=={x:X；z:Z}（2）（3分）设R是类型为XY的关系，U是类型为X的集合，则R(|U|)=={y:Y}五（8分，每小题4分）1．给定以下函数：f=={a1,b2,c1,e4}g=={b1,c2,d3}(1)（2分）求出fg（2）（2分）求出gf2.以更熟悉的集合表示描述下述函数：(1)（2分）i,j:|i+j=10(i+2,j2)(2)（2分）i:;S:S{i}第3页(共3页)六(12分，每小题6分)完成下列关于序列的运算“”和“rev”的通用式定义。1.(6分，分别为2分、4分)2.(6分，分别为2分、4分)七（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的操作