規格化設計歷史

  規格化設計的歷史目前網上的資料並不多,百度谷歌必應也表示無能為力......

  在這裡結合現實情況講一講自己對程式規格化的理解,首先程式碼規格化對程式碼的影響是間接的,或許它不能讓你程式碼裡面的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是一個很煩人的存在,但是規格化程式設計的重要性是毋庸置疑的。

Normal
0

7.8 磅
0
2

false
false
false

EN-US
ZH-CN
X-NONE

/* Style Definitions */
table.MsoNormalTable
{mso-style-name:普通表格;
mso-tstyle-rowband-size:0;
mso-tstyle-colband-size:0;
mso-style-noshow:yes;
mso-style-priority:99;
mso-style-parent:"";
mso-padding-alt:0cm 5.4pt 0cm 5.4pt;
mso-para-margin:0cm;
mso-para-margin-bottom:.0001pt;
mso-pagination:widow-orphan;
font-size:10.5pt;
mso-bidi-font-size:11.0pt;
font-family:等線;
mso-ascii-font-family:等線;
mso-ascii-theme-font:minor-latin;
mso-fareast-font-family:等線;
mso-fareast-theme-font:minor-fareast;
mso-hansi-font-family:等線;
mso-hansi-theme-font:minor-latin;
mso-font-kerning:1.0pt;}
table.MsoTableGrid
{mso-style-name:網格型;
mso-tstyle-rowband-size:0;
mso-tstyle-colband-size:0;
mso-style-priority:39;
mso-style-unhide:no;
border:solid windowtext 1.0pt;
mso-border-alt:solid windowtext .5pt;
mso-padding-alt:0cm 5.4pt 0cm 5.4pt;
mso-border-insideh:.5pt solid windowtext;
mso-border-insidev:.5pt solid windowtext;
mso-para-margin:0cm;
mso-para-margin-bottom:.0001pt;
mso-pagination:widow-orphan;
font-size:10.5pt;
mso-bidi-font-size:11.0pt;
font-family:等線;
mso-ascii-font-family:等線;
mso-ascii-theme-font:minor-latin;
mso-fareast-font-family:等線;
mso-fareast-theme-font:minor-fareast;
mso-hansi-font-family:等線;
mso-hansi-theme-font:minor-latin;
mso-font-kerning:1.0pt;}