OO第三次博客

規格化設計的發展歷史

　　在計算機的早期發展中，軟件開發沒有能夠遵循的系統方法，每每只有源代碼而沒有軟件說明書等文檔，所以這段時期的軟件通用性時頗有限的。後來到了20世紀60年代，軟件開始被普遍使用，軟件開發依然沒有規範化，而軟件的需求也愈來愈複雜，使得程序維護難度大大增長。爲了解決這一難題，人們認真思考後造成了新的程序開發要求：即程序除了擁有良好的性能和正常的功能外，還應該具備良好的可讀性的可拓展性，並易於後期的維護。1968年北約軟件工程大會上提出來軟件工程的概念。以後廣泛開始關注軟件開發過程的研究，在這期間肯定了一系列重要的文檔規範，這些規範在後來的發展中造成了軟件開發之中的規格化設計。

　　規格化設計做爲一種契約化編程手段，它要求開發者使用抽象和規格的方法設計程序，保證了程序的易維護性、高效性以及可拓展性，對於大型的軟件開發大有裨益，所以受到了人們的重視。

做業BUG分析

　　三次做業都沒有被報規格bug。

五個很差的前置條件和後置條件寫法以及改進

 　　1 五個很差的前置條件寫法以及改進：

　　　　a)前置條件考慮不充分，未對allTaxi數組內元素加以限制。

Input(Queue reqs,TaxiGUI gui,Map map,Taxi[]allTaxi){
            /** 
             * @REQUIRES:
             *      reqs!=null;
             *      gui!=null;
             *      map!=null;
             *      allTaxi!=null;

　　　　改進寫法：

Input(Queue reqs,TaxiGUI gui,Map map,Taxi[]allTaxi){
            /** 
             * @REQUIRES:
             *      reqs!=null;
             *      gui!=null;
             *      map!=null;
             *      allTaxi!=null;
             *      (\all int i;0<=i<=99;allTaxi[i]!=null);

　　　　b)使用天然語言。

public void openFile(String name) {
           /**
            * @REQUIRES:文件存在

　　　　改進寫法：

public void openFile(String name) {
         /**
            * @REQUIRES:FILE(name).exists==true;    

　　　　c)未對參數取值範圍加以限制。

synchronized void setStatus(int status) {
        /**
         * @REQUIRES:status!=null;

　　　　改進寫法：

synchronized void setStatus(int status) {
        /**
         * @REQUIRES:status!=null;
         *           status==0||status==1||status==2||status==3;

　　　　d)未考慮數組爲null的狀況。

synchronized Request removeFirst() {
        /**
         * @REQUIRES:None;

　　　　改進寫法：

synchronized Request removeF() {
        /**
         * @REQUIRES:this.reqQueue!=null;

　　　　e)冗餘的前置條件（方法內對文件路徑不存在的狀況做了相應的處理，所以沒必要再前置條件中加以限制）。

public void mapLoader(String fileName) {
        /**
         * @REQUIRES:File(fileName).exist;

　　　　改進寫法：

public void loading(String fileName) {
        /**
         * @REQUIRES:None;

　　2 五個很差的後置條件寫法以及改進：

　　　　a)使用天然語言。

public static void fileWriter(String file,String str){
        /**
         * @REQUIRES: 
         *         file！=null;
         *         File(file).exist;      
         * @MODIFIED:  File(file);
         * @EFFECTS:  write str to end of File(file);
         */

　　　　改進寫法：

public static void fileIn(String fileName,String str){//寫字符串str寫到文件File(fileName)中
        /**
         * @REQUIRES: 
         *         File(fileName).exist==true;      
         * @MODIFIED:  File(fileName);
         * @EFFECTS:  File(fileName)!=\old(File(fileName));
         */

　　　　b)後置條件爲布爾表達式，不該用‘=’。

 public boolean getArrived(){
         /**
             * @REQUIRES:None;
             * @MODIFIES:None;
             * @EFFECTS:\result=this.arrived;
             */

　　　　改進寫法：

 public boolean getArrived(){
         /**
             * @REQUIRES:None;
             * @MODIFIES:None;
             * @EFFECTS:\result==this.arrived;
             */

　　　　c)後置條件表述不清晰。

void setReachable() {
        /**
         * @REQUIRES:
         *         map!=null;
         * @MODIFIES:
         *      \this.reachable;
         * @EFFECTS:
         *      (\all point p;point q.reaches(q)||p.reaches(q);reachable[p.x][p.y].contains(q);
         */

　　　　改進寫法：

void setReachable() {
        /**
         * @REQUIRES:
         *         map!=null;
         * @MODIFIES:
         *      \this.reachable;
         * @EFFECTS:
         *      (\all point p,q;q.reaches(q)==true&&p.reaches(q)==true;reachable[p.x][p.y].contains(q)==true
         *　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　&&reachable[q.x][q.y].contains(p)==true;
         */

　　　　d)使用天然語言。

String SPFA(point src,point des,Vector<point>[][] reachable) {       
　　　　 /**
         * @REQUIRES:src!=null&&src.inMap==true;
         *             des!=null&&des.inMap==true;
         * @MODIFIES: None;
         * @EFFECTS:\result==String(shortest path from src to des);
         */

　　　　改進寫法：

String SPFA(point src,point des,Vector<point>[][] reachable) {
        /**
         * @REQUIRES:src!=null&&src.inMap;
         *             des!=null&&des.inMap;
         * @MODIFIES: None;
         * @EFFECTS:\result！=null&&\result.length()>=0;
         */

　　　　e)未書寫exception_behavior。

　　　　

void initMap(String name,TaxiGUI gui) {
         /**
         * @REQUIRES:
         *      name!=null;
         *      gui!=null;
         *      File(filename).exist;
         * @MODIFIES:
         *      \this.map;
         *      \this.numMap;
         * @EFFECTS:
         *      \all int i;0<=i<80;this.map[i]==readLine(name);
         *      !MapReadSucceed==>output error information
         */

 

　　　　改進寫法：

void initMap(String name,TaxiGUI gui) {
         /**
         * @REQUIRES:
         *      name!=null;
         *      gui!=null;
         *      File(filename).exist;
         * @MODIFIES:
         *      \this.map;
         * @EFFECTS:normal_behavior
         *                 \all int i;0<=i<80;this.map[i]==readLine(name);
         *                  !MapReadSucceed==>exceptional_behavior (WrongFormatException);         
　　　    */              

 

聚焦關係

 　　因爲部分規格是在代碼實現後才書寫的，因此在個人這三次做業中，功能bug和規格bug沒有彙集關係。

心得體會

　　在書寫規格前，我會先思考方法須要實現的功能，以後再分析方法調用時默認知足的條件、用戶可以感受到的數據修改以及執行後系統知足的狀態，最後將這些信息體如今規格中。

　　良好的規格給咱們閱讀代碼提供了便利，提升了代碼的可讀性，使得bug的定位以及後期的代碼重構不那麼複雜。在寫規格的過程當中，可以理清思路，減小了由於邏輯錯亂而產生的bug，達到事半功倍的效果。這幾回做業中我寫出的代碼規格依然存在表意不明，邏輯不清等問題，因此在之後的代碼書寫中，我還應該對代碼的規格書寫多加練習。