oo第十二次做業

1、規格化設計的大體發展歷史

規格是紮根於形式化的設計方法而產生的。

最初的軟件形式化方法源於二十世紀五十年代，及軟件工程這一律念剛剛開始興起的時代，對於工程間的協調管理，人們提出採用工程方法來組織、管理軟件的開發過程並深刻探討程序和程序開發過程的規律，創建嚴密的理論。這一結構發展至今，規格已經造成一套完整的邏輯體系並融入軟件開發的各個步驟，,從需求分析、功能描述(規約)、(體系結構/算法)設計、編程、測試直至維護。

在二十世紀七十年代，規格產生了第二次分離，這一分離主要是針對於說明和體的分離，並開始出現先後置協調的雛形。這一次的分離使得規格能夠更好的區分置換條件，以適應新興的跨時代面向對象技術。

二十一世紀初期開始，規格基本完善成現在的形式，並更加側重於基於構件的對象使用和對象實現。應用現有的規格規範，軟件能夠輕鬆的實現分佈式，跨平臺，鬆耦合的開發需求。

形式化方法的研究和應用已經有40多年的歷史了，其產生是Dijkstra和Hoare在程序驗證方面的工做和Scott，Stratchey以及其餘學者在程序語義方面的工做基礎上發展起來的，從最簡單的形式化方法到80年代較爲複雜的Z語言，直至造成具備表明性的形式規範語言——面向實時及分佈式的LOTOS語言和麪向對象的Z++語言等。形式化方法已經造成了較爲完整的體系。

早期的形式化方法主要侷限於程序的形式化驗證，早期的規範語言中，有兩種有表明性的，由工具支持的語言是AFFIRM語言和OBJ語言，主要功能也是進行程序驗證。80年代產生了Z語言和VDM語言這兩種形式語言，它們都是基於模型的形式規範語言，它們有一個共同的弱點是較難肯定該語言描述的軟件整體結構和範圍。80年代末期，形式化方法發展中的另外一個有表明性的方向是對代數方法和軟件技術結合的AMAST研究，HartmutEhrig領導研究並創造了ACT方法，開發了相應的使用環境。此外，使用代數方法的規範與語言還有一些較有影響的語言，好比PLUSS和FOOPS等。

 

2、規格BUG

做業次數	規格bug	名稱
9（無效）
10	1	Effects不完整
11	0

第十一次做業中JSF依然有不規範的地方，不過給我測試的同窗放了我一馬，十分感謝。不規範的列在下面。

1.Effects不完整：

 /**
    * Requires:none;
    * Modifies:timelis;
    * Effects:timelis. add(request.time);
    **/ 
改正後：
 /**
    * Requires:none;
    * Modifies:timelis,request;
    * Effects:timelis.conclude(request.time) == true && timelis.size()++;
    **/ 

2.沒有對變量進行限制：

　/**
　　* Requires:none;
　　* Modifies:guigv.taxilist.get(taxi).x,guigv.taxilist.get(taxi).y;
　　* Effects:x = x1 ; y = y1 ;
　　**/

改正後：

　/**
　　* Requires:x1 != null && y1 != null;
　　* Modifies:guigv.taxilist.get(taxi).x,guigv.taxilist.get(taxi).y;
　　* Effects:x = x1 ; y = y1 ;
　　**/

3.使用天然語言：

/**
     * Requires:txt.nextline() != null;
     * Modifies:Line;
     * Effects:read txt;
    **/

改正後：
/**
     * Requires:txt.nextline() != null;
     * Modifies:Line;
     * Effects:Line.add(txt.nextline()) && Line.size()++;
    **/

4.沒有將異常處理寫入Efficts

 /**
    * Requires:none
    * Modifies:Main.gui.SetLightStatus()
    * Effects:taxi.status = status;
    **/

改正後：
 
/**
    * Requires:none
    * Modifies:Main.gui.SetLightStatus(new Point(i,j), 2)
    * Effects:taxi.status = status || exceptional_behavior(xxx);
    **/

3、規格bug分析：

因爲沒有透徹理解規格的正確寫法和做用，致使規格的寫法很簡陋，並且不能清楚表達本身的意思。常用天然語言，同時常常會有各類遺漏。主要緣由是還不夠熟練，代碼水平也不夠高，不能徹底實現本身想要的功能。

4、心得體會：

相比於以前的做業，我認爲本身仍是有了進步的，可是仍然還和其餘同窗有很大的差距。我認爲首先還得在設計階段就不斷完善本身的想法，不能埋頭就開始寫。還須要再加以勤奮的練習，但願勤能補拙，向優秀的同窗靠攏。