1. 举例说明形式化说明技术和欠形式化方法的优缺点。

以下是简单总结，具体看这里

举例说明就先past拉，要不学学课本电梯的例子。

2. 在什么情况下应该使用形式化说明技术？使用形式化说明技术应遵守哪些规则？

1. 在使用非形式化的说明方式存在矛盾，二义性，含糊性，不完整性和抽象层次混乱等问题的时候，就需要采用形式化说明技术。
2. 应该遵守的规则(10个，表形本问传，档质赖测重）

• 应该选用适当的表示方法。
• 应该形式化，但不要过分形式化（中庸形式化）。
• 应该估算成本。
• 应该有形式化方法顾问随时提供咨询。
• 不应该放弃传统的开发方法（不放弃传统）。
• 应该建立详尽的文档。
• 不应该放弃质量标准（不放弃质量标准）。
• 不应该盲目依赖形式化方法（不盲目依赖）。
• 应该测试、测试再测试。
• 应该重用。

3.假设有这样一个有穷状态机：以一串字符为输入，判断字符串中是否含有合法的浮点二进制数。试对这个有穷状态机进行规格说明。

有穷状态机

4 试用有穷状态机说明上述的图书流通系统

考虑下述的自动化图书馆流通系统：每本书都有一个条形码，每个人都有一个带条形码的卡片。但一个借阅人想借一本书时，图书管理员扫描书上的条形码和借阅人卡片的条形码，然后在计算机终端上输入 C；当归还一本书时，图书管理员将再次扫描，并输入 R。图书管理员可以把一些书加到（ +）图书集合中，也可以删除（—）它们。借阅人可以再终端上查找到某个作者所有的书（输入“ A=”和作者名字） ，或具有指定标题的所有书籍（输入“ T= ”和标题），或属于特定主题范围内的所有图书（输入“ S=”加主题范围） 。最后，如果借阅人想借的书已被别人借走，图书管理员将给这本书设置一个预约，以便书归还时把书留给预约的借阅人（输入“ H=”加书号）。

4.1 图书状态的有穷状态机描述

状态机J：{ 书在图书馆 S1，书被借出 S2，书被预约 S3}
输入集K ：{ 书上条形码，借阅卡条形码，终端输入各种命令 }
初始态S：{ 书在图书馆 S1，书被借出 S2}
终态集F：{ 书被借出 S2，书被预约 S3}
转换函数T：

4.2 图书馆终端管理员模式的有穷状态机描述

状态机J：{ 管理员设置状态，书入库，书出库（删除） ，预约 }
输入集K ：{ 终端输入管理员命令，书的各种状态（ S1，S2，S3}
初始态S：{ 管理员设置状态 }
终态集F：{ 书入库，书出库（删除） ，预约， }
转换函数T：如图 4.4.2 所示

4.3 图书馆终端用户模式的有穷状态机描述

状态机J：{ 读者查询状态，查询结果 }
输入集K ：{ 终端输入用户查询命令，书的各种状态（ S1，S2，S3）}
转换函数T：如图 4.4.3 所示
初始态S：{ 读者查询状态 }
终态集F：{ 查询结果 }

5 试用 Petri 网说明第四题所述图书馆中一本书的循环过程，在规格说明中应该包括操作 H、C及 R。

Petri网特别是禁止线要看一下

其中 P1表示书在图书馆；P2表示书在读者手上； P3书被预约

上图解读：
只有P3没有权标，也就是没有预约，P1到P2的转换才被允许。