一、规格化设计相关
编程语言的规格化使用历史在网上的资料真的很少，我查阅了维基百科和谷歌学术的相关论文，关于这部分的讨论非常少。但可以确定的是，规格化的使用和工业上规范规格是有很大关系的，程序语言的发展和工业制造的发展有着一定的相似性。诸如国际化标准组织ISO，其宗旨是促进时间范围内的标准化工作的发展，推动国际间知识、科学、技术和经济方面的合作。具体来讲，它需要协调世界范围内的标准化工作，与其他国际性组织合作研究有关标准化问题。我们课上所讲和课下所用的规格化是为了规范方法使用的。工业产品和程序一样是面向用户生产的，这个用户可以是通常意义上的普通消费者，也可以是企业用户。在面向企业用户的制造中，工业产品的规格化可以申明产品的属性，包括各种尺寸，用途等；程序的规格化可以说明程序的用途、使用方法、使用条件和副作用。一段代码非常重要的一个用途，是让别人看懂，其次才是可以运行。
正因如此，程序规格化设计越来越被人们重视，其对于代码编写的规范能够让程序变得更加易懂，能让使用者更加轻松简单的学会如何正确使用这段程序。此外，通过规格的抽象和总结，使用者能够直接使用这段程序而免去浪费大量时间来看懂代码的痛苦过程。更重要的是，代码的维护变得更加简单。其一，按我自身的经历，程序中隐藏的逻辑错误比如括号位置写错或者其他有关优先级的bug，在找到相应错误方法后能够非常轻松的通过抽象出来的规格判断代码具体错误位置。其二，在真正的做项目开发时，规格化设计能够方便整个团队的开发，因其能够统一规范每个人的编写方式，能使分工更加细致，使团队之间更加协调。
二、规格bug
分析：首先标签格式错误这个问题只在第一次使用规格书写，也就是第九次作业时有。由于经验不足，我把REQUIRES、MODIFIES和EFFECTS全写成了小写。THREAD_EFFECTS和THREAD_REQUIRES错误同样也是在第九次作业中产生的，对于需要同步的方法和对象我并没有书写完全。EFFECTS不是布尔表达式这个bug被报了不少次，最基本的也是在第九次作业中，某些方法的规格书写不是非常完善，导致了后续作业继承过去的代码同样有规格上不完善的地方，而且由于一些不谨慎的原因，后续作业新编写的方法同样有一些不规范的地方，比如前置条件不完等。
三、改进
1.
/** * @REQUIRES: None * @MODIFIES: None * @EFFECTS: (\all int i; 0<=i<=r.taxis.size())==>\result.contains(MAX(r.taxis.get(i).credit)) */
在这个方法中，输入参数为一个具体的Request对象，方法功能是找到抢到该订单的拥有最大信用的出租车并返回，具体返回值是一个包含信用最大出租车的ArrayList。在方法具体的实现上，我并没有考虑输入指向空的情况，因此这部分JSF的前置条件写的不完整。此外，关于这个函数的后置条件我想了很久，找到最大值的部分如果使用方法内的具体代码会使后置条件变成算法实现，所以在这部分中使用一定的自然语言是相对合理的。
改进如下
/** * @REQUIRES: r!=null * @MODIFIES: None * @EFFECTS: (\all int i; 0<=i<r.taxis.size) && (\exists int j; 0<=j<r.taxis.size && r.taxis[j].credit>=r.taxis[i]) * ==>\result.contains(j)==true */
2.
/** * @REQUIRES: None * @MODIFIES: position of this taxi this.x, this.y, this.roadchanged, this.time * @EFFECTS: (\ exists points connected and nearest)==>taxi.position = point */
这一部分代码是出租车核心组成部分之一。其具体工作内容是在出租车处于去订单起始地点接乘客和接到乘客之后送乘客去订单目的地。上述规格书写中前置条件写的并不完整，副作用不清晰。这个方法具体上只管出租车的具体行进，其中寻路部分是使用其他方法直接计算返回一个相邻的最佳的点。参数输入部分只有一个Point类型的p，内容为出租车现在所处的点。把他设计成参数输入是为了避免其他可能的对出租车位置的影响，使其能够始终运行在计算好的正确的路线上。而且部队输入参数进行任何更改，行进是通过更改出租车对象自身位置属性达到的。
改进如下
/** * @REQUIRES: p.x>=0 && p.x<=79 && p.x>=0 && p.y<=79 * @MODIFIES: None * @EFFECTS: (int x, y; (x==(\old)this.x-1&&y==(\old)this.y) || (x==(\old)this.x+1&&y==(\old)this.y) || (x==(\old)this.x&& y==(\old)this.y-1) || (x==(\old)this.x&& y==(\old)this.y+1)) * && (Distance[x][y] == Distance[(\old)this.x][(\old)this.y]-1)==>(this.x==x && this.y==y) */
3.
/** * @REQUIRES: None * @MODIFIES: None * @EFFECTS: (findMaxCredit(r).size>1)==>(find_nearest(r, availiable_taxis).size>1)==>\result find_nearest(r, availiable_taxis)[0] */
这部分代码是请求线程的核心组成部分之一。具体工作内容是当指令的时间窗口度过之后选择一个最佳的抢到单的出租车进行派单。和第一个方法相同的是参数数部份同样有一个指令，而且代码部分同样没考虑指令指向空的情况。我认为后置条件部分使用自然语言能够使方法描述更简洁。
改进如下：
/** * @REQUIRES: r!=null * @MODIFIES: None * @EFFECTS: \result = taxi && (the first taxi found has max credit and is the nearest) */
4.
/** * @REQUIRES: request!=NULL && Main.requestsQueue!=NULL && Request_pattern!=NULL * @MODIFIES: Main.requests * @EFFECTS: (!request.matches(Request_patern))==> print "Wrong Input_LoadRequest()" * call setRequest() * tmpr = return value of setRequest() * (tmpr.getSrc().x==tmpr.getDst().x && tmpr.getSrc().y==tmpr.getDst().y) ==> \result * (isEqual(tmpr)) ==> Main.requestQueue.contains(tmpr) * call Main.gui.RequestTaxi() */
这部分代码使是输入处理线程的核心组成部分之一。具体工作内容是Load指令初始化程序时初始指令的加载和之后控制台输入指令的处理。两部分工作有很大的相同点因此我给他们抽象出来了同一个方法。方法的输入参数是一个字符串，方法中有对字符串各种形式的判断，因此前置条件关于字符串的部分可以省略。其次并没有对输入参数做任何的更改因此没有副作用。这部分规格书写的后置条件部分，大致写成了算法实现。
改进如下：
/** * @REQUIRES: None * @MODIFIES: None * @EFFECTS: (!request.matches(Request_pattern))==>print "Wrong Input_LoadRequest()" * (request.matches(Request_pattern))==>Main.requestsQueue.contains(request object which has the information of the input request) */
5.
/** * @REQUIRES: None * @MODIFIES: this.x, this.y, state * @EFFECTS: this.x == p.x && this.y == p.y && this.State == state; */
这部分代码比较简单，是Load初始化命令时调用的用于设定出租车初始位置和出事信用值的线程安全的方法。输入参数是一个Point类型的对象p，和一个int类型的状态值。方法代码中并没有对任何上述参数进行正确性验证因此前置条件部分需要改进。此外方法中同样没有对任何输入参数进行更改，所以副作用部分有错误。
改进如下：
/** * @REQUIRES: p.x>=0 && p.x<=79 && p.y>=0 && p.y<=79 && state>=0 && state<=3 * @MODIFIES: None * @EFFECTS: this.x == p.x && this.y == p.y && this.State == state; */
四、聚焦关系
五、心得体会
总的来说，这三次作业比中期的三次作业要好写很多，一个很大的原因是有了中期三次作业对多线程编程的锻炼。在代码设计上有了很大的提高之后进行编写事半功倍。这三次作业是本学期OO课程中最后的一个编程周期了，一共的九次训练，我的编程能力真的有了非常大的提高，从设计上到代码的编写方式上，现在回头看第一次多项式作业的代码真的可以说的上是惨不忍睹，很多地方情况的遗漏，算法实现上的各种妥协等。学习过程是痛苦的，编程过程是痛苦的，测试过程也是痛苦的，不过最后真的是值得的。
原文地址：https://www.cnblogs.com/NULL233/p/9095916.html