oo第三次博客

Posted 2020-11-09 fakeboom

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

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

二、被报告的规格bug

 

bug类型	出现位置
requires逻辑错误	main.java 37

 

 

 

 

其实最后一次作业被报告了7个jsf错误但是我觉得除了这一个其余的都不合理，已经申请仲裁，也会在下文提到。

三、产生规格bug的原因

/**
     * @REQUIRES: none;
     * @MODIFIES:  this.map;
     * @EFFECTS:  this.map!=\old(this).map;
     */
    public void readmap(String path){
        
        Scanner scan=null;
        File file=new File(path);
        if(file.exists()==false){
            System.out.println("地图文件不存在,程序退出");
            System.exit(1);
            return;
        }
        try {
            scan = new Scanner(new File(path));
        } catch (FileNotFoundException e) {
            
        }
        for(int i=0;i<80;i++){
            String[] strArray = null;
            try{
                strArray=scan.nextLine().split("");
            }catch(Exception e){
                System.out.println("地图文件信息有误，程序退出");
                System.exit(1);
            }
            for(int j=0;j<80;j++){
                try{
                    this.map[i][j]=Integer.parseInt(strArray[j]);
                }catch(Exception e){
                    System.out.println("地图文件信息有误，程序退出");
                    System.exit(1);
                }
            }
        }
        scan.close();
    }

此处的path如果不加判定，可能会产生crash，所一这块是我在写jsf的时候疏忽了。

应该改为

/**
     * @REQUIRES: path!= null;
     * @MODIFIES:  this.map;
     * @EFFECTS:  this.map!=\old(this).map;
     */

四、改进方法

（1）前置条件改进

 

/**
     * @REQUIRES: none;
     * @MODIFIES:  this.light;
     * @EFFECTS:  this.light!=\old(this).light;
     */
    public void readlight(String path){
        
        Scanner scan=null;
        File file=new File(path);
        if(file.exists()==false){
            System.out.println("红绿灯文件不存在,程序退出");
            System.exit(1);
            return;
        }
        try {
            scan = new Scanner(new File(path));
        } catch (FileNotFoundException e) {
            
        }
        for(int i=0;i<80;i++){
            String[] strArray = null;
            try{
                strArray=scan.nextLine().split("");
            }catch(Exception e){
                System.out.println("红绿灯文件信息有误，程序退出");
                System.exit(1);
            }
            int k = 0;
            for(int j=0;j<80&&k<strArray.length;k++){
                //try{
                    if(strArray[k].equals("1")||strArray[k].equals("0")) {
                        this.light[i][j]=Integer.parseInt(strArray[k]);
                        j++;
                    }
                //}catch(Exception e){
                    //System.out.println("红绿灯文件信息有误，程序退出");
                    //System.exit(1);
                //}
            }
        }
        scan.close();
    }

 

改为

/**
     * @REQUIRES: path!=null;
     * @MODIFIES:  this.light;
     * @EFFECTS:  this.light!=\old(this).light;
     */

(2)后置条件

    /**
     * @REQUIRES: num>=0 && num<100;
     * @MODIFIES: this.init;
     * @EFFECTS:  none;
     */
    public synchronized void init(int num) {
        
        init[num] = 1;
    }

改为

    /**
     * @REQUIRES: num>=0 && num<100;
     * @MODIFIES: this.init;
     * @EFFECTS:  init[num] == 1;
     */
    public synchronized void init(int num) {
        
        init[num] = 1;
    }

    /**
     * @REQUIRES: num>=0 && num<100;
     * @MODIFIES: none;
     * @EFFECTS: none;
     */
    public synchronized int getinit(int num) {
        
        return init[num];
    }

改为

    /**
     * @REQUIRES: num>=0 && num<100;
     * @MODIFIES: none;
     * @EFFECTS: \result == init[num];
     */
    public synchronized int getinit(int num) {
        
        return init[num];
    }

    /**
     * @REQUIRES: num>=0 && num<100;
     * @MODIFIES: none;
     * @EFFECTS: none;
     */
    public synchronized int getstatus(int num) {

        return status[num];
    }

改为

    /**
     * @REQUIRES: num>=0 && num<100;
     * @MODIFIES: none;
     * @EFFECTS: \result == status[num];
     */
    public synchronized int getstatus(int num) {

        return status[num];
    }

    /**
     * @REQUIRES: none;
     * @MODIFIES: none;
     * @EFFECTS: none;
     */
    public synchronized int[][] getnl(){

        return nowlocation;
    }

改为

    /**
     * @REQUIRES: none;
     * @MODIFIES: none;
     * @EFFECTS: \result == nowlocation;
     */
    public synchronized int[][] getnl(){

        return nowlocation;
    }

    /**
     * @REQUIRES: num>=0 && num<100;
     * @MODIFIES: none;
     * @EFFECTS: none;
     */
    public synchronized int[] getnls(int num) {

        return nowlocation[num];
    }

改为

    /**
     * @REQUIRES: num>=0 && num<100;
     * @MODIFIES: none;
     * @EFFECTS: \result == nowlocation[num];
     */
    public synchronized int[] getnls(int num) {

        return nowlocation[num];
    }

五、bug在方法上的聚焦

方法名	功能bug	规格bug
readmap	1	1
Scheduler	2	0

 

 

 

 

功能bug分析：这几次的bug主要集中在两方面，一个是读文件时如果没有考虑恰当，会因为各种各样奇怪的原因crash，第二个就是线程安全，之前因为没有用多线程处理调配，所以一直没法正确处理同质请求，这次新加了多线程调配，却疏忽了以前的一些问题，比如在gui里要给计算路径的方法加锁，还有要给托盘类里的静态信息加锁。

六、撰写规格的心得体会

其实在这几次作业中，我一直没想明白规格对于代码的重要性，因为第一次接触，又要使用布尔表达式，很多能用自然语言表述的情况不能用布尔表达式表达，但是在上周的oo课上测试中我发现了对于书写规范详尽的规格我可以通过规格补全方法，我才深刻认识到原来书写规范的规格可以让阅读者方便快捷地知道代码的功能，更好地使用代码，这种设计思想值得我们学习。