OO總結III
規格化設計的大致發展歷史
由於計算機誕生之初，並沒有編譯器操作系統這一類東西，也沒什麽高級語言，那時的程序員只能使用機器語言來編寫程序，後來為了方便程序員編寫又出現了助記符也就是匯編語言。
程序設計語言的三次分離使軟件技術產生飛躍
1950年代，第一次分離，主程序和子程序的分離
程序結構模型是樹狀模型，子程序可先於主程序編寫。通過使用庫函數來簡化編程，實現最初的代碼重用。產生基本的軟件開發過程：分析—設計—編碼—測試，使大型軟件系統的開發成為可能
1975—1980年代，第二次分離，規格說明（Spec）和體（body）的分離
說明是類型定義和操作描述，體是操作的具體實現。（具體的例子就是C++,Java等面向對象語言的類說明與類實現的分離。）解決方案設計只關註說明，實現時引用或者設計體。體的更改、置換不影響規格說明，保證了可移植性。支持多機系統，但要同樣環境。此時產生了劃時代的面向對象技術。
1995—2000年代，第三次分離，對象使用和對象實現的分離
基於構件開發：標準化的軟件構件如同硬件IC，可插拔，使用者只用外特性，不計內部實現。
Web Services：軟件就是服務。分布式，跨平臺，松耦合。
程序設計語言的第二次分離催生了規格化設計的誕生，規格化優點很多，故得到了人們的重視。
所被報告的規格bug
限於 bug樹的限制，對手無法上報？不存在的。想方設法給您報上去。
作業9
無
作業10
作業11
規格bug產生的原因
1.規格這種東西不是應該先寫了再實現函數體嗎？第七次作業寫了很多函數，第九次都要加上規格，自己不細心，總會有些遺漏的
2.新作業，新的需求，要改的函數有些多，自己不細心，總會有些遺漏的
3.對規格的要求理解不全面，自己不細心，總會有些遺漏的要求
4.測試者嚴以待人，我寬以待己，總會有些沒見過的規格要求
前置條件
不好寫法：
1.沒有指定範圍
@REQUIRES:i instanceof int && j instanceof int
2.沒有指定範圍
@REQUIRES:c instanceof Coordinate
3.邏輯優先級不對
@REQUIRES:num instanceof int&& num==1||num==3
4.=應為==
@REQUIRES:x=(xi,xj),y=(yi,yj);0<=xi<80&&0<=xj<80&&0<=yi<80&&0<=yj<80
5.類型描述不好
@REQUIRES:taxis instanceof Taxi[]
改進寫法：
1.
@REQUIRES:i instanceof int && j instanceof int && 0<=i<80 && 0<=j<80
2.
@REQUIRES:c instanceof Coordinate && 0<=c.i<80 && 0<=c.j<80
3.
@REQUIRES:num instanceof int && (num==1||num==3)
4.
@REQUIRES:x==(xi,xj),y==(yi,yj);0<=xi<80&&0<=xj<80&&0<=yi<80&&0<=yj<80
5.
@REQUIRES:\all int i;0<=i<taxis.length;taxis[i] instanceof Taxi
後置條件
不好寫法：
1.初始化用自然語言
@EFFECTS:
initialize the new Taxi
2.沒有對異常行為進行說明
@EFFECTS: norma_behavior(\result == selectdire.get(Rand(0,selectdire.size)));
3.沒有使用\old
@EFFECTS:
\result == true;responlist.size == responlist.size+1;responlist.contains(num));
4.過於簡略
@EFFECTS:set the graph
改進寫法：
1.
@EFFECTS: this.taxinum == taxinum; this.position == TaxiRandom.getPosition(80); this.credit == 0; this.dire == RoadPlan.DirectionSeek(80, this.position); this.status == TaxiStatus.Waiting; this.statusnum == 2; this.psg == null;
2.
@EFFECTS: norma_behavior(\result == selectdire.get(Rand(0,selectdire.size))); exception_behavior(throw IllegalArgumentException)
3.
@EFFECTS: \result == true;responlist.size == \old(responlist).size+1;responlist.contains(num));
4.
@EFFECTS: \all int i,j;0<=i<Map.map.length&&0<=j<Map.map[i].lenght;Map.map[i][j] == 1 || Map.map[i][j] == 3 ==> Map.graph[i * 80 + j][i * 80 + j + 1] == true;Map.graph[i * 80 + j + 1][i * 80 + j] == true; \all int i,j;0<=i<Map.map.length&&0<=j<Map.map[i].lenght;Map.map[i][j] == 2 || Map.map[i][j] == 3 ==> Map.graph[i * 80 + j][(i + 1) * 80 + j] == true;Map.graph[(i + 1) * 80 + j][i * 80 + j] == true;
功能bug與規格bug
功能bug和規格bug似乎沒有很直接的聚集關系，畢竟我們的流程是寫了函數才加的規格，出現規格bug大概是方法修改後規格改得不仔細。但是，越長的函數確實是越可能既出現規格bug又出現功能bug的。
設計規格和撰寫規格的基本思路和體會
首先想想方法的應用場景和方法內實現功能的要求，確定方法的Require，確定方法參數的範圍；
細化方法要實現的功能，確定方法會更改的屬性，確定Modifies；
根據已有函數編寫EFFECTS，我想大家可能都是這樣的吧，先實現了功能再來寫規格，但課程的設置就會導致這樣的結果，我覺得是作業的一大缺陷之一，並不是很符合設計規格和撰寫規格的流程。
測試者對規格的要求千變萬化，有時候測試者自己都不動腦子，None有沒有寫也要扣，System.out也說要加入Modifies，非要助教給了答復才撤銷。
我不是針對誰，我是說這種就是垃圾。
我覺得作業上規格帶給我的收獲遠遠不如實驗課上那兩個多小時來得多，作業的規格費時費心，互測上還讓人不開心，（互測使人抑郁也是賴不著課程組的）。
老師也說了，IFTTT這次作業可有可無？為啥不用這次作業來好好地訓練一下規格化的思想？
這三次OO互測的體會
誰愛開心誰開心
OO總結III