标签：针对 list IV 出错 应用 出租车 也有 作业 思路
一、规格化设计发展历史
软件规格化方法，最早可追溯到20世纪50年代后期对于程序设计语言编译技术的研究，当时出现了各种语法分析程序自动生成器以及语法制导的编译方法，使编译系统的开发从“手工艺制作方式”发展成具有牢固理论基础的系统方法。规格化设计的研究高潮始于20世纪60年代后期，针对当时所谓的“软件危机”，人们提出种种解决方法，如采用工程方法来组织、管理开发过程和通过钻研规律建立严密的理论以指导开发实践。
经过30多年的研究和应用，如今人们在规格化设计取得了大量、重要的成果，从早期最简单的一阶谓词演算到现在应用于不同领域、不同阶段的基于逻辑、状态机、网络、进程、代数等众多规格形式化方法，它的发展趋势是逐渐融入设计开发的各个阶段，从需求分析、功能描述、算法设计、编程、测试直到维护。
规格化设计对代码的创作者和使用者都有重要的作用。对于编程者，规范的设计有助于架构的建立和调整，有助于完善修正细节，有助于未来的维护和扩展；对于使用者，规格化的呈现有助于理解剖析，避免不必要的误解和分歧，同时也利于高效的阅读和学习。
二、bug分析
三次作业总共被报了四个规格bug，很遗憾的是其中有三个都是“忘记写了”……emm反思一下第十次可能和赶时间有关，但是第十一次在时间蛮充裕的情况下就真的是粗心没检查的锅。另外一个关于repOK的bug，我觉得测试者说的很有道理。因为在原来的repOK方法中，只要出现了对象型的变量我一律用“！=null”来处理，但是想想每个对象的类中也有它自己的repOK，理应传承下来，只有满足了所有的repOK才能说明科学合理性。
虽然从表格上看，功能bug与规格bug确实没有重合的地方，但是这并不意味着两者就毫无关联。两次作业中功能出现的问题集中在input、run、randomdrive这些代码规模较大，逻辑较复杂的方法中，本身规格就很难概括，只能借助自然语言的帮助，加上关键步骤的布尔表达式来描述。由于规格无法涵盖细小逻辑，很难体现出错误疏漏，或者换一种说法，书写规格没有起到应有的作用，所以从报告bug的角度，就看不出联系了。
三、规格改进示例
/** * @REQUIRES: * 0<=index<=6399; * @MODIFIES:None; * @EFFECTS: * normal_behavior: * !(\exist int next;map.reachlist[index].contains(next)) ==> \result==index; * 在index的可达节点中随机选取一个两点之间边流量最小的节点next. * \result==next; * exception_behavior(Exception e): * \result==index; */
↓
/** * @REQUIRES: * 0<=index<=6399; * 0<=oldindex<=6399; * @MODIFIES:None; * @EFFECTS: * normal_behavior: * !(\exist int next;map.reachlist[index].contains(next)) ==> \result==index; * 在index的可达节点中随机选取一个两点之间边流量最小的节点next. * \result==next; * exception_behavior(Exception e): * \result==index; */
······································································································································
/** * @REQUIRES: * 0<=start<=6399; * 0<=end<=6399; * 0<=flow<=100; * @MODIFIES: * \this.flow; * @EFFECTS: * \this.flow[start][end]==flow; * \this.flow[end][start]==flow; */
↓
/** * @REQUIRES: * 0<=start<=6399; * 0<=end<=6399; * distance from start to end is 1. * 0<=flow<=100; * @MODIFIES: * \this.flow; * @EFFECTS: * \this.flow[start][end]==flow; * \this.flow[end][start]==flow; */
······································································································································
/** * @REQUIRES: * 0<=index<=6399; * 0<=next<\this.reachlist[index].size(); * @MODIFIES:None; * @EFFECTS: * type==0 ==> \result==\this.reachlist[index].get(next); * type==1 ==> \result==\this.initreachlist[index].get(next); */
↓
/** * @REQUIRES: * 0<=index<=6399; * 0<=next<\this.reachlist[index].size(); * type==0 || type==1; * @MODIFIES:None; * @EFFECTS: * type==0 ==> \result==\this.reachlist[index].get(next); * type==1 ==> \result==\this.initreachlist[index].get(next); */
······································································································································
/** * @REQUIRES:None; * @MODIFIES:None; * @EFFECTS: * (r‘s time,start_x,start_y,end_x,end_y are equal to this‘s) ==> \result==true; * !(r‘s time,start_x,start_y,end_x,end_y are equal to this‘s) ==> \result==false; */
↓
/** * @REQUIRES: * r!=null; * @MODIFIES:None; * @EFFECTS: * (r‘s time,start_x,start_y,end_x,end_y are equal to this‘s) ==> \result==true; * !(r‘s time,start_x,start_y,end_x,end_y are equal to this‘s) ==> \result==false; */
······································································································································
/** * @REQUIRES:None; * @MODIFIES:None; * @EFFECTS: * \result==\this.inputs.get(i).start_x; */
↓
/** * @REQUIRES: * 0<=i<\this.inputs.size(); * @MODIFIES:None; * @EFFECTS: * \result==\this.inputs.get(i).start_x; */
······································································································································
/** * @REQUIRES:None; * @MODIFIES: * \this.credit; * @EFFECTS: * \this.credit==\this.credit+1; */
↓
/** * @REQUIRES:None; * @MODIFIES: * \this.credit; * @EFFECTS: * \this.credit==\old(\this.credit)+1; */
······································································································································
/** * @REQUIRES: * req!=null; * @MODIFIES:None; * @EFFECTS: * \result == request in inputs that equals req ; */
↓
/** * @REQUIRES: * req!=null; * @MODIFIES:None; * @EFFECTS: * \result == (\exist Request r; inputs.contains(r);r.equals(req)); * @THREAD_REQUIRES: * \locked(\this); * @THREAD_EFFECTS: * \locked(); */
······································································································································
/** * @REQUIRES: * req!=null; * @MODIFIES: * \this.inputs; * @EFFECTS: * \this.inputs.contains(req) ; * @THREAD_REQUIRES: * \locked(\this); * @THREAD_EFFECTS: * \locked(); */
↓
/** * @REQUIRES: * req!=null; * @MODIFIES: * \this.inputs; * @EFFECTS: * \this.inputs.contains(req) && \this.inputs.size()=\old(\this.inputs).size()+1; * @THREAD_REQUIRES: * \locked(\this); * @THREAD_EFFECTS: * \locked(); */
······································································································································
/** * @REQUIRES:None; * @MODIFIES: * \this.reachlist; * \this.initreachlist; * @EFFECTS: * \this.reachlist == new Vector<Integer>(); * (\all Vector x;reachlist.contains(x);x!=null); * \this.initreachlist == new Vector<Integer>(); * (\all Vector x;initreachlist.contains(x);x!=null); */
↓
/** * @REQUIRES:None; * @MODIFIES: * \this.reachlist; * \this.initreachlist; * @EFFECTS: * \this.reachlist!=null; * (\all Vector x;reachlist.contains(x);x!=null); * \this.initreachlist!=null; * (\all Vector x;initreachlist.contains(x);x!=null); */
······································································································································
/** * @REQUIRES:None; * @MODIFIES:None; * @EFFECTS: * \result==queue!=null && inputs!=null && taxigui!=null && outFile!=null && taxis!=null && taxiInfo!=null && map!=null; */
↓
/** * @REQUIRES:None; * @MODIFIES:None; * @EFFECTS: * \result==queue!=null && inputs!=null && taxigui!=null && outFile!=null && taxis!=null && taxiInfo!=null && map!=null && queue.repOK() && inputs.repOK() && (\all Taxi t;taxis.contains(t);t.repOK()) && map.repOK(); */
······································································································································
四、思路与体会
由于出租车的框架是在第七次作业时搭建好的，后面基本没有做出大的变动，所以大部分的规格是看着方法补充。前置条件就从传入的参数入手，基本类型需要判断在指定范围内，对象类型则要求不为空。中间条件抓住本类的类变量，逐一检查是否在此方法中被改变。后置条件比较复杂，需要兼顾条件判断、数组遍历、返回值、类变量前后改变等，如果是逻辑太多的方法就只能挑出关键步骤，借助自然语言描述。
不同的遭遇，不同的体会。在三次作业的互测过程中，测试者并没有死抠我的规格细节，扣的分主要是因为自己的粗心大意，所以在承受范围之内。至于书写规格的体会，由于没有做到像老师在课堂上说的 “先写规格后写代码”，整个过程可以说是“重温方法思路，再按规定格式翻译一遍”。虽然体验效果有些欠佳，但依然不能否认规格化设计的重要性。在真正的工程化编程中，规格的确有提高效率，减少出错的作用。同时我也认为，“规格化”不仅仅是贯彻体现在方法前的几行JSF注释中，更重要的是从构想到实施的过程，真正具有 “规格化”的思想。
标签：针对 list IV 出错 应用 出租车 也有 作业 思路
原文地址：https://www.cnblogs.com/wjy21/p/9103151.html
