一、规格化设计的发展历史
20世纪60年代，软件出现严重危机，Dijkstra提出了goto语句的危害，由此引发了软件界长达数年的论战，并产生了结构化程序设计方法。Pascal语言在20世纪70年代占有统治地位。
随着计算机技术的发展，结构化设计语言和结构化分析无法满足用户的需求，OOP由此应运而生，即面向对象的程序设计。OOP的诞生是程序设计方法学的一场革命，大大提高了开发效率，减少了软件开发的复杂性，提高了软件的可维护性，可拓展性。1990年以来，面向对象分析、测试、度量和管理研究都得到长足发展。
规格化设计伴随OOP而生，为了提高程序的规范性，对类、方法等进行规范化设计，有利于程序的模块化划分。这样设计程序的数据更加安全可控，测试也变得容易，软件的维护性得到提高，因而受到程序设计人员的重视。
二、规格bug表格及原因分析
三、前置条件后置条件写法改进
前置条件不好的写法1
对前置条件不做要求，自己在程序其他部分进行限制来保证一些隐含的前置条件会被满足。其实这样不是很好，降低了方法的通用性，如果都是自己写的代码还好说，在遇到继承，或者作为借口时，往往会出现意想不到的问题。最好将前置条件写明，来增强代码的可读性与可复用性。
前置条件不好的写法2
本身这个前置条件问题不大，但是credit既然作为int类型，最好设定好上界2^32-1。即使不是int类型，一些参数最好也设定合理的界限。
前置条件不好的写法3
隐含了(x1,y1），（x2,y2）这两个点必须相邻的要求。这样会导致不处理错误的数据，作为规格并不全面。需要补全相应的约束。不完全的前置条件，给设计者和方法使用者都会带来困扰
前置条件不好的写法4
只对一个参数进行了前置条件的要求，应该加上对usedgraph的约束，至少保证usedgraph!=null。
前置条件不好的写法5
对于方法内的的变量进行约束是不行的，规格与实现无关。应该去掉distance!=0
后置条件不好的写法1
单纯的通过自然语言来描述后置条件，这样并不如逻辑语言清晰。
改为EFFECTS： esult = max_credit() [min_distance()];
后置条件不好的写法2
直接将算法写到了EFFECTS。后置条件应该描述结果而不是实现过程，实现过程应该由程序员自己决定。
后置条件不好的写法3
代码中存在IO操作在后置条件中却没有写明。IO操作本身也应该是属于后置条件的范畴，应该在后置条件中加入
后置条件不好的写法4
该方法使用了锁机制来保证方法的线程安全性，后置条件应该说明要锁住哪些对象。
@THREAD_EFFECTS :locked (cnt);
后置条件不好的写法5
途中MAXNUM是方法内定义的变量，不应该在后置条件中使用。方法内的变量属于如何实现的范畴，与规格无关。
四、功能bug与规格bug关系分析
总体来说，我个人的功能bug和规格bug聚合度不高。功能bug有两个是没有注意在issue中的补充要求。还有是自己对流量计算方法的错误以及调用迭代器时出错。
五、设计规格撰写规格时的体会
在第九次作业中，由于之前已经完成了程序的大部分设计，因此工作时给已实现了的方法加上JSF。添加JSF时，我发现
（1）自己某些方法功能过多，导致JSF不好描述
（2）方法与方法之间的依赖度过高
后面的作业中，在实现新的功能需要添加新类、方法时，我会先完成Overview和规格的设计，再去进行实现。这样的设计流程，虽然在功能上差别不大，但是程序的安全性（可控制）与可拓展性有了显著的提升。撰写规格时，我主要的考虑顺序是：
（1）需要实现什么功能（EFFECTS）
（2）方法的线程安全性
（3）实现功能需要提供哪些参数（REQUIRES）
（4）在实现过程中改变的什么数据（MODIFIES）