标签：lock manage find 构造 算法实现 obj main int passenger
软件工程的重要目标之一是实现软件开发过程各阶段的自动化，软件自动化的前提是形式化,包括软件需求规格的形式化、软件设计规格的形式化和 算法描述的形式化。
Z语言由牛津大学程序设计研究小组开发，是一种应用较为广泛的形式规格说明语言，它以一阶谓词逻辑和集合论为基础对软件系统的静态特征和动态特征进行形象描述。
面向对象技术在系统分析设计，程序设计等方面所能提供的类层次，整体-部分关系，封装性，继承性使得其得到了广泛应用。因而人们也开始研究面向对象软件的形式规格描述问题。
从90年代初开始，国际上对Z语言的面向对象扩展相继提出了MOOZ，Object-Z,Z++等方案，将Z语言扩展到能够支持面向对象的系统分析方法上来。
到现在，面向对象规格化设计理论进一步丰富。比如
可见，规格化设计是开发大型软件项目必不可少的技术手段，学习规格化设计是重要且必要的。
[1] Hoare, C. A. R. “An Axiomatic Basis for Computer Programming.” Communications of The ACM, vol. 12, no. 10, 1969, pp. 576–580.
[2] Guttag, John V., et al. “Abstract Data Types and Software Validation.” Communications of The ACM, vol. 21, no. 12, 1978, pp. 1048–1064.
[3] Felleisen, Matthias, and Robert Bruce Findler. Behavioral Interface Contracts for Java. 2000.
第九次作业：
| 编号 | 类别 | 所在方法 | 方法代码行数 |
|---|---|---|---|
| 1 | Modifies逻辑错误 | main方法 | 37 |
测试者认为Main方法的Modifies不应为None.但是我认为整个出租车系统对Main方法来说都是内部的，也就是没有修改外部的属性，Main方法也没有修改传入的参数，所以Modifies为None我觉得是合理的。还在仲裁中。
第十次作业:
无
第十一次作业：
| 编号 | 类别 | 所在方法 | 方法代码行数 |
|---|---|---|---|
| 1 | Modifies不完整 | Map类的构造器 | 8 |
| 2 | Modifies逻辑错误 | Map类createMap | 30 |
1是因为构造器修改了自身的属性，写Modifies没有写全。出现这个问题是因为在本次作业中，对地图的构造方法进行了修改，但是遗漏了规格的更新。
2是因为createMap的MODIFIES里有多余的内容。方法内部并没有修改某个属性，但MODIFIES里写了。也是因为本次作业修改了方法，却遗漏了规格的更新。
| 编号 | 方法 | 原写法 | 改进写法 |
|---|---|---|---|
| 1 | Car: driving() | None | this.map instanceof Map |
| 2 | Car: waiting() | None | this.c_map instanceof TaxiGUI |
| 3 | Car: toCus() | None | this.p instanceof Passenger; this.map instanceof Map |
| 4 | CarInfo: toString() | None | this.info != null; |
| 5 | InputHandler: loadFlow(BufferedReader br) | br!=null | br!=null; this.map instanceof Map; |
| 编号 | 方法 | 原写法 | 改进写法 |
|---|---|---|---|
| 1 | Map: findShortestPath(int start, int end, int car_type) | the map is a connected graph==>\result == path where path is a Vector containing the shortest path from point start to point end with the minimum car flow; | \result.get(0)==start && \result.get(\result.size-1)==end && (\all int i; 0<=i<=\result.size-2;isAjacent(\result.get(i), \result.get(i+1)))&& (\all Vector v; v.get(0)==start && v.get(v.size-1)==end && (\all int i;0<=i<=v.size-2;isAjacent(v.get(i),v.get(i+1)));v.size>=\result.size); |
| 2 | Map: run | 500ms after starting, decrease the value of every element in \this.flow by value of the corresponding element in \this.original_flow; | \all int i,j;0<=i,j<80;flow[i][j]==\old(flow[i][j])-original_flow[i][j]; |
| 3 | OrderTrace: cusEndPoint() | \result == Point t that represents the customer‘s destination; | \result.getX()==p.getDes()/80 && \result.getY()==\p.getDes()%80; |
| 4 | OrderTrace: cusStartPoint() | \result == Point t that represents the customer‘s position; | \result.getX()==p.getStart()/80 && \result.getY()==\result.getStart()%80; |
| 5 | PassengerQueue: 构造方法 | \this.customers == new LinkedBlockingQueue(); | \this.customers instanceof LinkedBlockingQueue(); |
第九次作业：
| 方法名 | 功能bug | 规格bug |
|---|---|---|
| main | 1 | 1 |
第十次作业：
| 方法名 | 功能bug | 规格bug |
|---|---|---|
| InputHandler: loadMap | 1 | 0 |
| LightManager: run | 1 | 0 |
| LightManager: init | 1 | 0 |
| Car: takePassenger | 1 | 0 |
第十一次作业：
| 方法名 | 功能bug | 规格bug |
|---|---|---|
| Car: waitForLight | 1 | 0 |
| Map: 构造方法 | 0 | 1 |
| Map: createMap | 0 | 1 |
| Map: run | 1 | 0 |
先确定好这个方法的输入和输出, 确定方法内需要用到的数据结构。根据方法用到的算法，在草稿纸上演算一遍，确认只需要这些输入就可得到想要的结果。
然后根据输入确定REQUIRES,根据结果确定EFFECTS，根据EFFECTS确定MODIFIES。
标签：lock manage find 构造 算法实现 obj main int passenger
原文地址：https://www.cnblogs.com/9998-0804/p/9104556.html
