面向对象设计与构造第三次总结做业

时间 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.