OO第三次博客做业

规格化设计发展历史

在调研的过程当中再一次验证了“百度搜索不适合学术”这个观点，没有找到合适的搜索结果后，转用Google，才找到了一些细节。

保证程序的正确性以及减小软件错误一直是程序员关注的问题，Hoare提出了基于“前置后置条件”的接口规格方法。

为了创建正确的类规格，近些年来，研究者们进行了抽象变量、接口规格、状态抽象、查询方法等不一样方面的尝试，并取得了很大的进展。

为保证程序的正确性， Hoare[l] 提出了关于接口的规格方法，即若一种方法在执行前知足前置条件，运行后知足后置条件，那么这种方法就是正确的。 Hoare 提出的这个结论为规格化发展起到了奠定的做用，也为类中接口的规格化提供了理论基础。

针对各方法的精确规格定义， MeyeP] 提出契约式编程延续了对方法的精肯定义，但其不足是依赖内部状态来体现方法之间的相互依赖。

课程中使用的JSF更偏向于“契约式设计”(Design by Contract)：为传统的抽象数据结构增长了先验条件、后验条件和不变式。

规格bug分析

bug类型	bug内容	出现位置
JSF检查->Requires不完整	忘写JSF	Windows类
方法规格检查->Effects不完整	JSF不完整	Taxi类
方法规格检查->JSF不符合规范	可追踪出租车没有写继承	Taxi2类

bug产生缘由：

• 第九次做业是JSF被扣分最严重的一次。我是写完代码而后再去写JSF，在金工实习上补全JSF就上交了，最后发现由于有一个类的JSF写漏了，对面对每个没写的方法规格报了15个JSF imcomplete...
• 不是过重视JSF，致使部分后置条件不够详细，最后两次做业总共被报了3个JSF。

前置条件后置条件写法改进

前置条件

(1)修改前

/** @REQUIRES : map!=null,taxiGUI!=null,GuiInfo!=null;
     * @MODIFIES : this.id,this.credit,this.map,this.taxiGUI,this.GuiInfo,this.flowMonitor,this.VIP;
     * @EFFECTS : None;
     */

对新增变量flowMonitor判断
修改后

/** @REQUIRES : map!=null,taxiGUI!=null,GuiInfo!=null,flowMonitor!=null;
     * @MODIFIES : this.id,this.credit,this.map,this.taxiGUI,this.GuiInfo,this.flowMonitor,this.VIP;
     * @EFFECTS : None;
     */

(2)修改前

/** @REQUIRES : id > 0;
     * @MODIFIES : None;
     * @EFFECTS : \result == id;
     */

不须要对id进行判断
修改后

/** @REQUIRES : None;
     * @MODIFIES : None;
     * @EFFECTS : \result == id;
     */

(3)修改前

/** @REQUIRES: None;
     * @MODIFIES: None;
     * @EFFECTS: \result == System.currentTimeMills();
     */

对于Thread进行追加Require
修改后

/** @REQUIRES: None;
     * @MODIFIES: None;
     * @EFFECTS: \result == System.currentTimeMills();
     * @THREAD_REQUIRES:\locked(\this);
     * @THREAD_EFFECTS:\locked(\this);
     */

(4)修改前

/** @REQUIRES: None;
     * @MODIFIES: None;
     * @EFFECTS: (distance==1) ==> \result = true
    (distance!=1) ==> \result = false
     */

对于坐标范围的判断
修改后

/** @REQUIRES: src>0 && src <80 && dst >0 && dst < 80;
     * @MODIFIES: None;
     * @EFFECTS: (distance==1) ==> \result = true
    (distance!=1) ==> \result = false
     */

(5)修改前

/** @REQUIRES : s!=null;
     * @MODIFIES : this.str;
     * @EFFECTS : str == s;
     */
    public Request(String s) {

基本数据类型不须要进行判断（编译器保证）
修改后

/** @REQUIRES : None;
     * @MODIFIES : this.str;
     * @EFFECTS : str == s;
     */
    public Request(String s) {

后置条件

(1)修改前

/** @REQUIRES: requestQueue!=null;taxiGUI!=null;
     * @MODIFIES: this.requestQueue,this.taxiGUI;
     * @EFFECTS: None;
     */

修改后

/** @REQUIRES: requestQueue!=null;taxiGUI!=null;
     * @MODIFIES: this.requestQueue,this.taxiGUI;
     * @EFFECTS: this.requestQueue == requestQueue, this.taxiGUI == taxiGUI;
     */

(2)修改前

/** @REQUIRES : None;
     * @MODIFIES : None;
     * @EFFECTS : \result == invariant(this);
     */

repOK 的具体判断
修改后

/** @REQUIRES : None;
     * @MODIFIES : None;
     * @EFFECTS : \result = (requestQueue != null);
     */

(3)修改前

/**@REQUIRES : readFile!=null;taxiGUI!=null;flowMonitor!=null;GuiInfo!=null;
     * @MODIFIES : requestQueue,readFile,taxiGUI,flowMonitor,GuiInfo;
     * @EFFECTS : this.requestQueue == requestQueue;
     *      this.readFile == readFile;
     *      this.taxiGUI == taxiGUI;
     *      this.flowMonitor == flowMonitor;
     */

对新增的GuiInfo没有修改Effects
修改后

/**@REQUIRES : readFile!=null;taxiGUI!=null;flowMonitor!=null;GuiInfo!=null;
     * @MODIFIES : requestQueue,readFile,taxiGUI,flowMonitor,GuiInfo;
     * @EFFECTS : this.requestQueue == requestQueue;
     *      this.readFile == readFile;
     *      this.taxiGUI == taxiGUI;
     *      this.flowMonitor == flowMonitor;
     *      this.GuiInfo == GuiInfo;
     */

(4)修改前

/** @REQUIRES : str!=null；
     * @MODIFIES : this.reqSame,this.timeSame；
     * @EFFECTS : \request.equals(同质请求添加到同质判断队列)；
     */

尽可能转换天然语言为逻辑语句
修改后

/** @REQUIRES : str!=null；
     * @MODIFIES : this.reqSame,this.timeSame；
     * @EFFECTS : reqSame.add(str),timeSame.add(time)
     */

(5)修改前

/** @REQUIRES : taxis!=null;
     * @MODIFIES : None;
     * @EFFECTS :None;
     */

get方法必定要写\result !
修改后

/** @REQUIRES : taxis!=null;
     * @MODIFIES : None;
     * @EFFECTS : \result == taxis;
     */

功能bug和规格bug的汇集关系

此次博客做业这样要求，按照可能的论证：因为不清楚代码的功能细节，因此致使出现了规格bug，这种规格bug伴随着方法的功能bug出现，因此会出现聚类关系。
因为JSF是在代码收工以后写的，因此基本没有聚类关系。
三次做业最严重的规格bug就是忘写部分JSF，其余出现规格bug的地方并无出现功能问题。
若是说有什么没有被报的功能bug,那么对应的规格bug必定是有的，只是没有被抓出来而已。

设计与撰写规格的思路

• Require部分：通常都是对于输入的形参作非空判断
• Modify部分：对于方法写到的private变量挨个判断是否修改
• Effects部分：对于Modify的变量变化的状况进行分析

最后使用JSFTool.class进行复查

心得体会

最近几回OO做业感受收获比较小，在作课程做业时对于Java的语法没有更深学习的动力，也没有Java与其余技术的结合应用，若是只是完成做业只须要JavaSE的部分语法基础而已。这两周花费大量时间在JSF的书写上，并且遇到对面的刁钻扣分也容易受到打击，可能你们都以为相对于程序的功能Bug，要扣规格的分不要容易太多吧。

参考文献 [1]王伟,丁二玉,骆斌.基于抽象状态的类的行为规格化方法[J].计算机科学,2016,43(S1):457-460.