要了解规格化设计首先要了解抽象化的程序设计,二者是密不可分的。java
抽象化是将数据与程序,用语义呈现他们的外观,可是隐藏起它的实现细节。程序员
抽象的过程能够看作多对一的映射,让咱们忽略个体信息,将不一样事物当作相同的事物对待,可以减小程序的复杂度,使得程序员能够专一在处理少数重要的部分。算法
近几年来,程序员对已经产生的抽象水平产生不满,甚至不知足于在高级语言程序中广泛实现的抽象水平,解决这个问题的方法在于创造“更高级的语言”,用相对固定的数据结构以及有很强功能的原始类型来实现,可是这种方法的缺陷在于嘉定编程语言的设计者在设计语言的时候将大多数用户须要的抽象设计引进设计语言中,包含如此众多的内置抽象的编程语言可能笨拙的很难使用。编程
另外一种可取代的方法是设计一种语言机制,容许程序员在须要的时候构建本身的抽象方法。一般的机制是使用过程(procedure)。编程语言包含了两种重要的抽象方法:参数化抽象(abstraction by parameterization)和规格化抽象(abstraction by specification)。其中:数组
程序设计中,抽象类别包括下列4类:数据结构
1:过程抽象:可以引入一些新的操做;dom
2:数据抽象:可以引入新的数据对象类型;编程语言
3:反复运算抽象:可以反复运算遍历在集合中的元素,而没必要显示如何得到元素的细节;ide
4:类型层次:可以从多个单独的数据类型中抽象成几组相关的类型。函数
抽象用于将一个程序分解为多个模块,然而抽象是无形的,没有描述,咱们就没法知道如何将它与其实现的抽象区分。规格描述了服务的提供者和用户之间的协定,提供者赞成编写一个属于规格知足集的模块。
规格是对一个方法/类/程序的外部可感知行文的抽象表示,它的目的是为了定义抽象的行为。
若是一个实现提供了所描述的行为,这个实现就知足了一个规格。
规格的含义是知足其全部程序的集合,这个集合称为规格知足集。
此处为本身统计的bug,因为报告的jsf个数有限,本身从新看了一次仍是发现了许多bug和不规范的地方。
bug类别 | Requires不完整 | Modifies不完整 | Effects不完整 | Requires逻辑错误 | Modifies逻辑错误 | Effects逻辑错误 | Effects内容为实现算法 | 不符合JSF |
---|---|---|---|---|---|---|---|---|
个数 | 7 | 3 | 5 | 0 | 0 | 2 | 0 | 0 |
方法行数 | 3,5,5,13,22,20,4 | 5,7,7 | 20,30,15,17,15 | 30,15 |
一、有些方法或者类的JSF遗漏
好比本身写的Exception类里面忘记写JSF,一些信息存储的类里面的构造方法有时候也会忘记写,仍是本身不够细心。
二、没有按照标准格式书写
Effects以后的内容应该为布尔表达式。像是代码中出现的(\result = str),这种里面的=应该写成==
三、程序里面一些传入对象的方法,对应的Requires有的没写。
有传入仍是应该写明有Requires的要求,好比传入对象不等于null,或者对象的repOK 为ture之类。
四、某些过程会有附加的隐式输入,例如读入文件和在System.out写信息,这些也属于过程的输入
五、仍是偷了不少懒。。
有些例子前置条件和后置条件一块儿修改了。
一、前置与后置条件:
public int getDirection(Coordinate now, Coordinate next){ /** * @REQUIRES: None; * @MODIFIES: None; * @EFFECTS: (next.getX()-now.getX()==1&&next.getY()-now.getY()==0)==>(\result = 0); (next.getX()-now.getX() == -1 && next.getY()-now.getY()==0)==>(\result = 1); (next.getX()-now.getX() == 0 && next.getY()-now.getY()==1)==>(\result = 2); (next.getX()-now.getX()== 0 &&next.getY()-now.getY() == -1)==>(\result = 3); * @THREAD_REQUIRES: * @THREAD_EFFECTS: */ }
这里输入的两个坐标分别是当前坐标和下一步的坐标,这两个坐标须要知足的条件是在地图上是相邻的,因为可能出现道路忽然断开的情况,因此两个坐标的链接状态未知,当时想着在代码里面处理了这种异常情况因此没有写requires,可是其实也能在requires中体现,而后在代码中处理这种状况,抛出异常或者返回等操做,若是不写的话也要加入两个坐标不为空,有输入最好要限制其内容,什么都不写不是一种好的习惯。
这里的effects书写也不规范,要用双等号。
修改版本:
public int getDirection(Coordinate now, Coordinate next){ /** * @REQUIRES: now.getX()>=0 && now.getX() < 80 * && now.getY() >= 0 && now.getY() < 80 && next.getX()>=0 * && next.getX() < 80 && next.getY() >= 0 && next.getY() < 80 * && graph[now.getX()*80+now.getY()][next.getX()*80+next.getY()] == 1; * @MODIFIES: None; * @EFFECTS: * (next.getX()-now.getX()==1&&next.getY()-now.getY()==0)==>(\result = 0); * (next.getX()-now.getX() == -1 && next.getY()-now.getY()==0)==>(\result == 1); * (next.getX()-now.getX() == 0 && next.getY()-now.getY()==1)==>(\result == 2); * (next.getX()-now.getX() == 0 &&next.getY()-now.getY() == -1)==>(\result == 3); */ }
二、后置条件:
public void servingHandler() throws InterruptedException{ /**管理出租车服务状态 * @REQUIRES: None; * @MODIFIES: this.newtime;this.state;this.coordinate;this.schedulerInfo; * * this.info; * @EFFECTS: 对本线程的状态和参数进行改变 * @THREAD_REQUIRES: * @THREAD_EFFECTS: \locked(trackingInfo); */ }
这个方法实现的过程有些复杂,当时直接用天然语言瞎写了一下,没有规范化表述。不过在此函数中调用了其余函数,如今不知道如何将调用其余函数的effects写清楚。。
public void servingHandler() throws InterruptedException{ /** * @REQUIRES: None; * @MODIFIES:\this.newtime;\this.state; * \this.coordinate;\this.schedulerInfo;\this.info;\System.out; * InfoQueue; * @EFFECTS: * desMove(currentRequest.getDestination()); * this.credit.addAndGet(3); * InfoQueue.contains(schedulerInfo); * schedulerInfo.contains(info); * System.out!=null; * @THREAD_REQUIRES:None; * @THREAD_EFFECTS: \locked(trackingInfo); */ }
三、前置条件和后置条件:
@Override public void desMove(Coordinate destination) throws InterruptedException { /**出租车找最短路径行驶,找最小流量的边 * @REQUIRES: (\all Coordinate a,b;map;graph[a][b] == 1) * @MODIFIES: this.coordinate;this.Info;newtime; * @EFFECTS: this.coordinate == destination; * @THREAD_REQUIRES: * @THREAD_EFFECTS: */ }
这个函数是移动出租车到目标点,requires没有限制destination的范围,后置条件写的过于简略,没有将移动过程写清楚。
@Override public void desMove(Coordinate destination) throws InterruptedException { /**出租车找最短路径行驶,找最小流量的边 * @REQUIRES: now.getX()>=0 && now.getX() < 80 && now.getY() >= 0 * && now.getY() < 80 * &&(\all Coordinate a,b;a.getX()>=0 && a.getX() < 80 && a.getY() >= 0 && a.getY() < 80 && b.getX()>=0 && b.getX() < 80 && b.getY() >= 0 && b.getY() < 80;graph[a.getX()*80+a.getY()][b.getX()*80+b.getY()] == 1) * //保证地图连通 * @MODIFIES: this.coordinate;this.Info;newtime; * @EFFECTS:pathway == TaxiGUI.getInstance().getShortestPath(destination))==>(\all Coordinate a;pathway;this.info.contains(a)) * && (\all int i,int j;j < pathway.size()&&i == j * 5;info.contains(i)) * && \this.coordinate == pathway.get(pathway.size()-1) * && \this.newtime == newtime + waitime + 5*pathway.size()&&info.contains(newtime); */ }
四、前置条件和后置条件:
public static boolean judegeValid(Coordinate a, Coordinate b){ /** * @REQUIRES: None; * @MODIFIES: None; * @EFFECTS: 判断是否符合坐标输入条件 */ }
因为有输入参数,应该对参数范围加以规范和约束。
effects书写也不符合规范。
public static boolean judegeValid(Coordinate a, Coordinate b){ /** * @REQUIRES: a instanceof Coordinate && b instanceof Coordinate && a! = null && b!=null; * @MODIFIES: None; * @EFFECTS:(a.isOutOfBound()||b.isOutOfBound()||a.equals(b))==> \result == false; *!(a.isOutOfBound()||b.isOutOfBound()||a.equals(b))==> \result == true; */ }
五、前置条件和后置条件:
public void RoadStatusHandler(String cmd){ /** * @REQUIRES: * @MODIFIES: TaxiGUI; * @EFFECTS: 改变道路开关; */ }
String cmd不能是null,虽然也在代码中有处理,effects没写清楚。。
public void RoadStatusHandler(String cmd){ /** * @REQUIRES: str instanceof String;str!=null; * @MODIFIES: TaxiGUI;System.out; * @EFFECTS: !cmd.isValid()==>System.out == "#set Status Format Error"; * cmd.matches(this.m)&&cmd.isValid()&&m.group(5).equals("OPEN")==>TaxiGUI.getInstance().graph[m.group(1)*80+m.group(2)][m.group(3)*80+m.group(4)]==1; * cmd.matches(this.m)&&cmd.isValid()&&m.group(5).equals("CLOSE")==>TaxiGUI.getInstance().graph[m.group(1)*80+m.group(2)][m.group(3)*80+m.group(4)]==0; */ }
六、前置条件和后置条件
public void RequestHandler(String cmd) throws RequestFormatErrorException,InterruptedException{ /** * @REQUIRES: * @MODIFIES: rcv; * @EFFECTS: 请求读入 */ }
没有写异常状况,requires不完整,effects不完整
public void RequestHandler(String cmd) throws RequestFormatErrorException,InterruptedException{ /** * @REQUIRES:cmd instanceof String && cmd! = null; * @MODIFIES: rcv;System.out; * @EFFECTS: cmd.isValid()==>\this.rcv.contains(new PassengerRequest request); * !cmd.isValid()==>e == exceptional_behavior(RequestFromatErrorException)&&System.out == e.getMessage(); */ }
方法名 | 功能bug数目 | 规格bug数目 |
---|---|---|
public void input() | 2 | 1 |
public void SetRoadStatus(Coordinate a1,Coordiante a2) | 1 | 0 |
public void randomMove() | 1 | 1 |
个人功能bug主要在代码实现上面有问题,其实和规格的bug联系并无很大。
老师在课上强调,要先写出规格再开始写代码。也就是要先抽象出这个类或者方法的功能,输入输出再进行代码的书写,写出来的内容要符合规格的叙述。因此构思抽象规格是放在首位的,关注的是行为,而不是实现行为的细节。
一个规格的语义包含三部分:需求(Requires),修改(Modifies),结果(Effects)。
一、requires:规格须要有足够的限制性来排除其抽象的用户不可接受的任何实现,这就须要在requires里面明确指出来。一个局部的过程规格老是包含了一个requires格式,有些时候编程应该检查requires中的约束条件,若是不知足就跑出一个异常。
二、modifies:列出了被修改的全部输入名称,作到不遗漏。
三、effects:全部为被requires格式排除的输入描述了过程的行为,必须定义产生了何种输出,同时必须定义被列在modifies格式中的输入作的修改所产生的结果。在本课程中须要用到规范化的表达,实际工程上也有用到简洁的天然语言表达,可是必定要表述清楚,而且符合逻辑。
四、线程类的requires和effects须要书写,但通常不要给使用者限制requires.
实际上因尽量避免使用requires格式,由于若是输入产生了不知足requires的格式的时候,规格并无给出相应的操做。因此设计抽象的时候要设计成知足最小限度的受限,对过程行为的细节仅仅作必要的限制,给实现者更多的自由,能够进行更加有效的编程。