OO第三次作业总结

时间：2021-07-01 21:54:47

第三次作业总结

规格化的发展 为什么得到了人们的重视

规格设计用于对程序设提供分解，抽象等的手段。在撰写代码规格的时候，需要对组成部件进行抽象。

在1960s，软件设计出现危机，例如Dijkstra提出了goto语句的种种危害，引发了软件开发领域长期的论战，并且在这时候产生了结构化程序设计方法，例如Pascal语言在1970s占据有统治地位。

之后，随着计算机软件规模日渐庞大，结构化程序设计方法开始无法满足用户的需求，面向对象程序设计（OOP）应运而生。面向对象程序设计是一场重大的革命，提高了开发人员的效率，有效的控制了软件开发的复杂度，提高了软件的可维护性和可拓展性。

规格化设计是随着面向对象程序设计的火热而发展起来的，可以有效提高程序的规范性以及程序的模块化划分。这样使得程序设计的数据更加安全，软件的可维护性得到有效的提高。

规格化设计之所以能够受到软件开发人员的重视，主要是因为它能大幅度提高软件工程的质量。例如在大型软件开发中，随着时间的推移可能有越来越多的新功能被要求添加，但是随意修改代码会造成代码的不可靠，只有用抽象与规格的方法设计程序，才能保证代码的高可靠性与易维护性。规格实际上是一种契约化编程手段，将代码的功能进行抽象，使设计人员无需关注代码实现的细节，从而提高设计效率与正确性。

规格bug分析

没被报规格bug。

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

由于没有被报规格bug，分析不出原因。

优劣JSF示例

  • 前置条件（前者为写的不好的前置条件，后者为修改后）
//前置条件需要使用布尔表达式
boolean insert(Account a){
  /**
 * @ REQUIRES: a 非空；
 */
}
boolean insert(Account a){
   /**
 * @ REQUIRES: a!= null ;
 */ 
}
//没有对输入条件进行约束
synchronized int getDistance(int x1, int y1, int x2, int y2){
    /**
 * @REQUIER : x1, y1, x2, y2
 */
}
synchronized int getDistance(int x1, int y1, int x2, int y2){
    /**
 * @REQUIER : 0 <= x1, y1, x2, y2 < 80
 */
}
//将@REQUIRE理解成了该方法中的条件语句
void openWay(int x1, int y1, int x2, int y2){
    /**
 * @REQUIRE : x1 == x2 且 y1 == y2 - 1 且 (x1,y1)到(x2,y2)有路
 * 或 x1 == x2 且 y1 == y2 + 1 且 (x1,y1)到(x2,y2)有路
 * 或 x1 == x2 - 1 且 y1 == y2 且 (x1,y1)到(x2,y2)有路
 * 或 x1 == x2 + 1 且 y1 == y2 且 (x1,y1)到(x2,y2)有路
 */
}
void openWay(int x1, int y1, int x2, int y2){
    /**
 * @REQUIRE : 0 <= x1, y1, x2, y2 < 80
 */
}    
//遗漏了某些条件
synchronized int getDistance(int x1, int y1, int x2, int y2){
    /**
 * @REQUIER : 0 <= x1, y1 <= 79
 */
}
synchronized int getDistance(int x1, int y1, int x2, int y2){
    /**
 * @REQUIER : 0 <= x1, y1, x2, y2 <= 79
 */
}
//将该方法内的临时变量写进了@REQUIRE
Taxi chooseTaxi() {
    /**
 * @REQUIRE : competitive != null, bestTaxi != null, bestTaxi.getState() != wait, 100 > start >= 0
 * @MODIFIES : start, bestTaxi, 调用了write函数，要往文件里写相应的内容
 * @EFFECT : 返回选出的最合适该条请求的出租车并且返回
 */
    Taxi bestTaxi = null;
    int start = 0;
    while(bestTaxi == null || bestTaxi.getState() != State.wait){
        bestTaxi = competitiveMap[start];
        start ++;
        if(start == 100){ break; }
    }
    ......
    return bestTaxi;
}
Taxi chooseTaxi() {
    /**
 * @REQUIRE : competitive != null, bestTaxi != null, bestTaxi.getState() != wait
 * @MODIFIES : start, bestTaxi, 调用了write函数，要往文件里写相应的内容
 * @EFFECT : 返回选出的最合适该条请求的出租车并且返回
 */
    Taxi bestTaxi = null;
    int start = 0;
    while(bestTaxi == null || bestTaxi.getState() != State.wait){
    bestTaxi = competitiveMap[start];
    start ++;
    if(start == 100){ break; }
    }
    ......
    return bestTaxi;
}
  • 后置条件
//未说明异常情况
synchronized void write(String str){
    /**
 * @EFFECTS : 往文件内写入了str信息
 */
}
synchronized void write(String str){
    /**
 * @EFFECTS :
 * normal behavior:
 * 往文件内写入了str信息
 * io出现异常（读取文件出现异常） ==> exceptional_behavior (e);
 */
}
//逻辑不完整
Account queryByAccountId(String accountId) throws InvalidOperationException {
   /**
 * @ REQUIRES: accountId!= null ;
 * @ EFFECTS: 
 * (\result==a)==>(\all Account a;(\this.contains(a)==true)&&a.getAccountId()==accountId);
 */
   for(Account a: accounts){
           if(a.getAccountId().equals(accountId)){
               return a;
           }
       }
       throw new InvalidOperationException("Invalid Account");
   }   
Account queryByAccountId(String accountId) throws InvalidOperationException {
   /**
 * @ REQUIRES: accountId!= null ;
 * @ EFFECTS: 
 * (\result==a)==>(\all Account a;(\this.contains(a)==true)&&a.getAccountId()==accountId);
 * (\all Account a;a.getAccountId()==accountId && (\this.contains(a)==false))==>exceptional_behavior("Invalid Account!") ;
 */
   for(Account a: accounts){
           if(a.getAccountId().equals(accountId)){
               return a;
           }
       }
       throw new InvalidOperationException("Invalid Account");
   }   
//遗漏了某些细节上的变化，比如accounts的长处增加了1
   boolean insert(Account a){
   /**
 * @ REQUIRES: a!= null ;
 * @ MODIFIES: this;
 * @ EFFECTS: 
 * (\result==false)==>(\old(\this).contains(a)==true)
 * (\this.contains(a)==true)&&(\result==true); 
 */
   if(isIn(a)){
           return false;
       }else {
           accounts.add(a);
           return true;
       }
   } 
   boolean insert(Account a){
   /**
 * @ REQUIRES: a!= null ;
 * @ MODIFIES: this;
 * @ EFFECTS: 
 * (\result==false)==>(\old(\this).contains(a)==true)
 * (\this.size == \old(\this).size+1) && (\this.contains(a)==true)&&(\result==true); 
 */
   if(isIn(a)){
           return false;
       }else {
           accounts.add(a);
          // System.out.println(a + " is add in the list");
           return true;
       }
   }

功能bug和规格bug分析

只有功能bug，无法做出聚集上的分析。

设计规格思路和体会

  • 明确执行前对输入或系统状态的约束要求；

  • 将这些约束条件用布尔表达式表示出来，并再次检查逻辑正确性；

  • 明确方法在执行过程会对哪些用户能够感知到的数据进行修改，例如：对this的修改、对传图对象的修改，对环境对象的修改、对全局便量的修改；

  • 明确执行返回结果或系统状态应该满足的要求，分清正常结果、异常结果；

体会： 我到现在都还无法切身感受到规格化给我带来的非一般的感觉； 希望在今后的使用中能感受到。

标签：

相关文章