OO第三次總結
OO第三次總結
規格化設計的發展歷史和受到重視的原因
? 20世紀60年代，軟件出現嚴重的危機，Dijkstra於1968年發表著名的《GOTO有害論》，由此引發了軟件界長達數年的論戰，並產生了結構化的程序設計方法。隨著計算機技術的發展，結構設計化語言和結構化分析已經無法滿足用戶的需求，OOP由此應運而生，即面向對象的程序設計。面向對象程序設計的誕生是程序設計方法學的一場革命，大大提高了開發效率，減少了軟件開發的復雜度，提高了軟件的可維護性，可擴展性。1990年以來，面向對象分析、測試、度量和管理研究都得到長足的發展。規格化設計隨其而生，為了提高程序的規範性，對類。方法等進行規範化設計，有利於模塊化的劃分。最實際的，通過規格化設計，在進行大型多人的開發工作時，可以確保程序員之間能夠便捷地在他人的基礎之上開始自己的工作，大大提高了工作效率，也方便他人理解代碼，所以受到了大家的重視。
規格bug分析
| Bug類型 | 出現位置 | 方法行數 |
|---|---|---|
| Effects不完整 | mapInfo類point2N函數 | 5 |
| Modifies邏輯錯誤 | Taxi類refreshGUI函數 | 11 |
產生規格bug的原因
protected void refreshGUI() {
/**
* @REQUIRES: None;
* @MODIFIES: None;
* @EFFECTS: None;
* @THREAD_EFFECTS: \locked(readWriteLock.readLock);
*/
readWriteLock.readLock 在這個函數中我忽略了調用gui方法時會更改gui，更改如下：
/**
* @REQUIRES: None;
* @MODIFIES: gui;
* @EFFECTS: gui.SetTaxiStatus(No,currentPos,tempStatus);
* @THREAD_EFFECTS: \locked(readWriteLock.readLock);
*/ private int point2N(Point point) {
/**
* @REQUIRES: point != null;
* @MODIFIES: None;
* @EFFECTS: \result == point.x * mapSize + point.y;
*/
if (point == null) {
System.out.println("ERROR : NULL POINTER!");
return 0;
}
return point.x * mapSize + point.y;
}這裏返回值忽略了point=null時為0的情況，更改如下：
/**
* @REQUIRES: point != null;
* @MODIFIES: None;
* @EFFECTS: \result == point.x * mapSize + point.y && point != null
* || \result == 0 && point == null;
*/改進規格
1.mapInfo 類的 refreshMap 函數
public void refreshMap(int[][] map, TaxiGUI gui) {
/**
* @REQUIRES: map!=null;
* @MODIFIES: this.map;gui;
* @EFFECTS: this.map == map;
*/
readWriteLock.writeLock().lock();
this.map = map;
if (this == instance) {
gui.LoadMap(map, mapSize);
}
readWriteLock.writeLock().unlock();
}在這個方法中要載入一張新的地圖，這時需要對地圖大小進行判斷，否則如果map僅僅非空，大小不正確可能導致後續程序崩潰。更改如下：
/**
* @REQUIRES: map!=null && map.length == MAPSIZE
* && (\all Integer i; i<MAPSIZE && i>=0; map[i].length == MAPSIZE);
* @MODIFIES: this.map;gui;
* @EFFECTS: this.map == map;
*/2.MapFlow 類的 setMapFlow 方法
public void setMapFlow(ArrayList<Point> p1s, ArrayList<Point> p2s, ArrayList<Long> values) {
/**
* @REQUIRES: p1s!=null;p2s!=null;values!=null;
* @MODIFIES: edgeFlows;
* @EFFECTS: None;
*/
readWriteLock.writeLock().lock();
for (int i = 0; i < MapSize*MapSize*2; i++) {
edgeFlows[i] = new EdgeFlow();
}
for (int i = 0; i < p1s.size(); i++) {
int n = Point2N(p1s.get(i), p2s.get(i));
if (map.isConnected(p1s.get(i), p2s.get(i))) {
edgeFlows[n].flow = values.get(i);
}
}
readWriteLock.writeLock().unlock();
}在這個方法的 JSF 中僅要求了三個列表參數非空，但是在函數實現時沒有判斷列表長度為零或三個列表不等長的情況。更改如下：
/**
* @REQUIRES: p1s!=null && p2s!=null && values!=null
* && p1s.size() > 0
* && p2s.size() == p1s.size() && values.size() == p1s.size();
* @MODIFIES: edgeFlows;
* @EFFECTS: None;
*/3.RequestMatrix 類的 isSame 方法
public synchronized boolean isSame(ReqSchedular req) {
/**
* @REQUIRES: request!=null;
* @MODIFIES: None;
* @EFFECTS: requestSchedular.equals(request);
*/
for (ReqSchedular reqSchedular : reqMatrix[req.Src().x][req.Src().y].reqList)
{
if (reqSchedular.equals(req)) {
return true;
}
}
return false;
}這裏是首次寫規格時不熟悉遺留下的錯誤，缺少鎖的影響且返回值格式不正確，更改如下：
/**
* @REQUIRES: request!=null;
* @MODIFIES: None;
* @EFFECTS: \result == true ==>
* ( \exist ReqSchedular reqS;
* reqMatrix[req.Src().x][req.Src().y].reqList.contains(reqS);
* reqS.equal(req) )
* @THREAD_EFFECTS: \locked(this);
*/4.MapFlow 類的 updateEdgeFlow方法
public void updateEdgeFlow(Point p1, Point p2, long value) {
/**
* @REQUIRES: p1!=null;p2!=null;value!=null;
* @MODIFIES: edgeFlows[n];
* @EFFECTS: None;
*/
if (p1.equals(p2))
return;
int n = Point2N(p1, p2);
if (map.isConnected(p1, p2)) {
readWriteLock.readLock().lock();
edgeFlows[n].readWriteLock.writeLock().lock();
edgeFlows[n].flow = edgeFlows[n].flow + value;
edgeFlows[n].readWriteLock.writeLock().unlock();
readWriteLock.readLock().unlock();
}
}更改為：
/**
* @REQUIRES: p1!=null;p2!=null;value!=null;
* @MODIFIES: edgeFlows[n];
* @EFFECTS: n = Point2N(p1, p2) && edgeFlows[n].flow == \old(edgeFlows[n].flow) + value;
* @THREAD_EFFECTS: \lock(readWriteLock.readLock);
* \lock(edgeFlows[n].readWriteLock.writeLock)
*/5.FlowThread 類 run方法
public void run() {
/**
* @REQUIRES: p1 != null && p2 != null;
* @MODIFIES: None;
* @EFFECTS:None;
*/
try {
if (p1.equals(p2))
return;
try {
sleep(FlowTimeWindow);
} catch (InterruptedException e) {
// TODO Auto-generated catch block
//e.printStackTrace();
System.out.println("Flow Thread : sleep crash! ");
}
mapFlow.updateEdgeFlow(p1, p2, -1);
} catch (Exception e) {
System.out.println("Flow Thread Exception!");
}
}改為：
/**
* @REQUIRES: p1 != null && p2 != null;
* @MODIFIES: None;
* @EFFECTS: !p1.equals(p2) ==> (sleep(FolwTimeWindow) && mapFlow.updateEdgeFlow(p1,p2,-1));
*/分析被報的功能bug與規格bug在方法上的聚集關系
? 在互測中被挑出的功能bug和規格bug關聯並不大，可能是筆者剛剛接觸JSF，有許多函數方法功能可以正確實現但是功能並不完善，所以被找了規格bug，筆者認為互測階段被報的大量 JSF 的bug往往是測試者刻意為之（當然我也承認書寫不夠規範）。功能bug往往是比較復雜的函數中存在邏輯漏洞，這類函數的規格比較復雜，可能存在邏輯錯誤，但測試者並沒有仔細分析，所以大多沒有報JSF bug。我想這也是這種測試機制存在的一些問題，被測出的規格問題並不能反映程序的功能實現問題，而對於復雜函數，被測者通過寫規格為做出的優化，也很少通過測試反映出來。
設計規格和撰寫規格的基本思路和體會
? 寫規格可以強制要求程序員降低簡化每個成員方法的復雜度，在寫程序之前能夠明確一個方法的具體作用和影響，對程序作者和讀者而言都是一個明確、嚴謹的說明。但有的時候一些邏輯不好表述的過程的確很難寫出簡潔的規格，甚至讓規格比代碼還長。在一些開源代碼中，許多規格都是一些自然語言的註釋，反而更讓人清晰的理解一個方法的作用。在我個人看來，用布爾表達式書寫的規格在有些情況下是比較冗余，且難懂的，雖然從邏輯上可能會更準確。另外對於OO課程的 JSF 測試部分，我認為並沒有達到很好的效果，許多人的惡意挑錯反而降低了同學們的學習積極性。
OO第三次總結