1Cd_start=2按任意键Cd_start=3得分榜游戏结束开始储存中读取游戏游戏进行中图4.1游戏状态转换图D,应该有形式化的方法顾问随时提供咨询;E,不应该放弃传统的开发方式;F,应该建立详尽的文档;G,不应该放弃质量标准;H,不应该盲目依赖形式化方法;I,应该测试,测试再测试;J,应该重用。3,一个浮点二进制数的构成是:一个可选的符号(+或-),后跟一个或多个二进制位,再跟上一个字符E,再加上另一个可选符号(+或-)及一个或多个二进制位。例如,下列的字符串都是浮点二进制数:110101E-101-100111E11101+1E0更形式化地,浮点二进制数定义如下:〈floatingpointbinary〉∷=[〈sign〉]〈bitstring〉E[〈sign〉]〈bitstring〉〈sign〉∷=+|-〈bitstring〉∷=〈bit〉[〈bitstring〉]〈bit〉∷=0|1其中,符号∷=表示定义为;符号[...]表示可选项;符号a|b表示a或b。假设有这样一个有穷状态机:以一串字符为输入,判断字符串中是否含有合法的浮点二进制数。试对这个有穷状态机进行规格说明。4,考虑下述的自动化图书馆流通系统:每本书都有一个条形码,每个人都有一个带条形码的卡片。但一个借阅人想借一本书时,图书管理员扫描书上的条形码和借阅人卡片的条形码,然后在计算机终端上输入C;当归还一本书时,图书管理员将再次扫描,并输入R。图书管理员可以把一些书加到(+)图书集合中,也可以删除(—)它们。借阅人可以再终端上查找到某个作者所有的书(输入“A=”和作者名字),或具有指定标题的所有书籍(输入“T=”和标题),或属于特定主题范围内的所有图书(输入“S=”加主题范围)。最后,如果借阅人想借的书已被别人借走,图书管理员将给这本书设置一个预约,以便书归还时把书留给预约的借阅人(输入“H=”加书号)。
全文预览
