(1) 调研，然后总结介绍规格化设计的大致发展历史和为什么得到了人们的重视
-->规格化设计的大致发展历史
二十世纪60年代以前，程序设计使用的主要是机器语言、汇编语言等，由于它们是针对特定型号计算机的语言，在不同计算机之间的可移植性差，而且不同计算机一般具有不同的指令系统，使得这类语言可读性极差。
针对面向对象的方法，人们需要发展Hoare的理论以适应面向对象的特殊性。1957年之后，出现了使用代数公理验证规格的理论。Guttag使用抽象的数据类型来降低设计和实现大型软件的复杂度，用代数公理证明规格的正确性。Goguen和Zilles都着重强调代数化方法，使用代数方法验证抽象数据类型的规格化的正确性。使用抽象数据类型的代数规格法虽然可以描述方法之间的相关关系，但是失去了对单个方法的准确规格定义。
保证程序的正确性以及减少软件错误一直是研究者们关注的问题。1959年，Hoare提出了基于“前置后置条件”的接口规格方法，即若一种方法在执行前满足前置条件，运行后满足后置条件，那么这种条件就是正确的。Hoare提出的这个结论为规格化发展起到了奠基的作用。
二十世纪60年代中后期，软件的数量增多，规模增大，由于缺乏科学规范的系统规划与测试、评估标准，导致大批成本高昂的软件系统由于含有错误无法使用，甚至带来巨大损失。此时人们意识到程序的设计应易于保证正确性，也便于验证正确性，面向过程的程序设计方法开始出现。
80年代初开始，面向对象的程序设计开始出现。将任务抽象为对象以及对象的行为，面向具体的应用功能。对于每个封装的功能模块，只关心它的接口及能实现的功能，即方法的规格抽象。
针对各方法的精确规格定义，1992年，Meyer提出契约式编程延续了对方法的精确定义，但其不足是依赖内部状态来体现方法之间的相互依赖。Robert也引入契约来表达接口的前置条件和后置条件，在调用这个接口时可以用前置和后置条件验证正确性，在调用这个接口时可以用前置条件和后置条件验证正确性。但Robert提出使用带有断言的lambda计算来检测系统运行，这使得断言和程序语句难以区分，影响阅读也影响了程序的运行效率。
Yoonsik也尝试使用模型方法和模型变量来解决上述问题，并建立了规格方法JML，JML不需要直接引用具体的程序状态，而是使用抽象的模型变量来代表内部数据状态，模型方法使用模型变量进行规格，从而避免了实际代码和抽象规格的混乱。但这种方法中的模型变量难以定义，模型变量与实际代码之间的关系也难以界定。
也有研究者使用状态抽象的方法进行类的规格定义。1995年，Hoffman提出了一种状态抽象模块，它提供了一个好的数学模型，并且提高了抽象规格的清晰性和易用性。状态的抽象提高了接口的抽象程度，但是状态的变化使得模块的接口难以定义。堆方法是基于抽象状态方法扩充出来的另一种思路。堆方法是在对象引用和对象状态之间建立映射，堆中可以找到由区域应用的对象的状态，通过在程序中检验对状态，可以验证程序的正确性和完备性。但是堆方法也有缺陷，它定义的对象过多，容易造成空间爆炸。
-->规格化设计得到重视的原因
进行规格抽象，有助于更直观的了解程序功能模块的输入限制、可以实现的功能等等。规格抽象中不关心具体的算法，降低了程序的阅读难度，提高了程序的易读性。从方法规格对模块进行检查，便于保证和验证程序的正确性。规格实际上是程序员应该遵守的“契约”，对于代码的使用者和创作者都有帮助。对于编程人员，他们可以分工合作，根据统一的规格来完成一个程序。从局部来看，针对一个规格抽象的视线与针对其他规格抽象的实现无关，相互之间不会产生影响。当修改一个规格抽象的实现时，不需要对使用该抽象的其他任何规格抽象及其实现进行调整。这样既保证代码的相异性设计又保证了程序的可维护性。而对于程序的使用者，阅读规格，可以迅速了解程序的功能和作用，提高效率。
(2) 按照作业，针对自己所被报告的规格bug以及雷同的规格bug（限于bug树的限制，对手无法上报），列一个表格分析
第九、十、十一次作业没有被报JSF类型的bug。
(3) 分析自己规格bug的产生原因
第九、十、十一次作业没有被报JSF类型的bug。
(4) 分别列举5个前置条件和5个后置条件的不好写法，并给出改进写法
-->前置条件
1、前置条件缺少对参数存在性的判断
//修改前 /** * @REQUIRES: * his.graph != null; * @MODIFIES:None * @EFFECTS: * rackable ==> esult == his.backup.clone(); * ! rackable ==> esult == his.graph.clone(); * @THREAD_REQUIRES: * locked( his); * @THREAD_EFFECTS: * locked(); */ ---------------------------------------------------------------------------------------- //修改后 /** * @REQUIRES: * his.graph != null; * his.backup != null; * @MODIFIES:None * @EFFECTS: * rackable ==> esult == his.backup.clone(); * ! rackable ==> esult == his.graph.clone(); * @THREAD_REQUIRES: * locked( his); * @THREAD_EFFECTS: * locked(); */
2、前置条件没有明确参数范围
//修改前 public synchronized Vector<Integer> SPFA(int src, int dst, int graph[][]) { /** * @REQUIRES: * 0<=src<6400 * 0<=dst<6400 * @MODIFIES:None * @EFFECTS: * 在图是连通图的前提下，找src到dst的最短路径 * esult == path; * @THREAD_REQUIRES: * locked( his); * @THREAD_EFFECTS: * locked(); */ ----------------------------------------------------------------------------------------------------------------------------- //修改后 public synchronized Vector<Integer> SPFA(int src, int dst, int graph[][]) { /** * @REQUIRES: * 0<=src<6400 * 0<=dst<6400 * graph!=null; * graph.size==6400*6400; * @MODIFIES:None * @EFFECTS: * 在图是连通图的前提下，找src到dst的最短路径 * esult == path; * @THREAD_REQUIRES: * locked( his); * @THREAD_EFFECTS: * locked(); */
3、前置条件缺少对数字范围的判断
//修改前 public synchronized boolean setFlow(int src, int dst, int value) { /** * @REQUIRES: * 0<=src<6400; * 0<=dst<6400; * @MODIFIES: * his.flow; * his.snapflow; * @EFFECTS: * 如果start与end邻接,则 * his.flow[src][dst] = value; * his.flow[dst][src] = value; * his.snapflow[src][dst] = value; * his.snapflow[dst][src] = value; * esult = true; * 否则 * esult = false; * @THREAD_REQUIRES: * locked( his); * @THREAD_EFFECTS: * locked(); * */ --------------------------------------------------------------------------- //修改后 public synchronized boolean setFlow(int src, int dst, int value) { /** * @REQUIRES: * 0<=src<6400; * 0<=dst<6400; * 0<=value<=INT_MAX; * @MODIFIES: * his.flow; * his.snapflow; * @EFFECTS: * 如果start与end邻接,则 * his.flow[src][dst] = value; * his.flow[dst][src] = value; * his.snapflow[src][dst] = value; * his.snapflow[dst][src] = value; * esult = true; * 否则 * esult = false; * @THREAD_REQUIRES: * locked( his); * @THREAD_EFFECTS: * locked(); * */
4、前置条件缺少被要求的变量条件
//修改前 public boolean equals(int [] num1, long t) { /** * @REQUIRES:None; * @MODIFIES:None; * @EFFECTS: * esult == ( his.time == t && his.num == num); */ --------------------------------------------------------------------------------------------- //修改后 public boolean equals(int [] num1, long t) { /** * @REQUIRES: * num1!=null; * num1.size==4; * t>=0; * @MODIFIES:None; * @EFFECTS: * esult == ( his.time == t && his.num == num); */
5、前置条件缺少可能会导致异常
//修改前 public boolean parse(String s) { /** * @REQUIRES: * @MODIFIES: * @EFFECTS: * esult == m1.matches() || m2.matches() || m3.matches(); */ Pattern p1 = Pattern.compile("(\[CR,\([+]?\d{1,2},[+]?\d{1,2}\),\([+]?\d{1,2},[+]?\d{1,2}\)\])"); Matcher m1 = p1.matcher(s); Pattern p2 = Pattern.compile("(\[OP,\([+]?\d{1,2},[+]?\d{1,2}\),\([+]?\d{1,2},[+]?\d{1,2}\)\])"); Matcher m2 = p2.matcher(s); Pattern p3 = Pattern.compile("(\[CL,\([+]?\d{1,2},[+]?\d{1,2}\),\([+]?\d{1,2},[+]?\d{1,2}\)\])"); Matcher m3 = p3.matcher(s); return m1.matches() || m2.matches() || m3.matches(); } -------------------------------------------------------------------------------------------------------------- //修改后 public boolean parse(String s) { /** * @REQUIRES: * s!=null; * @MODIFIES: * @EFFECTS: * esult == m1.matches() || m2.matches() || m3.matches(); */ Pattern p1 = Pattern.compile("(\[CR,\([+]?\d{1,2},[+]?\d{1,2}\),\([+]?\d{1,2},[+]?\d{1,2}\)\])"); Matcher m1 = p1.matcher(s); Pattern p2 = Pattern.compile("(\[OP,\([+]?\d{1,2},[+]?\d{1,2}\),\([+]?\d{1,2},[+]?\d{1,2}\)\])"); Matcher m2 = p2.matcher(s); Pattern p3 = Pattern.compile("(\[CL,\([+]?\d{1,2},[+]?\d{1,2}\),\([+]?\d{1,2},[+]?\d{1,2}\)\])"); Matcher m3 = p3.matcher(s); return m1.matches() || m2.matches() || m3.matches(); }
-->后置条件
1、后置条件没有按照规格要求（赋值应该用==）
//修改前 /** * @REQUIRES: * 0<=id<=99; * taxiGUI!=null; * p!=null; * citymap!=null; * trafficlight!=null; * @MODIFIES: * his.id; * his.queue; * his.position; * his.credit; * his.state; * his.cnt; * his.p; * his.taxiGUI; * his.citymap; * his.trafficlight; * @EFFECTS: * his.id == id; * his.position = new Random().nextInt(nodenum); * his.cnt = 0; * his.state = STATE.IDLE * his.credit = 0; * his.queue = new LinkedBlockingQueue<Request>(); * his.taxiGUI == taxiGUI; * his.citymap = citymap; * his.p = p; * his.trafficlight = trafficlight; */ -------------------------------------------------------------------------------------------- //修改后 /** * @REQUIRES: * 0<=id<=99; * taxiGUI!=null; * p!=null; * citymap!=null; * trafficlight!=null; * @MODIFIES: * his.id; * his.queue; * his.position; * his.credit; * his.state; * his.cnt; * his.p; * his.taxiGUI; * his.citymap; * his.trafficlight; * @EFFECTS: * his.id == id; * his.position == new Random().nextInt(nodenum); * his.cnt == 0; * his.state == STATE.IDLE * his.credit == 0; * his.queue == new queue; * his.taxiGUI == taxiGUI; * his.citymap == citymap; * his.p == p; * his.trafficlight == trafficlight; */
2、后置条件写了具体的算法和数据结构
//修改前 /** * @REQUIRES:None; * @MODIFIES: * his.queue; * @EFFECTS: * his.queue = new LinkedBlockingQueue <Request>(); */ ---------------------------------------------------------------------------------------- //修改后 /** * @REQUIRES:None; * @MODIFIES: * his.queue; * @EFFECTS: * his.queue == new queue; */
3、后置条件缺少被改变的变量（很有可能导致逻辑bug）
//修改前 /** * @REQUIRES: * 0<=src<6400; * 0<=dst<6400; * @MODIFIES: * his.flow; * his.snapflow; * @EFFECTS: * 如果start与end邻接,则 * his.flow[src][dst] = value; * his.flow[dst][src] = value; * esult = true; * 否则 * esult = false; * @THREAD_REQUIRES: * locked( his); * @THREAD_EFFECTS: * locked(); * */ ---------------------------------------------------------------------------------------------------- //修改后 /** * @REQUIRES: * 0<=src<6400; * 0<=dst<6400; * @MODIFIES: * his.flow; * his.snapflow; * @EFFECTS: * 如果start与end邻接,则 * his.flow[src][dst] = value; * his.flow[dst][src] = value; * his.snapflow[src][dst] = value; * his.snapflow[dst][src] = value; * esult = true; * 否则 * esult = false; * @THREAD_REQUIRES: * locked( his); * @THREAD_EFFECTS: * locked(); * */
4、后置条件缺省线程安全的effect
//修改前 /** * @REQUIRES: * his.trafficlight != null; * 0 <= n < nodenum; * @MODIFIES: * None; * @EFFECTS: * long[] tra = new long[2]; * ra[0] = gap - (System.currentTimeMillis() - currenttime); * ra[1] = his.trafficlight[n]; * esult = ra; */ -------------------------------------------------------------------------------------- //修改后 /** * @REQUIRES: * his.trafficlight != null; * 0 <= n < nodenum; * @MODIFIES: * None; * @EFFECTS: * long[] tra = new long[2]; * ra[0] = gap - (System.currentTimeMillis() - currenttime); * ra[1] = his.trafficlight[n]; * esult = ra; * @THREAD_REQUIRES: * locked( his); * @THREAD_EFFECTS: * locked(); */
5、后置条件偏自然语言没有严格按照JSF规范写
//修改前 /** * @REQUIRES: * his.log != null && his.logs != null;; * @MODIFIES: * his.log; * his.logs; * @EFFECTS: * his.logs.add(new RequestLog(queue.peek(), this.log)); * his.log = new Vector<Integer>(); * @THREAD_REQUIRES: * locked( his); * @THREAD_EFFECTS: * locked(); */ ----------------------------------------------------------------------------------------------------------------- //修改后 /** * @REQUIRES: * his.log != null && his.logs != null;; * @MODIFIES: * his.log; * his.logs; * @EFFECTS: * ( his.logs.size == old( his.logs).size+1) && ( his.logs.contains(new RequestLog(queue.peek(), this.log))==true); * his.log = new log queue; * @THREAD_REQUIRES: * locked( his); * @THREAD_EFFECTS: * locked(); */
(5) 按照作业分析被报的功能bug与规格bug在方法上的聚集关系
| 方法名 | 功能bug数 | 规格bug数 |
| initGraph() | 1 | 1（但是太过细节没有被测试者发现） |
| checkFile() | 1 | 0 |
| Taxi.run() | 1 | 0 |
| CityMap.run() | 1 | 0 |
功能性bug与规格bug：这三次作业中第十次作业被报了四个功能性bug。有一个笔误bug，跟JSF有关，其余两个是逻辑实现上的bug，和JSF无关。因为是先写代码后写JSF，复制代码时产生的错误被同样复制到了JSF上，但是因为太过细节没有被测试者发现。归根结底还是笔者写代码不够细心。总体来说，功能性bug中与JSF相关的占四分之一。
(6) 归纳自己在设计规格和撰写规格的基本思路和体会
-->设计规格的基本思路和体会
笔者认为设计规格可以充分利用面向对象的思想，设计规格的过程就是架构搭建的过程，这对整个工程的设计实现与后期维护都是很关键的一步。先从类的平衡与分工开始分析，大致确定需要哪些类来完成需求，对每个类所拥有的方法进行进一步分配，分工合理化，并考虑后期可扩展性。确定好类的分工之后，再进一步细化方法，方法内容就可以从JSF的角度进行考虑，因为要想用JSF描述出方法，代码基本上不能超过50行才易描述。在设计的开始写好规格设计对整体代码实现有着很大的益处。
-->撰写规格的基本思路和体会
因为这几次作业设计没有充分先考虑规格，基本上是先写代码后写JSF。所以撰写规格时都是对比实现方法完成了什么，并对比当时写方法时的思路，看看方法完成了什么功能来写JSF的。写规格一定要做到没有二义性，描述要清晰严谨，想好前置条件，尽可能对使用者要求少，在满足前置条件的情况下，后置条件要具有完备性，整体的逻辑要严密。比如要充分考虑为空的边界。