OO第三次总结

Posted 2020-11-09 ll--

OO第三次总结

规格化设计的发展历史和受到重视的原因

? 20世纪60年代，软件出现严重的危机，Dijkstra于1968年发表著名的《GOTO有害论》，由此引发了软件界长达数年的论战，并产生了结构化的程序设计方法。随着计算机技术的发展，结构设计化语言和结构化分析已经无法满足用户的需求，OOP由此应运而生，即面向对象的程序设计。面向对象程序设计的诞生是程序设计方法学的一场革命，大大提高了开发效率，减少了软件开发的复杂度，提高了软件的可维护性，可扩展性。1990年以来，面向对象分析、测试、度量和管理研究都得到长足的发展。规格化设计随其而生，为了提高程序的规范性，对类。方法等进行规范化设计，有利于模块化的划分。最实际的，通过规格化设计，在进行大型多人的开发工作时，可以确保程序员之间能够便捷地在他人的基础之上开始自己的工作，大大提高了工作效率，也方便他人理解代码，所以受到了大家的重视。

规格bug分析

Bug类型	出现位置	方法行数
Effects不完整	mapInfo类point2N函数	5
Modifies逻辑错误	Taxi类refreshGUI函数	11

产生规格bug的原因

protected  void refreshGUI() {
    /**
     *  @REQUIRES: None;
     *  @MODIFIES: None;
     *  @EFFECTS: None;
     *  @THREAD_EFFECTS: \locked(readWriteLock.readLock);
     */
    readWriteLock.readLock().lock();
    int tempStatus = 0;
    //其中0- 停止运行；1-服务（在运行且车内有乘客）；2-等待服务（在运行但车内无乘客），3-准备服务。
    switch (status) {
        case STOPING: tempStatus = 0; break;
        case SERVING: tempStatus = 1; break;
        case WAITING: tempStatus = 2; break;
        case ORDERED: tempStatus = 3; break;
    }
    readWriteLock.readLock().unlock();
    gui.SetTaxiStatus(No, currentPos, tempStatus);
}

在这个函数中我忽略了调用gui方法时会更改gui，更改如下：

/**
 *  @REQUIRES: None;
 *  @MODIFIES: gui;
 *  @EFFECTS: gui.SetTaxiStatus(No,currentPos,tempStatus);
 *  @THREAD_EFFECTS: \locked(readWriteLock.readLock);
*/  

private int point2N(Point point) {
    /**
         *  @REQUIRES: point != null;
         *  @MODIFIES: None;
        *   @EFFECTS: \result == point.x * mapSize + point.y;
        */
    if (point == null) {
        System.out.println("ERROR : NULL POINTER!");
        return 0;
    }
    return point.x * mapSize + point.y;
}

这里返回值忽略了point=null时为0的情况，更改如下：

  /**
    *  @REQUIRES: point != null;
    *   @MODIFIES: None;
    *   @EFFECTS:   \result == point.x * mapSize + point.y && point != null
    *           || \result == 0 && point == null;
    */

改进规格

1.mapInfo 类的 refreshMap 函数

    public void refreshMap(int[][] map, TaxiGUI gui) {
        /**
         *  @REQUIRES: map!=null;
         *  @MODIFIES: this.map;gui;
        *   @EFFECTS: this.map == map;
        */
        readWriteLock.writeLock().lock();
        this.map = map;
        if (this == instance) {
            gui.LoadMap(map, mapSize);
        }
        readWriteLock.writeLock().unlock();
    }

在这个方法中要载入一张新的地图，这时需要对地图大小进行判断，否则如果map仅仅非空，大小不正确可能导致后续程序崩溃。更改如下：

/**
    * @REQUIRES: map!=null && map.length == MAPSIZE 
    *                    && (\all Integer i; i<MAPSIZE && i>=0; map[i].length == MAPSIZE);
    * @MODIFIES: this.map;gui;
    * @EFFECTS: this.map == map;
    */

2.MapFlow 类的 setMapFlow 方法

public void setMapFlow(ArrayList<Point> p1s, ArrayList<Point> p2s, ArrayList<Long> values) {
        /**
         *  @REQUIRES: p1s!=null;p2s!=null;values!=null;
         *  @MODIFIES: edgeFlows;
        *   @EFFECTS: None;
        */
    readWriteLock.writeLock().lock();
    for (int i = 0; i < MapSize*MapSize*2; i++) {
        edgeFlows[i] = new EdgeFlow();
    }
    for (int i = 0; i < p1s.size(); i++) {
        int n = Point2N(p1s.get(i), p2s.get(i));
        if (map.isConnected(p1s.get(i), p2s.get(i))) {
            edgeFlows[n].flow = values.get(i);
        }
    }
    readWriteLock.writeLock().unlock();
}

在这个方法的 JSF 中仅要求了三个列表参数非空，但是在函数实现时没有判断列表长度为零或三个列表不等长的情况。更改如下：

/**
 *  @REQUIRES: p1s!=null && p2s!=null && values!=null 
 *          && p1s.size() > 0 
 *          && p2s.size() == p1s.size() && values.size() == p1s.size();
 *  @MODIFIES: edgeFlows;
 *  @EFFECTS: None;
*/

3.RequestMatrix 类的 isSame 方法

public synchronized boolean isSame(ReqSchedular req) {
        /**
         *  @REQUIRES: request!=null;
         *  @MODIFIES: None;
        *   @EFFECTS: requestSchedular.equals(request);
        */
    for (ReqSchedular reqSchedular : reqMatrix[req.Src().x][req.Src().y].reqList) 
    {
        if (reqSchedular.equals(req)) {
            return true;
        }
    }
    return false;
}

这里是首次写规格时不熟悉遗留下的错误，缺少锁的影响且返回值格式不正确，更改如下：

    /**
     *  @REQUIRES: request!=null;
     *  @MODIFIES: None;
    *   @EFFECTS: \result == true ==> 
    *           ( \exist ReqSchedular reqS; 
    *             reqMatrix[req.Src().x][req.Src().y].reqList.contains(reqS);
    *             reqS.equal(req) )
    *   @THREAD_EFFECTS: \locked(this);
    */

4.MapFlow 类的 updateEdgeFlow方法

public void updateEdgeFlow(Point p1, Point p2, long value) {
    /**
     *  @REQUIRES: p1!=null;p2!=null;value!=null;
     *  @MODIFIES: edgeFlows[n];
    *   @EFFECTS: None;
    */
    if (p1.equals(p2))
        return;
    int n = Point2N(p1, p2);
    if (map.isConnected(p1, p2)) {
        readWriteLock.readLock().lock();
        edgeFlows[n].readWriteLock.writeLock().lock();
        edgeFlows[n].flow = edgeFlows[n].flow + value;
        edgeFlows[n].readWriteLock.writeLock().unlock();
        readWriteLock.readLock().unlock();
    }
}

更改为：

/**
 *  @REQUIRES: p1!=null;p2!=null;value!=null;
 *  @MODIFIES: edgeFlows[n];
*   @EFFECTS: n = Point2N(p1, p2) && edgeFlows[n].flow == \old(edgeFlows[n].flow) + value;
*   @THREAD_EFFECTS: \lock(readWriteLock.readLock);
*                   \lock(edgeFlows[n].readWriteLock.writeLock)
*/

5.FlowThread 类 run方法

    public void run() {
        /**
         *  @REQUIRES: p1 != null && p2 != null;
         *  @MODIFIES: None;
        *   @EFFECTS:None;
        */
        try {
        if (p1.equals(p2))
            return;
        try {
            sleep(FlowTimeWindow);
        } catch (InterruptedException e) {
            // TODO Auto-generated catch block
            //e.printStackTrace();
            System.out.println("Flow Thread : sleep crash! ");
        }
        mapFlow.updateEdgeFlow(p1, p2, -1);
        } catch (Exception e) {
            System.out.println("Flow Thread Exception!");
        }
    }

改为：

/**
 *  @REQUIRES: p1 != null && p2 != null;
 *  @MODIFIES: None;
 *  @EFFECTS: !p1.equals(p2) ==> (sleep(FolwTimeWindow) && mapFlow.updateEdgeFlow(p1,p2,-1));
*/

分析被报的功能bug与规格bug在方法上的聚集关系

? 在互测中被挑出的功能bug和规格bug关联并不大，可能是笔者刚刚接触JSF，有许多函数方法功能可以正确实现但是功能并不完善，所以被找了规格bug，笔者认为互测阶段被报的大量 JSF 的bug往往是测试者刻意为之（当然我也承认书写不够规范）。功能bug往往是比较复杂的函数中存在逻辑漏洞，这类函数的规格比较复杂，可能存在逻辑错误，但测试者并没有仔细分析，所以大多没有报JSF bug。我想这也是这种测试机制存在的一些问题，被测出的规格问题并不能反映程序的功能实现问题，而对于复杂函数，被测者通过写规格为做出的优化，也很少通过测试反映出来。

设计规格和撰写规格的基本思路和体会

? 写规格可以强制要求程序员降低简化每个成员方法的复杂度，在写程序之前能够明确一个方法的具体作用和影响，对程序作者和读者而言都是一个明确、严谨的说明。但有的时候一些逻辑不好表述的过程的确很难写出简洁的规格，甚至让规格比代码还长。在一些开源代码中，许多规格都是一些自然语言的注释，反而更让人清晰的理解一个方法的作用。在我个人看来，用布尔表达式书写的规格在有些情况下是比较冗余，且难懂的，虽然从逻辑上可能会更准确。另外对于OO课程的 JSF 测试部分，我认为并没有达到很好的效果，许多人的恶意挑错反而降低了同学们的学习积极性。