1960年代末—1970年代初，出现软件危机：对软件系统的大量需求与软件的研制周期长，可靠性差，维护困难的现实情况形成矛盾。于是人们希望编写出的程序结构清晰、易阅读、易修改、易验证，即得到好结构的程序。1968年，北大西洋公约组织召开第一次软件工程会议，分析了危机的局面，研究了问题的根源，第一次提出了用工程学的办法解决软件研制和生产的问题。

　　与此同时，许多学者也从结构化程序设计、程序正确性验证等方面展开了规格化设计的研究。Dijkstra 提出了“GOTO是有害的”，希望通过程序的静态结构的良好性保证程序的动态运行的正确性。Hoare提出了基于“前置后置条件”的接口规格方法。D.Gries综合了以谓词演算为基础的证明系统，首次把程序设计从经验、技术升华为科学。

　　规格化设计带来了许多好处。它使得软件开发过程变得更成熟，能更好地保证软件质量。而且使得团队协作开发更加可行，分工更为明确。所以人们非常重视。

规格bug

产生原因：

　　Requires不完整的两个错误原因：其一是在写被改变的变量的时候，类变量一多，混杂在临时变量之间就容易被忘记。第二是对参数要求的时候容易想不清楚。比如说存地图时，在输入处理环节就已经保证不会传入非法的参数，所以在存的这一步我没有对传入变量进行要求，但事实上应该要求的。我们不能提前预知到前方已经做过处理了，因此要施加我们的要求，好让前方的处理按照我们的规格进行处理。

　　Effects不完整是因为忘了写抛出异常。通过这几次互策 互测，及OO上机代码，我发现大家都有着很好的异常处理，不像我想到了就给方法加个try catch。他们的异常处理很方便定位错误位置，且逻辑性很好，学到了。

前置条件不好的写法

公开处刑1　

public void runLess(Point from, Point to){
    　　/** @REQUIRES: 起点from，终点to
        ……
        */
        ……
        
        from.method();
        to.method();
    
        ……
}

　　用自然语言来写前置条件，为了表达同样的意思需要更多笔墨。此处的Requires需对from,to进行约束，因为函数体内部运用了对象的方法。所以写成下面这样更简洁更明确。

/** @REQUIRES: from != null && to != null;

公开处刑2

public synchronized boolean judge(Passenger p) {
        /**@REQUIRES: p!=null && 0<=p.getCurrentX<80 && 0<=p.getCurrentY<80
　　　　　　　　&& 0<=p.getDestinationX<80 && 0<=p.getDestinationY<80;
        * @THREAD_EFFECTS: locked();
        */
}

　　这和我之前想不清楚的地方一样：我要对这个对象约束多深？比如：如果传入参数是一个ArrayList，我是否在保证其不为null的情况下还要保证内部元素不为null；如果是ArrayList<Taxi>的话是否还要检查元素为Taxi类型，是否还要检查Taxi的内部参数满足要求。现在我觉得不需要约束这么多，应交给别的地方来保证这些。例如在Passenger的构造方法中对乘客的坐标进行约束。所以此处写 p != null; 就够了。

　　没法写5个案例，因为我的前置条件不是在约束数字范围就是在限制不能为空。

后置条件不好的写法

 公开处刑1

public synchronized boolean isSame(Passenger p) {
        /**@REQUIRES: requestList != null && p != null;
        * @EFFECTS :
        *    
esult == requestList.contains(p);
        * @THREAD_EFFECTS: locked();
        */
        遍历requestList并根据Passenger的实例变量来判断是否同质
    }

　　这个写的不好的地方在于同质的话，就存在一个和p在时间、当前坐标、将要去的地方完全一样的对象，但这个对象和我传入的对象并不是一个对象，所以这种写法不好。但感觉很难改进，只能自己写一个contains的方法来保证这个Effects。

公开处刑2

public static void main(String[] args) {
        /** @EFFECTS: 
         * 启动xx线程，启动xx线程，启动xx线程
        */

　　Effects应该描述方法结束后系统的变化。在main方法开始前，这些线程还未出生，main结束的时候又一波带走了他们，所以main的Effects内只需写对类变量的改变就行了。

　　*如果一个方法调用了很多别的方法，我要对这个方法的效果描述到多深是一个困扰着我的问题。

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

　　没有什么关系。

　　因为不是先写规格再写功能的。

　　规格出问题的功能都没问题。反之亦然。

其他

　　这三次体验很不好，很影响我心情，遇到了好的测试者、被测试者，但所有的好心情也敌不过一次坏心情。尤其是最后一次吧，终于见到了OO课程被大家诟病的问题了。但他人恶意来面对我，我如果还将恶意传递出去，岂不是也成了恶人了吗。有什么必要呢，分数拿走便是了，我应该关注如何把代码写的更严密，挑不出瑕疵，关掉网站页面。