一．規格化設計的發展歷史
　　規格化設計的一個重要目的是為了將模塊的功能，約束表達清楚，方便用戶與開發者的信息交流，從這一點來看，規格化設計的出現與結構化設計有著密不可分的關系，接下來，我將從結構化設計的角度來討論規格化設計。
　　程序設計的演變大致可以分成以下三個過程：
　　1. 20世紀60年代以前，計算機剛剛投入實際使用，軟件設計往往只是為了一個特定的應用而在指定的計算機上設計和編制，采用密切依賴於計算機的機器代碼或匯編語言，軟件的規模比較小，很少使用系統化的開發方式，此時的代碼更多的是私人性質的，滿足個人要求的程序；
　　2. 60年代中期，大容量、高速度的計算機出現，隨之出現的是代碼量急劇提升，復雜度急劇增長、程序可靠性問題突出的問題。結果化程序設計隨之提出，它要求程序設計時以模塊為單位，每個模塊專職自己的工作，而要在模塊間交流，在開發者和用戶，開發者和開發者之間交流，就只需要相應接口即可；

三．規格錯誤的產生原因及解決
　　首先，2、3不用多加討論，屬於粗心導致的錯誤，剩下的三個點，恰好對應了jsf規格的三個種類。首先對於EFFECTS不完整的錯誤，因為run方法它實現了出租車四個狀態之間的切換和它的運行規則，所以其實不是很好表述，後來我想可以抽象表示其狀態的切換而忽略其它運行細節，所以有了這樣的表述:
@EFFECTS：
(this.request==null && count%20!=0 && \old this.status==”waiting”) || (this.request!=null && this.location==this.destination && \old this.status==”service”) ==> this.status==”waiting”||
(count%20==0 &&\old this.status==”waiting”) || (count%20!=0 && (this.location==this.destination && \old this.status==”service” || this.location==this.source && \old this.status==”taking_order”)) ==> this.status==”still” ||
(this.request!=null && \old this.status==”waiting”) ==>this.status==”taking_order” ||
this.request!=null && \old this.status==”still” ==>this.status==”service”
　　對於MODIFIES邏輯錯誤，這是我第一次書寫是沒有通透jsf表達規範導致的------對於局部變量，即便它是最終的返回值，也不應該寫入MODIFIES中；
　　對於REQUIRES不完整，run()方法內部用到的變量都是對象內部的屬性，對於這個應不應該寫到REQUIRES中，我問到的同學有不同看法，我將我認為需要限制的變量取值給予了規定。
四．類規格的不佳寫法
1.自然語言vs布爾表達式(EFFECTS)
　　這兩個不用多說，大家都明白兩者優劣，布爾表達式勝在準確，但是一來歸納難，二來寫法難，特別是對於run方法，有些同學（包括我）run方法寫的比較長，對於變量的修改較多，此時使用布爾表達式，怕是光一個jsf就要寫幾十行。此時，簡單並且有極強概括性的自然語言就很好寫了，若幹行就能說明問題，但是此時需註意的就是布爾表達式針對變量進行總結，但是自然語言往往更加偏向於敘述程序做了什麽事情，容易寫成敘述算法的不合格的類規格。此處實例即為我的run方法：
　　改前：@EFFECTS：A taxi will run here
　　改後（針對status變量的部分）：@EFFECTS：
　　(this.request==null && count%20!=0 && \old this.status==”waiting”) || (this.request!=null && this.location==this.destination && \old this.status==”service”) ==> this.status==”waiting” ||
　　(count%20==0 &&\old this.status==”waiting”) || (count%20!=0 && (this.location==this.destination && \old this.status==”service” || this.location==this.source && \old this.status==”taking_order”)) ==> 　　　　this.status==”still” ||
　　(this.request!=null && \old this.status==”waiting”) ==>this.status==”taking_order” ||
　　this.request!=null && \old this.status==”still” ==>this.status==”service”

2.自然語言vs布爾表達式(REQUIRES)
　　相比於EFFECTS，REQUIRES的書寫較為簡單，REQUIRES只需要對變量做一個範圍的規範即可，但是這兩天也遇到了使用自然語言書寫REQUIRES的同學，自然語言中，“合適的”(proper)這個詞可以說是個萬金油的詞匯，什麽方法也可以說，請給我一個proper的參數……但是這確實不妥，每個參數都應該有確定的取值範圍（也即使用布爾表達式更為妥當）。
3.自然語言的表達
　　如果選擇自然語言表達，怎麽也應該表達地清楚明了吧……近兩次測試中我碰到了若幹完全讀不通的EFFECTS。我覺得EFFECTS要麽使用布爾表達式，要麽就用“流利”的英文來表達，對於無法使用布爾表達式表示的關系或者操作可以使用自然語言來代替。
五．思路以及體會
　　一開始聽到要寫jsf我是很拒絕的，但是迫於扣分壓力又不得不寫（廢話）。在經歷了若幹bug的洗禮，我也找到了一點自己寫規格的思路吧。
　　REQUIRES和MODIFIES其實不用說太多，對每一個函數仔細評估一下就能知道它需要的條件和要改變的變量。對於EFFECTS，我們應首先從MODIFIES下手，對於需要修改的變量，追蹤它的變化軌跡和可能的值，就能寫出它的布爾表達式了，而變量的變化過程其實比較像有限狀態機，從某一步到下一步都有相應的觸發條件，而這個條件和變化結果就是我們要寫的內容了。

第三次OO博客作業