小菜雞兒的第三次OO博客

規格化設計歷史

　　規格化設計的歷史目前網上的資料並很少，百度谷歌必應也表示無能爲力......

　　在這裏結合現實狀況講一講本身對程序規格化的理解，首先代碼規格化對代碼的影響是間接的，或許它不能讓你代碼裏面的bug直接消失，或許它也不能讓電梯之間不相互阻塞，可是它能讓OO實驗拿到更多分啊//笑。玩笑歸玩笑，下面具體分析一下規格化設計（JSF爲例）的做用：

• 在代碼實現過程當中，人們每每不能從一開始對整個項目的每一個細節都面面俱到地思考一遍，規格化設計在開發初期能夠將項目中的細節隱去，工程師只須要考慮類or包須要完成的功能便可，只用在JSF的effecs寫幾行功能影響豈不是美滋滋。
• 其次在代碼具體實現過程當中，Modifies和Requires有助於減小bug的產生。在項目初期定下的JSF能保證程序猿們在亂七八糟的需求修改下不忘初心，在一次又一次的指導書修改中不忘這個類到底是要完成怎樣的歷史使命，明確了每一個變量的用途、每一個方法的使用目的，時時提醒程序猿們不要犯一些低級錯誤。
• 而在企業項目中，代碼的規格化尤其重要，一個項目大多都是由一個團隊來完成，若是沒有統一的代碼規範，那麼每一個人的代碼一定會風格迥異。且不說會存在多我的同時開發同一模塊的狀況，即便是分工十分明晰的，等到要整合代碼的時候也有夠頭疼的了。大多數狀況下，並不是程序中有複雜的算法或是複雜的邏輯，而是去讀別人的代碼實在是一件痛苦的事情。統一的風格使得代碼可讀性大大提升了，人們看到任何一段代碼都會以爲異常熟悉。顯然的，規格化的代碼在團隊的合做開發中是很是有益並且必要的。

---

 

規格bug分析

　　本身寫的代碼規格基本上屬於「你的代碼真的很爛」級別，博主懶癌晚期，每次觀測點的JSF屬於隨緣被掛狀態。下面來分析一下這些垃圾代碼，強迫症大佬謹慎食用：

/**@ REQUIRES: AllNode!=NULL;
* taxi!=NULL;
* loc= int[2];
* des= int[2];

嚴格地說Requires裏面要對各個變量進行詳細地規定，要是能與與repOK一致的話是最吼的：

/** @ REQUIRES: AllNode!=NULL;
* taxi!=NULL;
* (loc!=NULL) && (loc.size==2) && (All int i=1;i<=2;)==>(loc[i]>=0 && loc[i]<80);
* (des!=NULL) && (des.size==2) && (All int i=1;i<=2;)==>(des[i]>=0 && des[i]<80);

　　這幾回做業在書寫JSF規格時，更像是一種亡羊補牢的過程，首先要求咱們具體實現一次代碼，再向代碼添加JSF，其實與規格化設計略有相悖，另外我認爲課程組可能有一點點低估JSF的完成難度，一個優秀的後補JSF須要程序猿閱讀本身都快忘了的一坨屎，讀完後還須要將代碼抽象出通常性的邏輯。以目前北航計算機系大部分同窗的編程風格來講，數百行的類基本上比比皆是，數百行的方法也是大有人寫，將三位行數的代碼抽象出effects可不是一個簡單的過程，而與此同時還要完成複雜的流量紅綠燈設計以及基於gayhub的操做系統，這確實有一點點難了。不過在這幾回公測中，我有幸抽到了一份JSF尚可的代碼：

/**
 * @REQUIRES:m!=null;
 * @MODIFIES:\this.situation;
 * \this.isCalled;
 * \this.curTime;
 * @EFFECTS:normal_behavior:
 * 出租車行駛，\this.situation按照出租車的行駛狀況不斷變化；\this.isCalled在出租車成功接到單子時變爲true；接單結束後變成false；
 * exception_behavior(InterruptedException e):
 * System.out.println("Oops," + this.toString() + " seems to have some problem.");
 */
　　若是沒有記錯的話天然語言描述依然是在容許範圍以內的，固然就算不容許，我認爲依然不該憑此扣分，畢竟從複雜的代碼中抽象出effects仍是一個工程量很大的任務。

---

Bug分析
　　

	功能bug	規格bug	是否相關
第九次做業	0	0	否
第十次做業	3	5	否
第十一次做業	0	0	否

 

 　　在最近三次的做業中，第九次做業和第十一次做業沒有被互測出bug，第十次做業的問題主要集中在：1.出租車並未直接右轉；2.出租車在直行時並未按照紅綠燈行駛；3.出租車在派單過程當中並未按照最短路徑原則。首先第三個bug是由第一二個bug形成的，畢竟未正確按紅綠燈行駛會形成流量決策一定失敗，前兩個bug的主要問題是在派單函數中並未作到修改出租車的方向。在個人紅綠燈體系中，用1，2，3，4四個數字表示絕對方向，分別對應東北西南，而出租車選擇一個絕對方向行駛後應當在下一個紅綠燈路口前實現轉換，如：出租車A在第一個路口決定往北走，當它抵達第二個路口時，它的駛來方向應該是南邊，所以形成了紅綠燈判別不正確。規格bug主要集中在對出租車的多態實現時，全部的get&set方法沒有寫JSF，瞬間被掛滿~

 

---

心得體會
　　程序是讓人看的，是要分享給隊友或者老師，甚至是任何陌生的人共享交流。或許你的算法複雜度能作到o(1)，或許你的代碼可拓展性很強，可是這些都比不上一羣與你一塊兒開發項目的程序猿，一羣能讀懂並指出你規格化代碼bug的人。或許在這學期的面向對象課程中JSF是一個很煩人的存在，可是規格化程序設計的重要性是毋庸置疑的。