面向對象設計與構造第三次總結做業

時間 2019-12-04

原文原文鏈接

規格化設計的發展歷史

　　Specification一詞可追溯到16世紀末，但直到20世紀50年代才得以普遍使用。在軟件工程領域，上世紀70年代左右就有關於規格化設計的研究。
程序員

　　1975年，Liskov等人發表了論文Specification Techniques for Data Abstractions，從數據抽象的角度論述了規格的優勢、特性及重要性。文中主要討論的是形式化的規格，Liskov認爲形式化規格多是程序開發所固有的特徵，對於數據抽象是頗有用處的。形式化規格的優勢主要有：①驗證程序的正確性，②幫助程序員理解程序代碼，③在程序開發過程當中具備重要做用，④規格是設計者與實現者、程序員之間溝通的媒介。任何的規格都應該知足6個標準：正式（Formality）、可構造（Constructability）、易於理解（Comprehensibility）、最小化（Minimal）、普遍的適用性（Wide range of applicability）、可擴展型（Extensibility）。編程

　　1976年，在第二屆國際軟件工程會議上，Belford等人在Specifications a key to effective software development一文中從開發複雜系統的角度論證了完整的、一致的規格的重要性。在系統研發週期中，規格提供了在概念和定義階段的過渡。一個清楚、無歧義的規格是取得成功的關鍵，同時能減小開發過程當中的開銷。軟件需求自己具備模糊的特色，因此須要一個定義明確的規格來開發出可靠的軟件。該論文的研究成果出自於美國國防部彈道導彈高級技術中心的一個課題。數組

　　上世紀70年代是第四代計算機出現的階段，硬件採用了大規模集成電路，軟件方面出現了面向對象編程語言，從那時起計算機變得更加通用，從科學計算等應用逐步走向家庭應用。app

　　1993年，Liskov等人發表了Specifications and their use in defining subtypes，從類型層次的角度進一步論證了規格的重要性。論文提到了封裝的必要性，它可使修改某種類型的實現時，該類型的使用者不會受到影響，由於新實現的類與原來的類有着一樣的行爲，可是問題在於怎麼說明新的「行爲」與所須要的行爲是一致的呢？她認爲舊的實現不能算做定義，由於其包括太多細節。所以須要一種獨立於實現的東西，它可以描述行爲，這就是規格。其實，在那個時候，規格一直是數據抽象編程方法學的奠定石，只是在實際使用面向對象編程時沒有獲得太多的關注。編程語言

　　論文使用了Larch形式化規格語言，該語言在同年出版的《Larch: Languages and Tools for Formal Specification》一書中被普遍地推廣。早在1973年，Liskov就組織了一個編程語言的討論會，會上受Steve Zilles的啓發，該書的做者們提出了對抽象數據類型的操做均可以用代數方法，用簡單的等式來表示，因而他們考慮是否能將其運用到規格之上。但在1974年，他們認識到用純粹的代數方法來表示規格是不切實際的。早期的Larch語言於1983年發佈，後來在1985年第一次出版了全面的關於Larch語言的描述。儘管你們作了不少努力，在那時，「Larch in Five Easy Pieces」被讀者們稱爲「Larch in Five Pieces of Varying Difficulty」，可見當時Larch語言不是很易於接受。到了1990年，一些關於Larch的軟件工具開始出現，可用於規格的檢查和推理。後來就有了愈來愈多的工具可供使用。ide

bug分析

1.bug記錄表格工具

類型	方法代碼行數	產生緣由
Requires邏輯錯誤	8	複製粘貼後忘了修改
Requires不完整	五、九、1四、1五、30、3一、32	沒有注意到一些限制條件，一些方法沒有寫規格
Modifies不完整	1四、1五、30、3一、32	一些方法沒有寫規格
Effects不完整	1四、1五、30、3一、32	一些方法沒有寫規格
紅綠燈編碼錯誤	沒有方法	規格寫得不完整，編碼時疏忽

2.功能bug與規格bug彙集關係分析ui

方法名	功能bug數	規格bug數
opposite()	0	1
getPoint()	0	1
Request()	0	1
run()	0	5
main()	0	1
無	1	0

從表格中可見，功能bug數和規格bug數相關性不大，可能須要對更多程序的分析才能得出更準確的結論。this

前置條件與後置條件很差的寫法

1.出租車接收訂單的一個方法編碼

1 /**
2  * @REQUIRES: scheduler != null; order != null;
3  * @MODIFIES: this;
4  * @EFFECTS:  This taxi is ready to take order;
5  * @THREAD_EFFECTS: \locked(this);
6  */

　後置條件比較模糊，能夠寫得更明確些。改進以下：

1 /**
2  * @REQUIRES: scheduler != null; order != null;
3  * @MODIFIES: this;
4  * @EFFECTS:  this.status == TaxiStatus.WAITING ==> (this.order == order && this.orderReady == true && \result == true);
5 　　　　　　　　 this.status != TaxiStatus.WAITING ==> \result == false;
6  * @THREAD_EFFECTS: \locked(this);
7  */

2.出租車處於等待狀態的方法

1 /**
2  * @REQUIRES: this.status == TaxiStatus.WAITING;
3  * @MODIFIES: this;
4  * @EFFECTS: this taxi waits for 20 seconds;
5  */

後置條件寫得比較模糊,改進以下：

/**
 * @REQUIRES: this.status == TaxiStatus.WAITING;
 * @MODIFIES: this;
 * @EFFECTS: this taxi waits for 20 seconds;
 * !orderReady during 20 seconds ==> status = TaxiStatus.STOPED;
 */

3.出租車接單的方法

/**
 * @REQUIRES: passenger != null;
 * @MODIFIES: this;
 * @EFFECTS: this.position == passenger;
 *            passenger has got in this taxi;
 *             \result == the time when passenger gets in this taxi;
 */

前置條件不夠完整，除了規定乘客位置不爲null外，還應該限定位置的範圍。

/**
 * @REQUIRES: passenger != null; 0 <=  passenger.x < 80 &&  0 <=  passenger.y < 80;
 * @MODIFIES: this;
 * @EFFECTS: this.position == passenger;
 *               passenger has got in this taxi;
 *               \result == the time when passenger gets in this taxi;
 */

4.尋找最高信用出租車的方法

/**
 * @REQUIRES: taxiList != null; !taxiList.isEmpty();
 * @MODIFIES: taxiList;
 * @EFFECTS: \result == taxiList裏信用最高的出租車們;
 */

後置條件能夠寫得更加嚴謹一些，改進以下：

/**
 * @REQUIRES: taxiList != null; !taxiList.isEmpty();
 * @MODIFIES: taxiList;
 * @EFFECTS: (\all Taxi t; \result.contains(t); \all int i; 0 <= i < taxiList.size; t.credit >= taxiList[i].credit);
 * (\all Taxi t; \result.contains(t); taxiList.contains(t));
 * (\all int i, j; 0 <= i < j < taxiList.size; taxiList[i].credit >= taxiList[j].credit);
 */

5.根據編號得到某個出租車對象的方法

/**
 * @REQUIRES: 0 <= id < 100
 * @MODIFIES: None;
 * @EFFECTS: \result == taxi whose id equals parameter id;
 */

後置條件不許確，改進以下：

/**
 * @REQUIRES: 0 <= id < 100
 * @MODIFIES: None;
 * @EFFECTS: \result.id == id; this.taxis.contains(\result);
 */

6.獲取指定狀態的出租車編號的方法

/**
 * @REQUIRES: status != null;
 * @EFFECTS: \result == 狀態爲status的全部出租車編號數組;
 */

後置條件不許確，且比較侷限。改進以下：

/**
 * @REQUIRES: status != null;
 * @EFFECTS: (\all Taxi t; \result.contains(t.id); t.status == status);
 * (\all Taxi t; \result.contains(t.id); this.taxis.contains(t.id));
 */

7.出租車送乘客到目的地的方法

/**
 * @REQUIRES: dest != null; dest != order.passenger; 
 *            pseudoTime == the time when passenger got in this taxi;
 * @MODIFIES: this;
 * @EFFECTS: this.position == dest;
 *                this.credit == \old(this.credit) + 3;
 */

前置條件不完整，改進以下：

/**
 * @REQUIRES: this.status == TaxiStatus.SERVING; 
 *                    dest != null; dest != order.passenger; 
 *            pseudoTime == the time when passenger got in this taxi;
 * @MODIFIES: this;
 * @EFFECTS: this.position == dest;
 *                this.credit == \old(this.credit) + 3;
 */

8.添加行車記錄的方法

/**
 * @REQUIRES: position != null;
 * @MODIFIES: this;
 * @EFFECTS:     (\all (Long, Position) (time, position); 
 * \old(this.record).contains((time, position) ==> this.record.contains((time, position));
 *    this.record.contains((time, position));
 * @THREAD_EFFECTS: \locked();
 */

前置條件不完整，改進以下：

/**
 * @REQUIRES: position != null; time != null; 0 <= position.x < 80; 0 <= 
 * position.y < 80;
 * @MODIFIES: this; 
 * @EFFECTS:     (\all (Long, Position) (time, position); 
 * \old(this.record).contains((time, position) ==> this.record.contains((time, 
 * position));
 *    this.record.contains((time, position));
 * @THREAD_EFFECTS: \locked();
 */

9.判斷可否經過紅綠燈的方法

/**
 * @EFFECTS: \result == whether the taxi at pos could pass from 'from' to 'to';
 * @THREAD_EFFECTS: \locked();
 */

前置條件對的要求能夠寫到EFFECTS裏，拋出一個異常。

/**
 * @EFFECTS: \result == whether the taxi at pos could pass from 'from' to 'to';
 * pos == null || from == null || to == null ==> exceptional_behavior(NullPointerException);
 * !(0 <= pos.x < 80 && 0 <= pos.y < 80) ==> exceptional_behavior(IllegalPositionException);
 * @THREAD_EFFECTS: \locked();
 */

10.管理出租車的類的一個方法

/**
 * @REQUIRES: taxi != null;
 * @MODIFIES: this;
 * @EFFECTS: this.taxi.contains((taxi.id, taxi));
 */

前置條件不完成，應該對出租車編號進行限定。

/**
 * @REQUIRES: taxi != null; 0 <= taxi.id < 100;
 * @MODIFIES: this;
 * @EFFECTS: this.taxi.contains((taxi.id, taxi));
 */

撰寫規格的體會

　　某一次做業中要求改變道路流量的計算方式，乍一看須要修改不少地方，好比有個int getFlow(Point p, Point q)方法，用來獲取兩個點之間的流量，規格以下：

/**
 * @REQUIRES: p != null; q != null; 0 <= p.getX() < 80; 0 <= p.getY() < 80;
 *                0 <= q.getX() < 80; 0 <= q.getY() < 80; p.nextTo(q);
 * @MODIFIES: None;
 * @EFFECTS: \result == the flow of road between q and q;
 * @THREAD_EEFECTS: \locked(flows);
 */

　　後來發現只須要在管理流量的類中修改流量的更新方法，獲取流量的方法例如getFlow()，可是在調用這些方法的地方，例如出租車查詢道路流量，就不須要作修改，仍是老樣子。可見規格與抽象的好處，就像Liskov老太太說的那樣:

可修改性(modifiability)——可以實現一個抽象，而不須要更改任何使用該抽象的其餘抽象。

參考文獻

[1]Barbara Liskov and Stephen Zilles. 1975. Specification techniques for data abstractions. In Proceedings of the international conference on Reliable software. ACM, New York, NY, USA, 72-87. DOI=http://dx.doi.org/10.1145/800027.808426

[2]P. C. Belford, A. F. Bond, D. G. Henderson, and L. S. Sellers. 1976. Specifications a key to effective software development. In Proceedings of the 2nd international conference on Software engineering (ICSE '76). IEEE Computer Society Press, Los Alamitos, CA, USA, 71-79.

[3]Barbara Liskov and Jeannette M. Wing. 1993. Specifications and their use in defining subtypes. In Proceedings of the eighth annual conference on Object-oriented programming systems, languages, and applications (OOPSLA '93). ACM, New York, NY, USA, 16-28. DOI=http://dx.doi.org/10.1145/165854.165863

[4]John V. Guttag and James J. Horning. 1993. Larch: Languages and Tools for Formal Specification. Springer-Verlag, Berlin, Heidelberg.

[5]Barbara Liskov,John Guttag.程序開發原理:抽象、規格與面向對象設計[M].裘健，譯.北京:電子工業出版社,2006:25.