OO第三次博客做業

OO第三次博客做業

規格化設計的發展歷史

對於要求的規格化設計發展歷史，我實在是沒有找到對應的資料，但從程序設計方法的發展歷史中能夠看到規格化設計的身影，因此我就結合程序設計方法的發展歷史，來講說規格化設計的發展歷史。

因爲計算機誕生之初，並無編譯器操做系統這一類東西，也沒什麼高級語言，那時的程序員只能使用機器語言來編寫程序，後來爲了方便程序員編寫又出現了助記符也就是彙編語言。咱們上學期的計組學習，也寫了很多MIPS彙編語言程序，對彙編語言的各類特色也是深有體會。

1. 靈活度極高。因爲彙編語言沒有固定的模式，一個極其簡單的功能也能夠有不少不一樣的實現方式。舉個栗子：就一個簡單的if/else語句，在高級語言中就是if/else，可是若是用匯編寫，十我的能寫出十個不一樣的版本出來。
2. 可讀性極差。不少同窗在計組P2階段都有過這樣的體會，由於彙編程序沒有變量名的說法，整個程序就是各類指令和寄存器翻來覆去，若是彙編程序不寫註釋，過上半天左右回來看以前寫的代碼，就幾乎是不知所云了。
3. 維護極困難。這實際上是上面兩點所致使的問題。上學期咱們所寫的彙編程序還很是簡單，編寫的最複雜彙編程序的也就是作了一個簡單的遞歸操做而已，翻譯成C代碼也超不過50行。然而就是這樣簡單的代碼，若是編寫過程出現了bug，要想debug也是一件很費時費力的事情，不少同窗P2掛了的緣由就是由於沒有修復程序的bug。而且一個寫好的彙編程序若是想要改需求(手動滑稽)，大機率只能重構了吧。

機器語言和彙編語言的這些特色也讓當時的不少程序員頭疼，因而就有一部分大牛決定開發新的，更友好的程序語言，面向過程的程序設計應運而生。面向過程的語言被認爲是一種「高級語言」,相比面向機器的語言來講,面向過程的語言已經再也不關注機器自己的操做指令、存儲等方面,而是關注如何一步一步的解決具體的問題。雖然相比機器語言有了很大的提高，可是仍存在一些問題。就咱們以前所編寫的C語言程序來看，變量名不規範，整個程序就一個main函數從頭寫到尾的麪條代碼現象也十分常見，這樣的代碼從可讀性和可維護性上講不比機器語言好多少。

因而就有了下面的第一次軟件危機，催生出告終構化設計。

隨着計算機硬件的飛速發展,以及應用複雜度愈來愈高,軟件規模愈來愈大,原有的程序開發方式已經越 來越不能知足需求了。1960 年代中期開始爆發了第一次軟件危機,典型表現有軟件質量低下、項目沒法 如期完成、項目嚴重超支等,由於軟件而致使的重大事故時有發生。例如 1963 年美國 (http://en.wikipedia.org/wiki/Mariner_1) 的水手一號火箭發射失敗事故,就是由於一行 FORTRAN 代碼 錯誤致使的。

軟件危機最典型的例子莫過於 IBM 的 System/360 的操做系統開發。佛瑞德·布魯克斯(Frederick P. Brooks, Jr.)做爲項目主管,率領 2000 多個程序員夜以繼日的工做,共計花費了 5000 人一年的工做量,寫出將 近 100 萬行的源碼,總共投入 5 億美圓,是美國的「曼哈頓」原子彈計劃投入的 1/4。儘管投入如此巨大, 但項目進度卻一再延遲,軟件質量也得不到保障。布魯克斯後來基於這個項目經驗而總結的《人月神話》 一書,成了史上最暢銷的軟件工程書籍。

爲了解決問題,在 196八、1969 年連續召開兩次著名的 NATO 會議,會議正式創造了「軟件危機」一詞, 並提出了針對性的解決方法「軟件工程」。雖然「軟件工程」提出以後也曾被視爲軟件領域的銀彈,但後 來事實證實,軟件工程一樣沒法解決軟件危機。

差很少同一時間,「結構化程序設計」做爲另一種解決軟件危機的方案被提出來了。 Edsger Dijkstra 於 1968 發表了著名的《GOTO 有害論》的論文,引發了長達數年的論戰,並由此產生告終構化程序設計方 法。同時,第一個結構化的程序語言 Pascal 也在此時誕生,並迅速流行起來。

結構化程序設計的主要特色是拋棄 goto語句,採起「自頂向下、逐步細化、模塊化」的指導思想。結構化程序設計本質上仍是一種面向過程的設計思想,但經過「自頂向下、逐步細化、模塊化」的方法,將軟件的複雜度控制在必定範圍內,從而從總體上下降了軟件開發的複雜度。結構化程序方法成爲了 1970 年 代軟件開發的潮流。

科學研究證實,人腦存在人類短時間記憶通常一次只能記住5-9個事物,這就是著名的7+-2原理。結構化程序設計是面向過程設計思想的一個改進,使得軟件開發更加符合人類思惟的 7+-2 特色。

結構化程序設計，一種編程範型。它採用子程序（函數就是一種子程序）、代碼區塊、for循環以及while循環等結構，來替換傳統的goto。但願藉此來改善計算機程序的明晰性、質量以及開發時間，而且避免寫出麪條式代碼。然而結構化的程序設計，仍是有其缺陷。當代碼變得愈來愈複雜，而且須要軟件自身不斷擴展不斷維護時，結構化的設計方法就有些力不從心了，所以面向對象的程序設計登上了歷史舞臺。

"分而治之"是處理大型問題的通常性原則，面向對象也是如此,面向對象的設計經過模塊組織程序，將一個龐大的程序切割成不少較小的模塊，經過接口來互相聯繫。可是如何進行分解成了主要難題。分解大程序一大利器是抽象，這也就引出了規格化抽象。規格化抽象是將執行細節(即模塊如何實現)抽象爲用戶所需求的行爲(即模塊作什麼)。這是從具體實現中抽象出模塊，須要的僅僅是模塊的實現能符合咱們所依賴的表述形式。經過規格化抽象，能夠把一個軟件分紅多個組件，使這些組件能夠最終組合起來解決最初的問題。這些組件的開發因爲有規格化的描述，開發較爲容易，而且後期若是須要更新維護只須要對相應的組件進行更改便可，極大的簡化了修改和維護的難度，對大型工程的開發有極大的幫助。於是受到程序員的熱捧。

規格Bug分析

說實話，我對OO課程關於設計規格這一部分的教學方式不敢苟同，若是真的要實現規格化設計，不該該等到第一次出租車寫完了以後才說要添加規格信息。而應該在第一次出租車做業以前就先有一次做業專門訓練如何寫規格。而後在寫出租車時先用一次做業進行數據抽象，把每一個類的規格和方法規格都寫好，下一次做業集中實現。經過這樣的方法，一方面與正常的大型工程的開發流程相適應，另外一方面可讓同窗們體會到規格的真正做用所在，若是規格寫得好，相信能夠作到像OO課上實驗時那樣，能夠不考慮其餘模塊的具體實現，僅根據規格來寫就不會出問題。

過程規格一方面是一個方法與其用戶交互的契約，另外一方面是對實現者作出的規約要求，但咱們的課程實際上兩點都沒有實現。

一方面規格自己因爲是布爾表達式可讀性較差，對於不超過二三十行的方法，實際上讀代碼都比讀規格來的直接，再加上因爲數據封裝大部分方法實際上都是對用戶隱藏的，用戶根本用不到，也就談不上什麼交互契約。

另外一方面因爲出租車做業主體早在第七做業就寫完了，咱們其實是在根據代碼寫規格，談不上對實現者的規約要求。

因此規格部分的三次做業，我認爲較爲合理的順序應該是

1. 規格寫法集中訓練(以較爲簡單的程序做爲訓練，鍛鍊先寫規格再寫代碼，先規劃再實現的流程)
2. 出租車數據抽象及規格設計(集中進行出租車的數據抽象和規格設計，不關心具體代碼的寫法，前兩次做業不須要互測，由於寫的好的第三次做業將會順水推舟，寫的很差的，第三次做業至關於白手起家，在第三次做業天然會見分曉，這纔是規格化設計的正確食用方法)
3. 出租車做業的集中實現，根據以前所寫的規格集中編寫代碼。

而咱們目前的OO課程中，規格這一部分更像是在打補丁，而不是在作規劃。

因爲出租車的大部分代碼早就在第一次出租車做業實現好了，以後是根據代碼寫規格，面對數百個方法，把以前寫好的代碼再寫一遍規格，大部分都是重複性的工做，十分枯燥乏味，再加上互測階段部分惡意扣分現象的發生，不少同窗對規格產生厭惡心理，甚至打心底咒罵規格，一旦產生這種心理，實際上這門課程已經失敗了，這也就是爲何規格這幾回課程基本上課就沒人聽的主要緣由。

規格化自己一個重要目的是爲了方便實現，而在咱們的課程中規格的主要目的是用來扣別人分。規格的一大目的是爲了準確描述，而若是太過關注格式問題，緊盯着各類不妨礙實現者理解的細節問題不放，而忽略了規格自己的含義，就真的很讓人唏噓。

我在這幾回做業中還算幸運，規格沒有被發現太多問題。第一次和第三次做業沒有被報規格問題，第二次做業由於一些<寫成了<=，以及有幾個變量名沒有寫對，被扣了兩個jsf。

這些bug產生的緣由，主要都是由於是根據代碼來寫規格，有一大部分工做是複製粘貼而且爲了知足格式須要，在判斷大小關係時要修改不等號方向，致使不等號寫錯，另外一方面因爲這幾回做業出現的變量實在是太多，在寫規格的過程當中確實是沒有過重視，致使變量名寫錯，原本應該判斷x的範圍卻寫成了判斷y的範圍，這個規格若是交給其餘人來實現將會出現不可避免的錯誤，後果將會十分嚴重。

很差的寫法和改進方案

1. 下面這個就是致使我第三次程序出bug的那個使用Loadfile初始化出租車的方法的jsf，能夠看到整個jsf寫的十分簡略，基本白話，並且幾乎沒有細節說明。

/**
     * @REQUIRES: scanner!=null&&taxis!=null&&output!=null;
     * @MODIFIES: scanner; taxis;
     * @EFFECTS:
     * initialize taxis;
     * (wrong format)  ==> exceptional_behavior (Exception)||exceptional_behavior (ExceptionInInitializerError);
     */

改進後的版本

/**
     * @REQUIRES: scanner!=null&&taxis!=null&&taxis.length==100&&output!=null;
     * @MODIFIES: scanner; taxis;
     * @EFFECTS:
     * (\all int i; 0<=i<30; taxis[i] == new Taxi_VIP(i));
     * (\all int i; 30<=i<100; taxis[i] == new Taxi_Normal(i));
     * (\all int i; 0<=i<100; taxis[i] is mentioned in file ==>init the state, credit and location of taxis[i]);
     * (wrong file format) ==> exceptional_behavior (ExceptionInInitializerError);
     * (wrong taxi Information) ==> exceptional_behavior(Exception);
     */

1. 下面的整個是紅綠燈更新的方法，雖然看上去沒有問題，但實際上其中的lightMap直接使用了gui自帶的紅綠燈二維數組guigv.lightmap賦值，雖然gui的這些靜態變量被默認初始化了，可是仍是應該寫上

/**
     * @REQUIRES: None;
     * @MODIFIES: lightMap;
     * @EFFECTS:
     * (\all int i,j; 0 <=i<80, 0 <=j<80; (\old(lightMap[i][j]==1) ==> lightMap[i][j]==2)&&(\old(lightMap[i][j]==2) ==> lightMap[i][j]==1))
     */

改進後

/**
     * @REQUIRES: lightMap!=null&&lightMap.length==80&&(\all int i; 0<=i<80; lightMap[i].length==80);
     * @MODIFIES: lightMap;
     * @EFFECTS:
     * (\all int i,j; 0 <=i<80, 0 <=j<80; (\old(lightMap[i][j]==1) ==> lightMap[i][j]==2)&&(\old(lightMap[i][j]==2) ==> lightMap[i][j]==1))
     */

1. 下面這個是更新出租車隊列的方法，雖然看起來全是規規整整的表達式，但實際上並不標準，其中用到的isActivate方法是用來判斷出租車是否應該在這次循環被喚醒。

/**
     * @REQUIRES: taxis!=null&&this.taxiMap!=null;
     * @MODIFIES: this.taxis; this.taxiMap;
     * @EFFECTS:
     * (\all Taxi taxi in this.taxis; change state and location);
     * (\all Taxi taxi in this.taxis; taxiMap[\old(taxi.x)][\old(taxi.y)].remove(taxi)&&taxiMap[taxi.x][taxi.y].add(taxi))
     * (\exist Taxi taxi in this.taxis; taxi.move() failed)==>exceptional_behavior (Exception);
     */

改進後

/**
     * @REQUIRES: this.taxis!=null&&this.taxiMap!=null&&this.taxis.length==100&&this.taxiMap.length==80&&(\all int i;0<=i<80;taxiMap[i].length==80);
     * @MODIFIES: this.taxis; this.taxiMap;
     * @EFFECTS:
     * (\all Taxi taxi in this.taxis; this.taxi.isActivate ==> this.taxi.move());
     * (\all Taxi taxi in this.taxis; taxiMap[\old(taxi.x)][\old(taxi.y)].contains(taxi)==false&&taxiMap[taxi.x][taxi.y].contains(taxi)==true)
     * (\exist Taxi taxi in this.taxis; taxi.move() failed)==>exceptional_behavior (Exception);
     */

1. 下面這個是更新一輛出租車的狀態的方法，能夠看到寫的也十分簡略。

/**
     * @REQUIRES: None;
     * @MODIFIES: this;
     * @EFFECTS:
     * change state and stateTime;
     * (can't find a way to destination) ==> exceptional_behavior (Exception);
     * @THREAD_EFFECTS: \locked(this);
     */

改進後

/**
     * @REQUIRES: this.stateTime!=null&&(this.state.equals(State.ORDER)||this.state.equals(State.SERVICE))==>this.destination!=null;
     * @MODIFIES: this;
     * @EFFECTS:
     * (\old(this.state).equals(State.WAIT)&&\old(this.stateTime==20000))==>(this.stateTime=0&&this.state.equals(State.STILL));
     * (\old(this.state).equals(State.WAIT)&&\old(this.stateTime=!20000)&&this.destination!=null)==>(this.stateTime=0&&this.state.equals(State.ORDER));
     * (\old(this.state).equals(State.STILL)&&\old(this.stateTime==1000)&&this.mainRequest==null)==>(this.stateTime=0&&this.state.equals(State.WAIT));
     * (\old(this.state).equals(State.STILL)&&\old(this.stateTime==1000)&&this.mainRequest!=null)==>(this.stateTime=0&&this.state.equals(State.SERVICE)&&this.executeMainRequest());
     * (\old(this.state).equals(State.ORDER)&&this.destination.equal(this.x, this.y))==>(this.state.equals(State.STILL)&&print information);
     * (\old(this.state).equals(State.SERVICE)&&this.destination.equal(this.x, this.y))==>(this.state.equals(State.STILL)&&print information&&this.requestOver());
     * (can't find a way to destination) ==> exceptional_behavior (Exception);
     * @THREAD_EFFECTS: \locked(this);
     */

1. 下面這個是新增路徑流量的方法，在增長流量的同時刪除時間太久的流量信息,但一樣寫的太過簡略

/**
     * @REQUIRES: 0 <= src <6400&&0 <=dst <6400&&abs(time-System.currentTimeMillis())<=100;
     * @MODIFIES: this.flowMap;
     * @EFFECTS:
     * put FlowNode into according queue of getKey(src, dst) and delete FlowNodes which are too old;
     */

改進

/**
     * @REQUIRES: 0 <= src <6400&&0 <=dst <6400&&abs(time-System.currentTimeMillis())<=100&&this.flowMap!=null&&flow>0;
     * @MODIFIES: this.flowMap;
     * @EFFECTS:
     * this.graph[src][dst]==0 ==> return;
     * flowMap.get(getKey(src,dst))==null ==> flowMap.get(getKey(src,dst)).contains(new FlowNode(flow,time)); 
     * (\all FlowNode flowNode in \old(flowMap).get(getKey(src,dst));flowNode.time<time-600 ==> flowMap.get(getKey(src,dst)).contains(flowNode)==false);
     */

基本思路和體會

說到設計規格，實際上這幾回做業，基本上都是寫好了代碼，再回過頭來補規格，談不上什麼基本思路和體會。在此只能說一下我是怎麼撰寫規格的，相信有大量的同窗和個人方法是同樣的，就作一個反面教材吧。

因爲每次都是對已經寫好的方法來撰寫規格，requires部分只須要看傳進來的參數和該方法內用到的非局部變量，看這些參數的和變量是否爲空，是否在規定範圍內。modified更是隻須要查看非局部變量是否有更改，是否對文件和標準輸入輸出有操做。對於effects部分，能用布爾表達式描述的用布爾表達式描述，實在描述不了的用天然語言描述，只須要關注\result，以及對非局部變量所作的變更，是否有拋出異常。

這樣的寫法通過這幾回做業確實是沒什麼收穫，就是複習了一下離散一，瞭解了一些格式，至於規格到底有什麼用，大概就是給測試者看吧，順便消磨一些原本就不怎麼充裕的時間，畢竟本身寫的程序讀代碼都比讀規格來得快，做爲測試者看規格實際上也就是看看規格是否是和這個方法一致，若是真的想要發現bug，還得本身花大功夫測試。我不否定這幾回做業的功能性bug數與規格bug數量確實是正相關，可其中又有多少是因爲規格寫的很差致使功能出了問題呢？大部分實際上是功能不對，規格只是順着錯誤的功能進行描述，或是功能正確但規格沒寫對。

總而言之，這幾回做業做業給個人感覺就是「雞肋」，典型的費時費力還收穫極少。有這些時間我還不如好好去看看推薦的多線程和設計模式的那兩本書，相信比我在這對着寫好的代碼寫規格收穫多得多，也不用每次被互測階段的各類可能遭遇所困擾。

心得體會

最後一次寫代碼的做業已經結束了，剩下的不知道是些什麼，其實我也不太關心了，這十幾周已經鍛煉出了一顆佛系的心。通過這十二週的折磨，個人代碼風格有了提高，對面向對象有了更深的理解，只不過代價大了些。大部分時間都被做業佔用了，沒有多少時間總結，也沒有多少時間去學習新的知識。我買了推薦的那兩本書，本身也研讀了其中的部分章節，確實受益不淺，其內容之廣之深確實是幾節課根本沒法說清楚的，而咱們的OO課程卻作到了一節課講小半本書的速度，大部分細節被忽略，我我的能力有限，自學速度實在是跟不上，多線程那本書纔看了三章就只能拋下換另外一本。你們都在吐槽這門課有多麼糟糕，在我看來最糟糕的部分在於，在同窗們尚未什麼知識經驗積累狀況下強制推行超過同窗們當時水平範圍的要求，自己課程容量極大但願同窗們可以在課下完成自學，但同時又佈置大量的做業佔用課下時間（要知道這學期不僅有OO還有OS，OS也不是一個整天浪一浪就能學好的課程），沒有什麼知識經驗基礎，靠着這些做業來積累經驗，就彷彿是在從新發明輪子，難度大還吃力不討好。

如今回過頭來看我寫過的9次編程做業，我花這麼多時間在這門課上到底值不值，我目前的回答是不值。這學期開學時我作了很多的計劃，有很多的願景，如今看來都是虛無縹緲罷了，這確實和我這學期的決策有關係，想把全部事情都作好的結果每每是什麼事都作很差，這也算是我這學期最大的收穫吧，雖然過去早就明白這個道理，但從未如此刻骨銘心。說的有點多也有點遠，以上純屬我的見解。最後仍是很感謝常常一塊兒討論的各位大佬，感謝助教在羣裏不厭其煩的回答，以及老師爲構思這門課程作出的努力。