第三次OO总结

规格化设计的调研

随着50年代高级语言的出现，编译技术不断完善，涌现出多种流派的语言，其中就有里程碑式的Pascal语言；进入70年代，由于众多语言造成的不可移植、难于维护，Ada程序设计语言诞生了，强调大型系统可读性胜于可写性，Ada程序自成清晰的文档；经过80年代计算机硬件和操作系统的改善，程序设计重点从算法和数据结构实现技术向规模说明方向转移。从空间的角度观察, 广义上来说, 软件规格说明描述的是整个软件系统；狭义来说, 软件规格说明描述的是软件系统的组成部件。从时间的角度来观察, 广义来说, 软件规格说明方法适用于整个软件生命周期； 狭义上来说, 软件规格说明方法仅适用于软件生命周期的特定阶段。规格化设计可以提高程序的可读性，也可以提高阅读效率，便于以后的修改。

规格bug

可能是我运气太好了，这几次都没被扣规格的bug……

改进写法

1. 前置条件

1.1 忽略前置条件

previous

　　public int[][] getMatrix(Point dst){
　　/**
　　     *@ REQUIRES: None
　　     *@ MODIFIES: visited, dist
　　     *@ EFFECTS: normal_behaver
　　　　       　　　 　\result == the shortest distance between point(x,y) from point(x2,y2) ;
　　*/
　　}

late

　　public int[][] getMatrix(Point dst){
　　/**
　　     *@ REQUIRES: !tmp.empty
　　     *@ MODIFIES: visited, dist
　　     *@ EFFECTS: normal_behaver
　　　　       　　　 　\result == the shortest distance between point(x,y) from point(x2,y2) ;
　　*/
　　}

1.2 前置条件不全

previous

　　private void chooseTaxi(){
　　/* *
    　　*@ REQUIRES: None
　　    *@ MODIFIES: \this.TarTaxi;
   　　 *@ EFFECTS: \any int i=0;i<this.list.size;i++:!list.get(i).getTaxiState().equals(TaxiState.STOP)==> \target = list.get(i);
　　*/　　}

late

　　private void chooseTaxi(){
　　/* *
    　　*@ REQUIRES: \this.taxi!=null&&\this.taxi is sorted by credit;
    　　*@ MODIFIES: \this.TarTaxi;
    　　*@ EFFECTS: \any int i=0;i<this.list.size;i++:!list.get(i).getTaxiState().equals(TaxiState.STOP)==> \target = list.get(i);
　　*/　　}

1.3 范围错误

previous

public void taxiControl(int n) {
        /**
         *@REQUIRES: n>0 && n<100
         *@MODIFIES: None;
         *@EFFECTS: ......
         */
    }

late

public void taxiControl(int n) {
        /**
         *@REQUIRES: n>=0 && n<100
         *@MODIFIES: None;
         *@EFFECTS: ......
         */
    }

1.4 自然语言

previous

    private int loadMap(BufferedReader Reader) throws IOException{
        /*
        @ REQUIRES: in this method we load the map
        @ MODIFIES: Map[][]
        @ EFFECTS:     \any char!=0&&char!=1 ==>System.out&&System.exit
                    \any somewhere not cross road but has light ==>System.out&&System.exit
        */
    }

late

    private int loadMap(BufferedReader Reader) throws IOException{
        /*
        @ REQUIRES: File(path).exist
        @ MODIFIES: Map[][]
        @ EFFECTS:     \any char!=0&&char!=1 ==>System.out&&System.exit
                    \any somewhere not cross road but has light ==>System.out&&System.exit
        */
    }

1.5 格式错误

previous

public void run(Taxi t){
        /*
          @ REQUIRES: \t.status.equals(TaxiStatus.SERVING);
          @ MODIFIES: None
          @ EFFECTS: ......
         */
    }

late

public void run(Taxi t){
        /**
         @ REQUIRES: t.status.equals(TaxiStatus.SERVING);
         @ MODIFIES: None
         @ EFFECTS: ......
         */
    }

2. 后置条件

2.1 自然语言

previous

    public synchronized void changeRoute() {
        /*
        @ REQUIRES: None
        @ MODIFIES: None
        @ EFFECTS: get the minimum flow and change the route
         */
    }

late

    public synchronized void changeRoute() {
        /*
        @ REQUIRES: None
        @ MODIFIES: None
        @ EFFECTS: \result = this.route = this.map.minRoute(this.position, point);
         */
    }

2.2 后置条件不全

previous

    private int getDir(Point from, Point to){
        /*
        @ REQUIRES: None
        @ MODIFIES: None
        @ EFFECTS:     (to.getX() - from.getX() > 0) \return = 0;//D
                    (to.getX() - from.getX() < 0) \return = 1;//U
                    (to.getY() - from.getY() > 0) \return = 2;//R
                    (to.getY() - from.getY() < 0) \return = 3;//L
        */    }

late

    private int getDir(Point from, Point to){
        /*
        @ REQUIRES: None
        @ MODIFIES: None
        @ EFFECTS:     (to.getX() - from.getX() > 0) \return = 0;//D
                    (to.getX() - from.getX() < 0) \return = 1;//U
                    (to.getY() - from.getY() > 0) \return = 2;//R
                    (to.getY() - from.getY() < 0) \return = 3;//L
                    \return = 4;
        */    }

2.3 没有体现modified的改变

previous

    public void run() {
        /*
        @ REQUIRES: None
        @ MODIFIES: system， r, position. credit, state, req, route, timer
        @ EFFECTS:     \this.state = 2&&\this.reqList.isEmpty==>\this.lastposition = \old.this.position;\this.position = getNextPos();t+=0.2+checkLight(lastposition, position, p);
                    \this.state = 2&&!\this.reqList.isEmpty==>\this.lastposition = \old.this.position;\this.position = getNextRoute();t+=0.2+checkLight(lastposition, position, p);
                    \this.state = 1||\this.state = 3==>this.lastposition = \old.this.position;\this.position = getNextRoute();t+=0.2+checkLight(lastposition, position, p);
                    \this.state = 0 ==> t+=0.2+checkLight(lastposition, position, p);
        */
    }

2.4 不符合格式规定

previous

    public boolean repOK() {
        /*
        @ REQUIRES: None
        @ MODIFIES: None
        @ EFFECTS:  (this.map==null||this.map.length==0) \result = false;
                    \result = true;
         */
    }

late

    public boolean repOK() {
        /*
        @ REQUIRES: None
        @ MODIFIES: None
        @ EFFECTS:  (this.map==null||this.map.length==0) ==> \result == false;
                    (this.map!=null&&this.map.length!=0) ==> \result == true;
         */
    }

2.5 忽略后置条件

心得体会

这个规格也不知道该说点什么，都是写完代码看着复制粘贴，改改格式，然后基本也都是电工课解决的hhh可能之后3次要认真一点了

我一直很佛，对自己的程序和别人的程序都是随便测几个，虽然这不是对学术负责的态度？但是觉得吧几天写出来的东西怎么也会有错，至少我是这么认为自己的。自从ifttt自暴自弃，我就没被报过bug（除了第一次出租车的loadfile有点问题，主要还是自暴自弃吧）可能是大难不死必有后福？不过OO倒是让我知道了要更热爱生活，不然除了黑黢黢的屏幕，什么都不剩了。