這是OO的第三次博客作業，也是JSFO（面向JSF編程）的第一次博客作業。暗示了我們面向對象課程已經再向JSF的編寫過渡。

不知不覺OO的作業已經寫完3/4，那些熬夜趕作業的日子仍然歷歷在目，仿佛是昨天一樣。好在這三次是不用像開始接觸多線程那麽拼了。

總而言之還是先把這次作業寫完吧。

論規格化設計

我們要進行規格化設計，首先得明白什麽是規格化設計，為什麽要規格化設計。經過簡單的調查（百度），我們來談談規格化設計。

規格化設計的發展歷史

從發展歷史談起，想知道誰首先提出規格設計抽象，規格化抽象的源頭，顯然是不現實的。畢竟這並不算計算機科學的一個重大發現，拿不到圖靈獎的。但是這並不代表規格化設計就不重要。

早在1969年（是的，你沒看錯，就是1969），已經有人開始提出規格化設計了。來自北愛爾蘭貝爾法斯特女王大學的C.A.R.Hoare發表了一篇名為An Axiomatic Basis for Computer Programming（計算機程序的公理基礎）的論文。著實讓我大吃一驚，規格抽象從如此之早就已經得到人們的重視。這也是我能調查到規格化發展歷史中，其被提出相當早的了。

在這篇論文中，Hoare就已經提出了基於“前置後置條件”的接口規格方法。很容易聯想到我們所寫的JSF中的requires和effects。所以說這篇論文的發布，可以說是高瞻遠矚的，到現在都很難以想象在1969年，計算機都尚未推廣發展的時候，就有人已經開始思考規格化了。在計算機還未普及時就有人提出規格，也從側面也反映出來規格化設計的重要性。

在這裏我特地貼出原文的一部分供大家瞻仰，並借此說明為什麽規格化設計得到了coder們的重視。其中中文翻譯為機翻，幫助理解的。不然貼這麽大段英語原文估計沒人願意讀。

The most important property of a program is whether it accomplishes the intentions of its user. If these intentions can be described rigorously by making assertions about the values of variables at the end (or at intermediate points) of the execution of the program, then the techniques described in this paper may be used to prove the correctness of the program, provided that the implementation of the pro- gramming language conforms to the axioms and rules which have been used in the proof.

程序最重要的屬性是它是否完成了用戶的意圖。如果可以通過在程序執行結束時（或在中間點）對變量值作出斷言來嚴格描述這些意圖，那麽本文描述的技術可以用來證明程序的正確性，提供編程語言的實現符合證明中使用的公理和規則。

But the practical advantages of program prov- ing will eventually outweigh the difficulties, in view of the increasing costs of programming error. At present, the method which a programmer uses to convince himself of the correctness of his program is to try it out in particular cases and to modify it if the results produced do not cor- respond to his intentions. After he has found a reasonably wide variety of example cases on which the program seems to work, he believes that it will always work. The time spent in this program testing is often more than half the time spent on the entire programming project; and with a realistic costing of machine time, two thirds (or more) of the cost of the project is involved in removing errors during this phase. The cost of removing errors discovered after a program has gone into use is often greater, particularly in the case of items of computer manufacturer‘s software for which a large part of the expense is borne by the user. And finally, the cost of error in certain types of program may be almost alculable--a lost spacecraft, a collapsed building, a crashed aeroplane, or a world war. Thus the practice of program proving is not only a theoretical pursuit, followed in the interests of academic respectability, but a serious recommendation for the reduction of the costs associated with programming error.

但鑒於編程錯誤的成本增加，程序驗證的實際優勢最終將超過困難。目前，程序員用自己的方法說服自己程序的正確性的方法是在特定情況下嘗試並在產生的結果不符合其意圖的情況下對其進行修改。在他找到了該程序似乎能夠工作的各種各樣的案例之後，他認為它將始終有效。在這個程序測試中花費的時間往往超過整個編程項目花費的時間的一半;並且對機器時間的實際成本計算而言，項目成本的三分之二（或更多）涉及在此階段消除錯誤。消除程序投入使用後發現的錯誤的代價通常更大，特別是在用戶承擔大部分費用的計算機制造商軟件的情況下。最後，某些類型的程序中的錯誤代價可能幾乎是可以降低的 - 一個丟失的航天器，一座倒塌的建築物，一架墜毀的飛機或世界大戰。因此，程序證明的實踐不僅是理論上的追求，其次是為了學術的可尊重性，而是為減少與程序錯誤相關的成本而提出的嚴格建議。

為什麽規格化得到了大家的重視

在我的理解，Hoare所提出的規格抽象用於保證程序的正確性。雖然使用規格抽象來驗證程序正確性需要花費時間，但如果程序投入使用後發現錯誤，這個代價遠比驗證所花的時間要大（作為一個北航的學生看到Hoare提出的例子也是倍感親切）。如果一個航空器的程序中，出現了哪怕一點的紕漏，都會引起無比慘痛的後果。

包括甚至到今天，軟件的規模隨著軟件行業的成熟和發展，軟件系統的復雜性使得錯誤出現的幾率大幅提升，而編程錯誤的成本也不言而喻。為了解決這個問題，使用規格化方法來驗證程序的正確性，簡化編程過程也是相當有必要的，也得到了不少研究者的認可。

除此之外，一個出色的規格化設計可以幫助程序員理解程序和分割程序。一個企業中不可能只有一個碼農。作為一個合作的team，代碼需要讓團隊中的所有人都理解。因此一個好的規格化設計能讓他人很容易的理解你的代碼，在團隊中也十分有用。相信所有碼農都希望閱讀到的是風格清晰明確，可讀性強的代碼，而不願意閱讀亂七八糟，不明就裏的代碼。

規格BUG戰

我被報了哪些BUG

三次當中僅有第一次被報了JSF規格BUG，共計13個，但是包括測試者為扣而扣的，如modifies中沒有gui，modifies中沒有System.out這種莫名其妙的。搞笑的是他備註有問題及時申訴但是一副不想撤的樣子。

表格如下：

在第一次就被“狠人”給制裁之後，後面兩次我不敢不好好寫。第十次作業時我做的第一件事就是把他所有報的地方給修改掉，然後看看還有沒有地方寫錯了。

分析一下這些bug吧，由於我的代碼大多數為了美觀加了不少空行，這些行數都是過濾掉空行所剩下的行數。可以看出來大部分是沒超過50行的。

requires不完整：這一部分大多為漏寫，我在寫很多方法的requires時並沒有考慮太多就寫了None，實際上是可以填寫的。比如這個

　　/**
     * @REQUIRES : None; 
     * @MODIFIES : this.OrderSet;
     * @EFFECTS : (this.OrderSet.contains(taxi_id)) ==> \result == false;
     *            (!this.OrderSet.contains(taxi_id)) ==> (\result == true && this.OrderSet.contains(taxi_id));
     */
    public boolean takeOrder(int taxi_id){
        return this.OrderSet.add(taxi_id);
    }

這是出租車搶單的方法。其實是可以寫requires的，很明顯出租車的編號有範圍限制，應該為：

　　　/**
     * @REQUIRES : 0 < taxi_id <= 100; 
     * @MODIFIES : this.OrderSet;
     * @EFFECTS : (this.OrderSet.contains(taxi_id)) ==> \result == false;
     *            (!this.OrderSet.contains(taxi_id)) ==> (\result == true && this.OrderSet.contains(taxi_id));
     */
    public boolean takeOrder(int taxi_id){
        return this.OrderSet.add(taxi_id);
    }

當然代碼中有不少是這個原因有雷同，上限為5個。而有意思的是測試的狠人還扣了一個放在了Requires邏輯錯誤裏面。

/**
     * @REQUIRES : 0 <= taxi_id < 100; 
     * @MODIFIES : None;
     * @EFFECTS : true ==> (System.out.println("查詢時間：" + (System.currentTimeMillis() - Timer.start_time) / 100 + "(*100ms)") &&
     *                      System.out.println("出租車坐標:(" + taxi.getTaxi_x() + "," + taxi.getTaxi_y() + ")") &&
     *                      System.out.println("出租車狀態:" + taxi.getState())) ;
     */
    public void inquiryTaxi(int taxi_id){

（當時Requires是None，重復報了）

然而還有兩個我認為是不合理的，因此申請仲裁中，表格裏面也打了括號。

modifies不完整：也是漏寫了，類裏面有的屬性沒有加進去。

effects不完整：同上，沒有加入effects中。

effects邏輯錯誤：兩個方法都是effects裏面改寫“==”而我寫成了 “=”。有一個我自己都找了好久才發現，只能說是個狠人。

分析可知主要問題出自於漏寫Requires，這一部分多半處於考慮不周造成的。而其余的也是漏寫誤寫巨多，因此很難從代碼行數中總結出來規律。在改完了這些漏寫的bug後，後兩次並沒有被爆JSFbug。

但是在寫JSF的過程中，對於行數長的方法，在進行規格抽象時確實感受到了困難壓力，因此多用了自然語言來處理，這也是JSF的問題吧。

我為什麽會產生規格BUG

先找一些客觀原因。

第一，首先我還是繼承著上一次的觀點，在作業都難以保證沒有bug的情況下，妄談優化、優雅，顯然是不現實的。雖然這三次作業在難度上確實是降低了，大概是希望我們能有更多時間來註重規格化。但是當我拿著第七次作業的代碼補充了流量之後，只能看著一個個長的不行的方法對如何寫JSF發愁。第七次作業，要我們實現出租車系統，難度雖然不大，比不上電梯、IFTTT，但也不像後面兩次那樣隨便寫寫就能完成，所以在第七次我還是把實現放在優雅之前考慮的。後面的作業在第七次作業的基礎上完成，根基不穩，導致JSF根本無法立足。而第九次作業我光是寫實現就寫到了星期三，下午才開始寫JSF，基本上是亡羊補牢。

難度是一部分，如果要寫的作業是oo實驗課上寫的那個銀行轉賬系統，像這種難度，那我肯定能把JSF寫的又快又好。而第七、九次作業的難度並沒有這麽友好，能讓我把代碼實現的更為優雅，可能是因為我太菜了。

另外一部分是希望課程組能在第七次作業就開始寫JSF，而不是那些設計原則。如果能把JSF寫好，代碼的風格應該也不會違背那些設計原則。一個超過50行的方法就已經很難寫JSF了，更何況當我們不知道要寫JSF時，僅僅要實現功能，像我這種菜雞寫出超過50行的代碼可能已經是常態了。如果早做打算，從第一次出租車作業就要求JSF，那麽設計者在編碼時一定會認真考慮每一個方法。

第二，寫JSF和OO這門課的互測機制有著難以調和的矛盾。這一部分也希望能在之後做好協調。舉個例子，我們做一個選擇題

A.拿高分 B.寫出好的代碼

肯定有不少人比起寫好的代碼，更註重拿高分。就會出現幾種極端的存在：

1.選擇A，寫代碼的時候，類能寫多"少"寫多"少"，方法能寫多"少"寫多"少"。到時候別人扣我JSF也扣不了幾個。這樣的代碼當然不可能是優雅的。

2.選擇A，但是懶得好好寫代碼。那麽怎麽拿分呢？找bug之外費時又費力，當然是扣JSF簡單方便了。現階段大多數人的編程水平可能談不上優雅，跟大佬的更是沒法比，JSF難以做到十全十美。測試者對每一個方法仔細
“揣摩”，然後憑著“自己的理解”來扣JSF，甚至是為了扣JSF而扣JSF，一扣就是10個20個，美其名曰“怕別人扣我的”。這種人我把其稱之為“狠人”。

3.選擇A和B。這種人我們稱之為大佬。

4.選擇B，好好寫代碼，方法寫的巨多，JSF盡量認真寫。但是到最後碰到“狠人”，方法多，JSF被爆的更多，欲哭無淚。下一次吸取教訓也開始扣JSF，逐漸變成“狠人”。

JSF本身主觀性就很強，導致惡意扣分也很正常。這三次作業我才發現“狠人”並不少，甚至最後一次“狠人”更是到難以想象。像這種惡意扣JSF，並不是止步於所有人都開始好好寫JSF，而是擴散成更多人開始惡意扣JSF，很多人開始厭惡JSF甚至聞JSF色變，這顯然不是一個好現象。面向對象編程已經開始轉變成面向運氣編程，如果測試者是好人，那麽就能好好存活下去。但凡遇到個“狠人”，就只能默默吃癟。

當惡意扣JSF滋生時，應該想辦法杜絕惡意的扣JSF現象發生。JSF應當是一個幫助別人理解代碼，描述方法的工具，而不是作為從中賺取分數的工具。

希望明年能夠好好協調好寫JSF和互測JSF的關系，讓更多人註重於“我要好好寫代碼，這樣才好寫JSF”，而不是“我要好好扣他的JSF”。

接下來是分析下自身原因，首先是因為時間不足，星期三下午開始寫JSF，那麽多方法一個一個寫，難免會出紕漏，由分析看出來漏寫誤寫居多。另外一個個人原因是因為不重視，心想“大家應該都是扣幾個JSF意思意思吧”，結果正好碰到的是“狠人”，結果被扣的一塌糊塗。

當然最大的原因還是代碼寫的差，作為一個大部分時間都要用於實現功能的編程菜雞，寫出來的代碼自然跟優雅無關。大量的50行以上代碼，以致於不得不用自然語言來寫effects。在JSF中出紕漏當然也不是偶然了，雖然這些並沒有被報BUG。

JSF改進

雖然規格bug大多數來源於漏寫誤寫，但是可以改進的也不少，比如

1.

　　/**
     * @REQUIRES : None; 
     * @MODIFIES : this.AskList;
     * @EFFECTS : AskList.contains(ask);
     */
    public synchronized void addAsk(Ask ask){
        AskList.add(ask);
    }

可以改為@EFFECTS : AskList.contains(ask) && AskList.size == \old(AskList).size + 1;這樣表達添加請求更加明正確。

2.

　　/**
     * @REQUIRES : AskList != {}; 
     * @MODIFIES : this.AskList;
     * @EFFECTS : !AskList.contains(ask);
     *            (\all Ask a; a != ask; AskList.contains(a) == \old(AskList.contains(a));
     */
    public synchronized void deleteAsk(Ask ask){
        AskList.remove(ask);
    }

這個雖然正確，但是過於繁瑣，可以該為@EFFECTS : !AskList.contains(ask) && AskList.size == \old(AskList).size - 1; 同樣的意思，看上去就簡潔很多

3.

　　/**
     * @REQUIRES : 0 <= x1 < 80,0 <= x2 < 80,0 <= y1 < 80,0 <= y2 < 80; 
     * @MODIFIES : None;
     * @EFFECTS : \result == ""+x1+","+y1+","+x2+","+y2;  
     */
    private static String Key(int x1,int y1,int x2,int y2){
        return ""+x1+","+y1+","+x2+","+y2;
    }

這個是用於流量判斷的，REQUIRES除了滿足 0 <= x1 < 80,0 <= x2 < 80,0 <= y1 < 80,0 <= y2 < 80，之外，應該還要保證(x1,y1),(x2,y2)表示相鄰點。

4.

/**
     * @REQUIRES : None; 
     * @MODIFIES : None;
     * @EFFECTS : \result == (\exist int k; 0 <= k < asklist.getSize(); asklist.getAsk(k).equals(ask));
     */
    public synchronized boolean judge_same(Ask ask,AskList asklist)
    {
        Point current_src = ask.getOrigin();
        Point current_dst = ask.getDestination();
        long current_time = ask.getTime();
        
        for(int i = 0 ; i < asklist.getSize() ; i++)
        {
            Ask askInList = asklist.getAsk(i);
            if(askInList.getOrigin().equals(current_src) && askInList.getDestination().equals(current_dst) && askInList.getTime() == current_time)
                return true;
        }
        
        return false;
    }

這裏REQUIRES可以添加asklist != {} ;否則與get(i)相矛盾。

5.

大多運用自然語言。如果進行重構很多方法可以再抽象出來，這樣寫JSF時也不會感覺無從下手，從而使用自然語言。

功能BUG與規格BUG的聚集關系

第九次作業被爆的最多，上面已經是撤回過3個的數據。第十次的測試者還是比較善良，至少沒有從我JSF中找錯誤而是只關註功能錯誤。第十一次作業是遇到的最善良的測試者，一個bug都沒有申報（估計是沒有測試）。祝好人一生平安，OO拿高分。

如果僅從表格來分析，貌似找不到什麽聚集點，關系不太緊密。但是如果仔細分析一下，會得出如下結論：扣我JSF扣得最兇的人，BUG也不會放過我（報了3個BUG申訴撤回了一個），這說明測試者是個狠人。而之後遇到的人並沒有扣JSF，說明還是很善良的。所以得出如下結論：JSF被扣多少很大部分不是取決於你寫的如何，而是取決於你的測試者是個好人還是狠人。

這三次測試過程我只在第一次扣了被測者3個JSF，之後兩次測試均未扣JSF。尤其是第三次測試，因為星期四一天基本是在OS上，晚上還要寫OS報告。星期五一天都有課，晚上還有馬原。因此只是隨便測了一下，申報了一個紅綠燈文件沒有過濾空格的BUG，結果這次遇到好心人並沒有對我下手。看來善惡終有報，天道有輪回。

總結與體會

1、這三次作業下來，收獲還是相當多的。最大的收獲就是從JSF的書寫中，了解了規格化設計，對於什麽是“好的代碼”有了更深刻的理解。雖然自己的代碼還是寫的跟那些大佬的代碼沒法比，甚至說是“真的很爛”也沒有問題。但是比起以前寫的亂七八糟，冗長繁復的代碼好太多了。

聽說下次作業是向第三次作業加規格。我回過頭回顧一下ALS電梯的代碼，發現真是沒眼看。有的類內容很少，而scheduler類內容多，而且動輒上百行。這樣一份代碼想寫出JSF基本上是很難的，迫切需要重構。好在我現在是知道從何改起了。

2、還有一個收獲是心態。以前的我被扣了一個莫名其妙的bug就會難受很久，現在的我已經不會因為這點分數斤斤計較了，對分數看開了。在被狠人給狠狠制裁一把之後，現在我哪怕被扣了三個bug也能坦然面對。感謝OO讓我的心態得到了極好的鍛煉。

之前有人問前輩OO需要什麽，得到的回答讓我受益匪淺。

3、就我最後一次聽到幾個同學被扣分數量，發現狠人還是不少。看來和諧6系僅僅只是老師口中的一句笑談。和諧6系？不存在的。永遠不要相信你的同學。哪怕在群裏說自己多慘，你也不知道他扣了別人多少。

4、這幾次寫JSF的思路是這樣：

已有代碼

補充代碼完成功能

按照代碼寫JSF

顯然這樣是不是一個好的設計思路。理想中的JSF編寫思路應該是：

思考如何完成功能

構思一個大致的JSF

通過構思來編寫代碼

完善JSF

OO的旅程已經走過四分之三，萬裏長征已經走完了7500裏。希望能順利熬過最後幾次作業，也希望和諧6系能夠真正的構建起來。只要人人都獻出一點愛，世界將會變成美好的人間。

JSF生存指南P1