1.规则化发展历史
形式化方法的研究高潮始于20世纪60年代后期，针对当时所谓“软件危机”,人们提出种种解决方法,归纳起来有两类：一是采用工程方法来组织、管理软件的开发过程；二是深入探讨程 序和程序开发过程的规律，建立严密的理论，以其用来指导软件开发实践。前者导致“软件工程”的出现和发展，后者则推动了形式化方法的深入研究。经过30多 年的研究和应用，如今人们在形式化方法这一领域取得了大量、重要的成果，从早期最简单的形式化方法一阶谓词演算方法到现在的应用于不同领域、不同阶段的基于逻辑、状态机、网络、进程代数、代数等众多形式化方法。形式化方法的发展趋势逐渐融入软件开发过程的各个阶段,从需求分析、功能描述(规约)、(体系结构/算法)设计、编程、测试直至维护。
2.规格bug
| 作业次数 | 规格bug数 | 名称 | 雷同bug |
| 9 | 6 | Modified不完整/Effect不完整/jsf不规范 | 3 |
| 10 | 0 | / | 0 |
| 11 | 0 | / | 0 |
3.产生bug的原因
对于规格问题，个人认为理解上存在着因人而异的细微差别，少数的bug个人认为并非不符合规格，但也确实存在不规格的书写，其中对Modified的理解不全面，并未对方法的影响完全描述。
4.关于五个不好的前置条件和后置条件
看了看别人的博客和被调出的bug，尽量找了自己的毛病（挠头.jpg）
前置条件：
1.不要忽略run方法的前置条件
2.对于对象数组, 应判断数组中每个对象也不为空 @REQUIRES: (arr != null) && (\all i in arr; i != null)
3.有的条件用分号隔离了，换用&&或|| 更明确
4.对于对象s属于数组arr，不应使用"s∈arr"。替换为“arr.contains(s)==true”
5.从数组arr中删除对象s，应使用"arr.contains(s)!=true && arr.size() == .old(arr.size()) - 1"
后置条件:
1.应用“==”代替“=”
2.尽量不用自然语言书写
3.后置条件描述不完善
5.功能bug以及规格bug在方法上的聚类问题
关于规格bug，在于Modified方面对于方法的效果理解不完整而省略导致。功能bug只是在于第10作业中文件输出时，未修改（与第九次作业不同的租车道路行驶时间今间隔不同）时间间隔。
6.规格撰写的基本思路和体验
由于是递进式的作业，我们被要求在之前完成的作业方法的基础上书写规格。于是体会到了老师上课所说的规格设计应该提前与方法的具体书写。在规格的设计中我发现了我一些方法的内聚问题，也明白了在书写方法前对方法规格设计的意义：有利于对方法更加精炼的设计。
原文地址：https://www.cnblogs.com/a-cloud---/p/9111594.html