OO第三次阶段性总结

时间  2019-12-07
标签 第三次 阶段性 总结 繁體版
原文   原文链接

1、规格化设计的历史以及人们重视的缘由

发展历史

从20世纪60年代开始，就存在着许多不一样的形式规格说明语言和软件开发方法。在形式规格说明领域一些最主要的发展过程列举以下：java

1969－1972 C.A.R Hoare撰写了"计算机编程的公理基础（An Axiomatic Basis for Computer Programming）"和"数据表示的正确性证实"两篇开创性的论文，并提出了规格说明的概念。git

1974－1975 B.Liskow/S.N. Zilles和J. Guttag引入了"抽象数据类型"的概念。算法

1976      E.W. Dijkstra定义了"最弱前置条件"的概念编程

1977      R.Burstall和J.Goguen提出了第一个代数规格说明语言：Clearapp

1988      Standford的SRI开发了代数规格说明语言OBJ3ide

1980-1986 C.Jones定义了VDM语言，也就是维也纳开发方法。测试

1985－1992  牛津大学的程序研究小组开发了Z规格说明语言。与此同时BP研究室开发了称之为B方法的面向模型的规格说明语言。this

1985－1993 在MIT和Digital SRC开发了代数规格说明语言Larchspa

从1991年开始，面向对象的形式规格说明语言开始发展，例如，Object-Z, VDM++, CafeOBJ等语言。设计

1996－2000年 在欧洲CoFI（Common Framework Initiative）项目资助下开发"统一"代数规格说明语言CASL(Common Algebraic Specification Language)

重视缘由

我认为规格首先给了你们编程时一个统一的认识，明确了程序运行的前提和程序运行后的效果，这一点在我的编程中有助于理清思路，而在集体的工程开发过程当中也有助于协做，使你们开发的方向一致。

另外一方面我认为正确的规格能够方便编程者进行调试，经过断言判断前置条件是否知足以及检验后置条件是否在程序运行后知足。

2、规格Bug数量及缘由分析

做业 Bug类型及细节 所在文件及行数
第九次 无 无
第十次 Effects内容为实现算法：\result写成了\return 不少文件中
第十一次 Effects不完整：在有try-catch的方法中忘记写exceptional_behavior InputHandler.java/192

规格bug缘由分析：第九次没有被报规格bug，大概是测试者不太关心。第十次和第十一次做业中都是有所疏忽致使。其中第十次做业是一个笔误，几乎全部文件都写成了\return==balabala，第十一次做业中有一个方法因为后来有改动，没有添加exceptional_behavior。

3、很差的规格写法及改进

前置条件

1. 天然语言描述

1     /**
2      * @REQUIRES: k存在
3      * @MODIFIES: v
4      * @EFFECTS: v == \old(v) + 1;
5      */
很差 
1     /**
2      * @REQUIRES: k != null
3      * @MODIFIES: v
4      * @EFFECTS: v == \old(v) + 1;
5      */
好

2. 不是布尔表达式

    /**
     *
     * @REQUIRES:
     *      this.taxiStatus = IDLE;
     * @MODIFIES:
     *      this.credit;
     * @EFFECTS:
     *      this.credit = \old(this.credit) + 1;
     *      (\all PassengerRequest r in range, r.grabbedByTaxi(this))
     *
     */
很差 
    /**
     *
     * @REQUIRES:
     *      this.taxiStatus == IDLE;
     * @MODIFIES:
     *      this.credit;
     * @EFFECTS:
     *      this.credit = \old(this.credit) + 1;
     *      (\all PassengerRequest r in range, r.grabbedByTaxi(this))
     *
     */
好

3. 没有规定范围

    /**
     *
     * @REQUIRES:
     *       locX, locY, dstX, dstY；
     * @MODIFIES:
     *     edge between (locX, locY),(dstX, dstY), ConsolePrinter;
     * @EFFECTS:
     *     edge.existence == op;
     *
     */
很差 
    /**
     *
     * @REQUIRES:
     *     0 <= locX, locY, dstX, dstY <= 79;
     * @MODIFIES:
     *     edge between (locX, locY),(dstX, dstY), ConsolePrinter;
     * @EFFECTS:
     *     edge.existence == op;
     *
     */
好

4. 遗漏了某些条件，通常是传入参数外的某些条件

    /**
     * @REQUIRES: mapVertex != null;
     * @MODIFIES: ConsolePrinter
     * @EFFECTS: \result == the opposite vertex of mapVertex
     */
很差 
    /**
     * @REQUIRES: mapVertex != null && mapVertex.repOK == true;
     * @MODIFIES: ConsolePrinter
     * @EFFECTS: \result == the opposite vertex of mapVertex
     */
好

5. 对于一个容器中的全部对象，均须要规定前置条件

    /**
     *
     * @REQUIRES:
     *      this.edgeMap != null
     * @MODIFIES:
     *      None
     * @EFFECTS:
     *      (\exist MapEdge e, edgeMap.contains(e), \min(edgeMap.flowrates) == e.flowrate && \result == e);
     *
     * @THREAD_EFFECTS:
     *      (\ all MapEdge e in this.edgeMap);
     */
很差 
    /**
     *
     * @REQUIRES:
     *      (\ all MapEdge e, this.edgeMap.contains ( e), e != null)
     * @MODIFIES:
     *      None
     * @EFFECTS:
     *      (\exist MapEdge e, edgeMap.contains(e), \min(edgeMap.flowrates) == e.flowrate && \result == e);
     *
     * @THREAD_EFFECTS:
     *      (\ all MapEdge e in this.edgeMap);
     */
好

后置条件

1. 不是布尔表达式

    /**
     *
     * @REQUIRES:
     *      this.requestQueue != null
     * @MODIFIES:
     *      None
     * @EFFECTS:
     *      return this.requestQueue;
     *
     */
很差 
    /**
     *
     * @REQUIRES:
     *      this.requestQueue != null
     * @MODIFIES:
     *      None
     * @EFFECTS:
     *      \result == this.requestQueue;
     *
     */
好

2. 返回容器时不够明确

    /**
     *
     * @REQUIRES:
     *      this != null
     * @MODIFIES:
     *      None
     * @EFFECTS:
     *      \result == (\all MapEdge e in this.edgeMap)
     *
     */
很差 
    /**
     *
     * @REQUIRES:
     *      this != null
     * @MODIFIES:
     *      None
     * @EFFECTS:
     *      \result == new Arraylist<MapEdge> r;
     *      (\all MapEdge e, this.edgeMap.contains(e), r.contains(e))
     *
     */
好

3. 改变值书写不规范

    /**
     *
     * @REQUIRES:
     *      this != null, num > 0;
     * @MODIFIES:
     *      this.credit;
     * @EFFECTS:
     *      this.credit +=  num;
     *
     */
很差 
    /**
     *
     * @REQUIRES:
     *      this != null, num > 0;
     * @MODIFIES:
     *      this.credit;
     * @EFFECTS:
     *      this.credit == \old(this.credit) + num;
     *
     */
好

4. 没有写异常状况

        /**
         * @REQUIRES:
         *         this.list != null;
         * @MODIFIES:
         *         None
         * @EFFECTS:
         *         this.hasNext() ==> (\result == this.list[\old(index)+1] && index == \old(index) + 1);
         *
         * @THREAD_EFFECTS:
         *      \locked(this.list);
         */
很差 
        /**
         * @REQUIRES:
         *         this.list != null;
         * @MODIFIES:
         *         None
         * @EFFECTS:
         *         this.hasNext() ==> (\result == this.list[\old(index)+1] && index == \old(index) + 1);
         *         exceptional_behavior(NoSuchElementException)
         *
         * @THREAD_EFFECTS:
         *      \locked(this.list);
         */
好

5. 后置条件没写全

    /**
     * @REQUIRES: key != null;
     * passengerRequest != null;
     * @MODIFIES: this.unprocessedRequests, ConsolePrinter;
     * @EFFECTS: unprocessedRequests.contains(passengerRequest);
     * @THREAD_EFFECTS: \locked(this.appendlock);
     */
很差 
    /**
     * @REQUIRES: key != null;
     * passengerRequest != null;
     * @MODIFIES: this.unprocessedRequests, ConsolePrinter;
     * @EFFECTS: unprocessedRequests.contains(passengerRequest); unprocessedRequests.size == \old(unprocessedRequest).size + 1
     * @THREAD_EFFECTS: \locked(this.appendlock);
     */
好

4、功能Bug与规格Bug的聚类关系

本人仅在第九次做业中被报了功能bug，分别是输入格式错误会致使crash（说好的测试者保证呢）以及bfs在添加流量后判断条件有误致使找出了流量最小而不是距离最近的道路（在车汇集在一堆的时候可能绕路）。

以后的jsf问题我认为均是格式或者规范问题，与功能并无什么关系，基本上都是功能实现正确但jsf写的时候可能有所遗漏。

5、撰写规格的思路与体会

以前写做业每每是先写程序代码最后再写规格，后来有尝试先写规格再改程序代码。规格的问题每每出在改正了程序的代码，而后程序跑着没什么问题了，结果改的地方一多就忘记改规格了。虽然看群里你们对于JSF的设计都有些抱怨，但JSF在复查代码的方面的确有必定的帮助，也对我造成工程化思想有了一些小小的推进做用。

但愿课程组能够逐渐完善JSF，起码如今感受不少复杂的逻辑用JSF表达起来很是费力以致于不得不用天然语言。

相关文章
相关标签/搜索
每日一句
    每一个你不满意的现在，都有一个你没有努力的曾经。
本站公众号
   欢迎关注本站公众号,获取更多信息
联系我们 最近搜索 最新文章 沪ICP备13005482号-10 MyBatis教程 SQL 教程 MySQL教程 Java 教程 Thymeleaf 教程 Hibernate教程 Spring教程 Redis教程