请每位选课同学给课程助理刘海洋发一个邮件，建立联系。
- 9.6: 为下次课预习，建议阅读 A_sld_intro.pdf 幻灯片文件 60 页起
- 9.7: 下次课在 9 月 13 日（周二），需要携带笔记本电脑，并安装好 rodin 系统及两个插件：refactory, animb（可以直接下载配置好的版本）。上次课示例用的 Event-B 工程
1_MAX 已上传至课程材料页面。
- 9.14: 教材新的一章已上传至课程材料页面。本周内请补完上课给出的银行系统的例子（关于 move2 操作与 saving account 的精化），并将结果发到 Abrial 教授邮箱。
- 9.16: 下一次课将以之前内容的小结开始，相关小结的幻灯片
A_sld.car.summary1.pdf 已上传到课程材料页面。2_CAR.zip 是汽车例子的对应 rodin 工程文件。
- 9.20: 本次的作业见课程材料页面 的
exer03.pdf。
注意向 Abrial 教授提交作业时请确保用自己的名字重命名工程文件。有关工程文件的导出与导入，参看这里的说明页面。
- 9.27: 新上传课件：Event-B 文献第三章，压力控制模型的幻灯片、工程文件。
新上传第 4 次作业的幻灯片与工程文件。主要内容是命题逻辑的交互式证明。
新上传课程大作业的计划说明，请大家从给出的 7 个题目中选择一个，或者自选题目。自选题目的同学，可在假期书写自己的大作业计划，并提交 Abrial 教授审阅。
|