软件形式化方法作业
（2010年3月～6月）
序号布置日期 提交日期 作业内容
54.27 5.10 在你已经做过的抽象机里选择两个，做它们的数据精化（选有点意思的）。在上交的作业里，对每个规范清晰给出下面几部分内容：
  1. 原机器规范
  2. 精化的想法，解决的问题
  3. 精化后的规范
  4. 精化工作中的证明义务分析
44.13 4.25 练习使用的银行保险柜抽象机文件（课堂实例）

1，基于本次课实例中定义带锁柜子的 抽象机，定义采用其他规则的柜子，例如超市的储物柜或者车站机场的物品存储柜。先设计一套规则，而后再给出规范定义

2，设法为银行保险柜抽象机引进一把主钥匙，只有主钥匙和具体柜子的钥匙都插入后才能开锁。考虑两种设计：

  • 必须锁闭保险柜后主钥匙（和具体钥匙）才能取出（这样，每个时刻只能允许一个顾客打开保险柜）
  • 保险柜打开后主钥匙可以拔出，以允许同时接待多名顾客
3，课堂上给出的银行保险柜没有采用“防御式设计”，最后提供给外部的操作有前条件。请修改抽象机设计，使所有最终的接口操作都采用防御式设计，没有除了类型之外的前条件，并给出操作正常完成与否的信息。
33.23 3.31 1，扩充阅读记录抽象机
  • 考虑一本书有若干拷贝，借出一本就少了一本，因此可能借不到
  • 考虑增加图书和销毁图书
  • 考虑一个小朋友可以同时借2本书
2，扩充马拉松赛记录机
  • 增加查询运动员成绩的操作
  • 增加取消违规的运动员（而不是取消某个位置的运动员）的操作
  • 假定记录机有一个 ``半程记录'' 操作台，记录经过半程的运动员，只有有半程记录的选手才算跑完了马拉松。给机器 RUNNER 加入半程记录功能和相关功能
3，修改完善第一次作业自己做的抽象机。从下周开始每次课用一段时间，讨论 5-6 位同学的抽象机规范。说明包括：1), 所描述系统的非形式考虑；2), 自己定义的抽象机；3), 遇到的问题和分析
23.18 3.24 1，读《工业开发中的形式化方法：成就，问题和未来》一文（网页），写读书报告

2，《B Book》第78页下面方框里的性质，请证明第一条和第五条

3，设计一个公交刷卡器模型。假定公交车有两个刷卡接口，乘客可以在任意接口刷卡，但需要上下车各刷一次。 刷卡器还提供查询和汇总功能。请先写出一个清晰的非形式化需求，而后给出B规范。

13.9 3.17 1，完成一个以座位集合为状态的座位预定抽象机（课堂上给出了一些相关构造）

2，自己找一个软件系统的题目，写出其非形式描述和抽象机定义

下次上课先交流工作的情况

两个抽象机都要在 Atelier B 系统里试验，把 B 规范拷贝到一个 doc 文件里，整理一下代码的格式。并说明在 Ateliel B 里试验的情况：生成了多少证明义务，自动证明了多少。检查一个没有做出的证明（如果有），分析这个证明义务是否正确。考虑（并说明）为什么系统不能证明它