JSF生存指南P1

這是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寫的又快又好。而第7、九次做業的難度並無這麼友好，能讓我把代碼實現的更爲優雅，多是由於我太菜了。

另一部分是但願課程組能在第七次做業就開始寫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，結果此次遇到好心人並無對我下手。看來善惡終有報，天道有輪迴。

---

 總結與體會

一、這三次做業下來，收穫仍是至關多的。最大的收穫就是從JSF的書寫中，瞭解了規格化設計，對於什麼是「好的代碼」有了更深入的理解。雖然本身的代碼仍是寫的跟那些大佬的代碼無法比，甚至說是「真的很爛」也沒有問題。可是比起之前寫的亂七八糟，冗長繁複的代碼好太多了。

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

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

以前有人問前輩OO須要什麼，獲得的回答讓我受益不淺。

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

 四、這幾回寫JSF的思路是這樣：

已有代碼 

補充代碼完成功能

按照代碼寫JSF

 

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

思考如何完成功能

構思一個大體的JSF

經過構思來編寫代碼

完善JSF

---

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