zoukankan      html  css  js  c++  java
  • OO第三次单元总结

     一、规格化设计发展历史 

      软件规格化方法,最早可追溯到20世纪50年代后期对于程序设计语言编译技术的研究,当时出现了各种语法分析程序自动生成器以及语法制导的编译方法,使编译系统的开发从“手工艺制作方式”发展成具有牢固理论基础的系统方法。规格化设计的研究高潮始于20世纪60年代后期,针对当时所谓的“软件危机”,人们提出种种解决方法,如采用工程方法来组织、管理开发过程和通过钻研规律建立严密的理论以指导开发实践。

      经过30多年的研究和应用,如今人们在规格化设计取得了大量、重要的成果,从早期最简单的一阶谓词演算到现在应用于不同领域、不同阶段的基于逻辑、状态机、网络、进程、代数等众多规格形式化方法,它的发展趋势是逐渐融入设计开发的各个阶段,从需求分析、功能描述、算法设计、编程、测试直到维护。

      规格化设计对代码的创作者和使用者都有重要的作用。对于编程者,规范的设计有助于架构的建立和调整,有助于完善修正细节,有助于未来的维护和扩展;对于使用者,规格化的呈现有助于理解剖析,避免不必要的误解和分歧,同时也利于高效的阅读和学习。

     二、bug分析 

      

      三次作业总共被报了四个规格bug,很遗憾的是其中有三个都是“忘记写了”……emm反思一下第十次可能和赶时间有关,但是第十一次在时间蛮充裕的情况下就真的是粗心没检查的锅。另外一个关于repOK的bug,我觉得测试者说的很有道理。因为在原来的repOK方法中,只要出现了对象型的变量我一律用“!=null”来处理,但是想想每个对象的类中也有它自己的repOK,理应传承下来,只有满足了所有的repOK才能说明科学合理性。

      

      虽然从表格上看,功能bug与规格bug确实没有重合的地方,但是这并不意味着两者就毫无关联。两次作业中功能出现的问题集中在input、run、randomdrive这些代码规模较大,逻辑较复杂的方法中,本身规格就很难概括,只能借助自然语言的帮助,加上关键步骤的布尔表达式来描述。由于规格无法涵盖细小逻辑,很难体现出错误疏漏,或者换一种说法,书写规格没有起到应有的作用,所以从报告bug的角度,就看不出联系了。

     三、规格改进示例 

    • 前置条件  
    /**
         * @REQUIRES:
         *         0<=index<=6399;
         * @MODIFIES:None;
         * @EFFECTS:
         *         normal_behavior:
         *            !(exist int next;map.reachlist[index].contains(next)) ==> 
    esult==index;
         *             在index的可达节点中随机选取一个两点之间边流量最小的节点next.
         *             
    esult==next;
         *         exception_behavior(Exception e): 
         *             
    esult==index;
      */

                                   

    /**
         * @REQUIRES:
         *         0<=index<=6399;
         *         0<=oldindex<=6399;
         * @MODIFIES:None;
         * @EFFECTS:
         *         normal_behavior:
         *            !(exist int next;map.reachlist[index].contains(next)) ==> 
    esult==index;
         *             在index的可达节点中随机选取一个两点之间边流量最小的节点next.
         *             
    esult==next;
         *         exception_behavior(Exception e): 
         *             
    esult==index;
      */

    ······································································································································

    /**
         * @REQUIRES:
         *         0<=start<=6399;
         *         0<=end<=6399;
         *         0<=flow<=100;
         * @MODIFIES:
         *         	his.flow;
         * @EFFECTS:
         *         	his.flow[start][end]==flow;
         *         	his.flow[end][start]==flow;
      */

                                   ↓

    /**
         * @REQUIRES:
         *         0<=start<=6399;
         *         0<=end<=6399;
         *         distance from start to end is 1.
         *         0<=flow<=100;
         * @MODIFIES:
         *         	his.flow;
         * @EFFECTS:
         *         	his.flow[start][end]==flow;
         *         	his.flow[end][start]==flow;
      */

    ······································································································································

    /**
         * @REQUIRES:
         *         0<=index<=6399;
         *         0<=next<	his.reachlist[index].size();
         * @MODIFIES:None;
         * @EFFECTS:
         *         type==0 ==> 
    esult==	his.reachlist[index].get(next);
         *         type==1 ==> 
    esult==	his.initreachlist[index].get(next);
      */

                                   ↓

    /**
         * @REQUIRES:
         *         0<=index<=6399;
         *         0<=next<	his.reachlist[index].size();
         *         type==0 || type==1;
         * @MODIFIES:None;
         * @EFFECTS:
         *         type==0 ==> 
    esult==	his.reachlist[index].get(next);
         *         type==1 ==> 
    esult==	his.initreachlist[index].get(next);
      */

    ······································································································································

    /**
         * @REQUIRES:None;
         * @MODIFIES:None;
         * @EFFECTS:
         *         (r's time,start_x,start_y,end_x,end_y are equal to this's) ==> 
    esult==true;
         *         !(r's time,start_x,start_y,end_x,end_y are equal to this's) ==> 
    esult==false;
      */

                                   ↓

    /**
         * @REQUIRES:
         *         r!=null;
         * @MODIFIES:None;
         * @EFFECTS:
         *         (r's time,start_x,start_y,end_x,end_y are equal to this's) ==> 
    esult==true;
         *         !(r's time,start_x,start_y,end_x,end_y are equal to this's) ==> 
    esult==false;
      */

    ······································································································································

    /**
         * @REQUIRES:None;
         * @MODIFIES:None;
         * @EFFECTS:
         *         
    esult==	his.inputs.get(i).start_x;
      */

                                   ↓

    /**
         * @REQUIRES:
         *         0<=i<	his.inputs.size();
         * @MODIFIES:None;
         * @EFFECTS:
         *         
    esult==	his.inputs.get(i).start_x;
      */

    ······································································································································

    • 后置条件  
    /**
         * @REQUIRES:None;
         * @MODIFIES:
         *         	his.credit;
         * @EFFECTS:
         *         	his.credit==	his.credit+1;
      */

                                   ↓

    /**
         * @REQUIRES:None;
         * @MODIFIES:
         *         	his.credit;
         * @EFFECTS:
         *         	his.credit==old(	his.credit)+1;
         */

    ······································································································································

    /**
         * @REQUIRES:
         *         req!=null;
         * @MODIFIES:None;
         * @EFFECTS:
         *         
    esult == request in inputs that equals req ;
         */

                                   ↓

    /**
         * @REQUIRES:
         *         req!=null;
         * @MODIFIES:None;
         * @EFFECTS:
         *         
    esult == (exist Request r; inputs.contains(r);r.equals(req));
         * @THREAD_REQUIRES:
         *         locked(	his);
         * @THREAD_EFFECTS:
         *         locked();
         */

    ······································································································································

    /**
         * @REQUIRES:
         *         req!=null;
         * @MODIFIES:
         *         	his.inputs;
         * @EFFECTS:
         *         	his.inputs.contains(req) ;
         * @THREAD_REQUIRES:
         *         locked(	his);
         * @THREAD_EFFECTS:
         *         locked();
         */

                                   ↓

    /**
         * @REQUIRES:
         *         req!=null;
         * @MODIFIES:
         *         	his.inputs;
         * @EFFECTS:
         *         	his.inputs.contains(req) && 	his.inputs.size()=old(	his.inputs).size()+1;
         * @THREAD_REQUIRES:
         *         locked(	his);
         * @THREAD_EFFECTS:
         *         locked();
         */

    ······································································································································

    /**
         * @REQUIRES:None;
         * @MODIFIES:
         *         	his.reachlist;
         *         	his.initreachlist;
         * @EFFECTS:
         *         	his.reachlist == new Vector<Integer>();
         *         (all Vector x;reachlist.contains(x);x!=null);
         *         	his.initreachlist == new Vector<Integer>();
         *         (all Vector x;initreachlist.contains(x);x!=null);
         */

                                   ↓

    /**
         * @REQUIRES:None;
         * @MODIFIES:
         *         	his.reachlist;
         *         	his.initreachlist;
         * @EFFECTS:
         *         	his.reachlist!=null;
         *         (all Vector x;reachlist.contains(x);x!=null);
         *         	his.initreachlist!=null;
         *         (all Vector x;initreachlist.contains(x);x!=null);
         */

    ······································································································································

    /**
         * @REQUIRES:None;
         * @MODIFIES:None;
         * @EFFECTS:
         *         
    esult==queue!=null && inputs!=null && taxigui!=null && outFile!=null && taxis!=null && taxiInfo!=null && map!=null;
         */

                                   ↓

    /**
         * @REQUIRES:None;
         * @MODIFIES:None;
         * @EFFECTS:
         *         
    esult==queue!=null &&  inputs!=null && taxigui!=null && outFile!=null && taxis!=null && taxiInfo!=null && map!=null && queue.repOK() && inputs.repOK() && (all Taxi t;taxis.contains(t);t.repOK()) && map.repOK();
         */

    ······································································································································

     四、思路与体会 

      由于出租车的框架是在第七次作业时搭建好的,后面基本没有做出大的变动,所以大部分的规格是看着方法补充。前置条件就从传入的参数入手,基本类型需要判断在指定范围内,对象类型则要求不为空。中间条件抓住本类的类变量,逐一检查是否在此方法中被改变。后置条件比较复杂,需要兼顾条件判断、数组遍历、返回值、类变量前后改变等,如果是逻辑太多的方法就只能挑出关键步骤,借助自然语言描述。

      不同的遭遇,不同的体会。在三次作业的互测过程中,测试者并没有死抠我的规格细节,扣的分主要是因为自己的粗心大意,所以在承受范围之内。至于书写规格的体会,由于没有做到像老师在课堂上说的 “先写规格后写代码”,整个过程可以说是“重温方法思路,再按规定格式翻译一遍”。虽然体验效果有些欠佳,但依然不能否认规格化设计的重要性。在真正的工程化编程中,规格的确有提高效率,减少出错的作用。同时我也认为,“规格化”不仅仅是贯彻体现在方法前的几行JSF注释中,更重要的是从构想到实施的过程,真正具有 “规格化”的思想。

  • 相关阅读:
    使用blend制作地图区域改变颜色动画效果
    使用Win32创建串口通讯程序[转]
    ArcGIS的网络分析【转】
    推荐10款非常优秀的 HTML5 开发工具[转]
    Win32串口编程(转:韩耀旭)
    软件项目版本号的命名规则及格式介绍【转】
    [ArcGIS+Win7][转]安装ArcGIS后打开"打开或关闭 Windows 功能"一片空白解决方案
    js判断客户端是否安装了activex控件[转帖]
    纪念失去的爱情(抒情诗)
    委托事件之买烟
  • 原文地址:https://www.cnblogs.com/wjy21/p/9103151.html
Copyright © 2011-2022 走看看