面向对象第三次总结性博客

写在前面

　　这几次作业主要以JSF规格化设计为主，检验了大家规格的书写能力。而主观上的JSF扣分也将参与课程者分成了两种人，有认真扣分的“太空人”，也有将心比心的好心人。前者可以在JSF上拿到满意的分数，后者可能会被“太空人”扣去很多分数。

　　但终归结底的是，JSF规格书写还是蛮屌的。我是无法将我的类书写成无法被找错的格式，所以在对他人的扣分中我也只是把十分明显的错误按类别扣分了，幸运的是，我也没有在JSF互测中损失很多分数。

　　好了，接下来该进入正题了，下面我将从以下几点来完成这次博客：

　　(1)调研，然后总结介绍规格化设计的大致发展历史和为什么得到了人们的重视

　　(2)按照作业，针对自己所被报告的规格bug以及雷同的规格bug（限于bug树的限制，对手无法上报），列一个表格分析规格bug类别（采用bug树上的名称）、每个出现所对应方法的代码行数

　　(3)分析自己规格bug的产生原因

　　(4)分别列举5个前置条件和5个后置条件的不好写法，并给出改进写法

　　(5)按照作业分析被报的功能bug与规格bug在方法上的聚集关系

　　即给出表格：方法名、功能bug数、规格bug数

　　(6)归纳自己在设计规格和撰写规格的基本思路和体会。

一、总结调研

规格发展史

　　程序设计的演变大致可以分成以下三个过程：

　　1. 20世纪60年代以前，计算机刚刚投入实际使用，软件设计往往只是为了一个特定的应用而在指定的计算机上设计和编制，采用密切依赖于计算机的机器代码或汇编语言，软件的规模比较小，很少使用系统化的开发方式，此时的代码更多的是私人性质的，满足个人要求的程序

　　2. 60年代中期，大容量、高速度的计算机出现，随之出现的是代码量急剧提升，复杂度急剧增长、程序可靠性问题突出的问题。结果化程序设计随之提出，它要求程序设计时以模块为单位，每个模块专职自己的工作，而要在模块间交流，在开发者和用户，开发者和开发者之间交流，就只需要相应接口即可；

　　3. 80年代，面向对象的设计开始在业界大行其道，相比于单纯的结构化设计，面向对象的设计从审视问题的角度上就有了差异，程序发生了从围绕“行为”执行到围绕“客体”执行的变化，随之而来的，就是封装性地提高，可重用性的提高，可以说，面向对象进一步实现了结构化设计，是结构化设计更进一步的实现。说明是类型定义和操作描述，体是操作的具体实现。（具体的例子就是C++,Java等面向对象语言的类说明与类实现的分离。）解决方案设计只关注说明，实现时引用或者设计体。体的更改、置换不影响规格说明，保证了可移植性。支持多机系统，但要同样环境。此时产生了划时代的面向对象技术。在结构化越加明确的同时，开发者与设计者，开发者与用户，开发者与开发者之间的交流，就需要“抽象”来实现，因为彼此间不需要关心对方的实现方法，而只需要知道这个模块的接口有什么要求，会改什么，能做什么就行。通过规格化抽象，我们就能将这种交流变得高效，同时也降低了维护和修改的难度。

　　4.基于构件开发：标准化的软件构件如同硬件IC，可插拔，使用者只用外特性，不计内部实现。Web Services：软件就是服务。分布式，跨平台，松耦合。

规格很重要

　　在大型项目的开发中，单个项目不可能由一个人完成。多人协作共同完成任务就意味着不仅仅需要知道自己的代码做了什么，还要知道别人的代码做了什么。

　　别人永远不知道你的代码是要做些什么，只有通过规格化这样子别人才看的懂。别人通过你的规格知晓你类中各个方法的功能，然后当他用的时候就了然于心了。

　　这种规格化设计在项目开发中能明显提高效率，是很顺滑的润滑剂。　

二、规格bug分析

第九次作业

Modifies不完整	9行：* @EFFECTS : esult== a;
Requires逻辑错误	1行：* @REQUIRES: i!=null;

　　第一个错误是因为对面类别报错了，这里的a是一个临时变量，所以对于a并没有任何Modifies。

　　第二个错误是因为i是整型变量，当初依样画葫芦，犯错了。

第十次作业

JSF不符合规范

n行：repOk没有写JSF

　　错误的原因是当初写repOK操之过急，殊不知也要写JSF方法，知道之后立即改正了自己的错误。

第十一次作业

Modifies逻辑错误

30行：* @MODIFIES : this.graph;

　　错误的原因是Map类中的都是static属性，所以不能用this.graph,要用Map.graph。扣我的人和我说这是上次他被扣的，我也能理解，也学习到很多。

三、规格改进方案（前置后置）

前置1：对传入的参数应该有前置条件

//错误示范
    /**
    * @REQUIRES : None;
    * @MODIFIES : this.timeGap;
    * @EFFECTS : this.timeGap==timeGap;
    */
    lightControl(long timeGap)
    {
        this.timeGap = timeGap;
    }
//正确写法
    /**
    * @REQUIRES : timeGap>0;
    * @MODIFIES : this.timeGap;
    * @EFFECTS : this.timeGap==timeGap;
    */
    lightControl(long timeGap)
    {
        this.timeGap = timeGap;
    }

前置2：“=”应该为“==”

    //错误示范    
    /**
      *@REQUIRES:status!=null,staus=TAKING||staus=WAITING||staus=SERVING||staus=STOP;
        *@MODIFIES: this.status;
        *@EFFECTS: 
        *        status==status;
        */    
    public void SetStatus(TaxiStatus staus){
        this.status=s;
    }
    //正确写法
    /**
        *@REQUIRES: staus!=null,staus==TAKING||staus==WAITING||staus==SERVING||staus==STOP;
        *@MODIFIES: this.status;
        *@EFFECTS: 
        *        status==staus;
        */    
    public void SetStatus(TaxiStatus staus){
        this.status=staus;
    

前置3：前置条件应该是布尔表达式

//错误示范
/**
     * @REQUIRES: index is from 0 to 100;
     * @MODIFIES:this.index; 
     * @EFFECTS: this.index == index;
     */
    public TaxiCar(int index) {     
        this.index = index;
    }
//正确写法
/**
     * @REQUIRES: 0<=index<100;
     * @MODIFIES:this.index; 
     * @EFFECTS: this.index == index;
     */
    public TaxiCar(int index) { 
        this.index = index;
    }

前置4：对于数字类型判断问题

//错误示范
/**
    *@REQUIRES:index!=null;
    *@EFFECTS: 
    *        
esult==wc[inidex];
*/    
    public Taxi get(int inidex){
        return this.wc[inidex];
    }
//正确写法
/**
    *@REQUIRES: inidex!=null，0<=inidex<=99;
    *@EFFECTS: 
    *        
esult==wc[inidex];
    */    
    public Taxi get(int inidex){
        return this.wc[inidex];
    }

前置5：括号问题

//错误示范
/**
     * @REQUIRES: req != null && index >= 80 || index < 0;
     * @MODIFIES: this.req; this.index;
     * @EFFECTS: this.req == req; this.index; 
     */
    public Record(Request req, int index) {
        this.req = req;
        this.index = index;
    }
//正确写法
/**
     * @REQUIRES: req != null && (index >= 80 || index < 0);
     * @MODIFIES: this.req; this.index;
     * @EFFECTS: this.req == req; this.index; 
     */
    public Record(Request req, int index) {
        this.req = req;
        this.index = index;
    }

后置1：缺少线程规格

//错误示范 
       /**
        *@MODIFIES: System.out;
        *@EFFECTS: 
        *        true==>(do the things below in an endless loop)==>(wait())==>(dispatch());
        */    
    public void run(){
        while(true){
            try {
                synchronized(this.MS){
                    this.MS.wait();
                    this.dispatch();
                }
                //System.out.println(System.currentTimeMillis());
            } catch (Throwable e) {
                System.out.println("Error in Scheduler");
                System.exit(0);
            }
        }
    }
//正确写法
        /**
        *@MODIFIES: System.out;
        *@EFFECTS: 
        *        true==>(do the things below in an endless loop)==>(wait())==>(dispatch());
        *@THREAD_EFFECTS: this.MS;
        */    
    public void run(){
        while(true){
            try {
                synchronized(this.MS){
                    this.MS.wait();
                    this.dispatch();
                }
                //System.out.println(System.currentTimeMillis());
            } catch (Throwable e) {
                System.out.println("Error in Scheduler");
                System.exit(0);
            }
        }
    }

后置2："="应该写成"=="

//错误示范
    /**
    * @EFFECTS : 
esult = Main.time;
    */
    public synchronized long getTime(int num)
    {
        return Main.time;
    }
//正确写法    
        /**
    * @EFFECTS : 
esult== Main.time;
    */
    public synchronized long getTime(int num)
    {
        return Main.time;
    }    

后置3：未处理异常

//错误示范
/**@ EFFECTS:   
esult == min a;
*/
public static int min (int[ ] a) throws NullPointerException, EmptyException 
//正确写法
/**@ EFFECTS:   normal_behavior
                
esult == min a;
(a == null) ==> exceptional_behavior (NullPointerException);
(a.length == 0) ==> exceptional_behavior (EmptyException);
*/
public static int min (int[ ] a) throws NullPointerException, EmptyException 

后置4：后置条件遗漏修改变量

//错误示范
    /**
    * @MODIFIES : this.Credit,this.pos,this.status;
    * @EFFECTS : this.Credit==Credit;
    * this.pos.x==x;
    * this.pos.y==y;
    */
    public void setTaxi(int Status,int Credit,int x,int y)
    {
        this.Credit =Credit;
        this.pos.setLocation(x, y);
        this.status  = TaxiStatus.WFS;
    }
//正确写法
    /**
    * @MODIFIES : this.Credit,this.pos,this.status;
    * @EFFECTS : this.Credit==Credit;
    * this.pos.x==x;
    * this.pos.y==y;
    * this.status==TaxiStatus.WFS;
    */
    public void setTaxi(int Status,int Credit,int x,int y)
    {
        this.Credit =Credit;
        this.pos.setLocation(x, y);
        this.status  = TaxiStatus.WFS;
    }

后置5：后置条件描述不完整

//错误示范
/**
     * @REQUIRES : None; 
     * @MODIFIES : this.AskList;
     * @EFFECTS : AskList.contains(ask);
     */
    public synchronized void addAsk(Ask ask){
        AskList.add(ask);
    }
//正确写法
/**
     * @REQUIRES : None; 
     * @MODIFIES : this.AskList;
     * @EFFECTS : AskList.contains(ask) && AskList.size == old(AskList).size + 1;
     */
    public synchronized void addAsk(Ask ask){
        AskList.add(ask);
    }

四、功能BUG与规格BUG的聚焦关系

作业	功能BUG数量	规格BUG数量	聚焦关系
第九次	2	2	无
第十次	2	1	无
第十一次	2	1	无

 　　从bug数无法明显地看到功能BUG和规格BUG的联系。但我认为这两者一定有着某种意义上的联系，好的规格设计一定是在深思熟虑之后，这也就会相应地减小功能BUG。而且如果被发现规格BUG，那一定是设计者在设计时的欠缺，可能就可以因此而找到他的功能BUG。

四、感想与体会

　　在撰写JSF的过程中，有很多地方都不知道怎么写，但也就这样写下来了，可能是自己的经验不足，虽然有写的比较好的地方，但仍有多处欠缺。希望OO课程交给我的工程化设计模式与规格撰写可以对我之后的程序员之路有所帮助。

　　OO之旅临近尾声，希望自己可以继续坚持，为OO之旅画上好的句号。