No way to no bug？
规格化设计的大致发展历史
从一位大师的演讲谈起：
The major cause of the software crisis is that the machines have become several orders of magnitude more powerful! To put it quite bluntly: as long as there were no machines, programming was no problem at all; when we had a few weak computers, programming became a mild problem, and now we have gigantic computers, programming has become an equally gigantic problem.— Edsger Dijkstra, The Humble Programmer (EWD340), Communications of the ACM
在我看来，他的意思是“编程”的复杂度随着计算机性能的提升和需求的提升而增加了。复杂度提高意味着“单人作战”和“闪电战”不再适应当时的需求，势必需要一种体系来支持“团队协作”和“持久战”。这在过去科技发展的进程中并非没有类似经验：产品的生产如何从手工作坊制造到工场集中生产再到工业化生产的？规格化，标准化是其中重要的推动力。编程领域的发展也是这样，需要规格化设计来支撑起“工业级别”的编码工程。
支持这一说法的证据之一是：有“一揽子”软件工程失败了，这些工程复杂度高投入人力物力大，但却依然以失败告终。| Started | Terminated | System name | cost |
|---|---|---|---|
| 1980s | 1993 | TAURUS | £75m |
| 1984 | 1990 | RISP | £63m |
| 1997 | 2000 | Bolit | $35m |
虽然导致软件项目失败的因素较为复杂，但从工程角度而言，没有进行规格化设计是关键因素之一。这说明有需要“革新”的需求。
于是软件工程开始成为人们研究的重点，人们期望研究出如何用系统化、规范化、数量化等工程原则和方法去进行软件的开发和维护，以降低软件工程的失败率。 期间出现和很多理论和优秀的工程语言，而发展到现在，出现了JSF这样的规格设计要求。 但，很不幸，现在依然有不少以失败告终的软件工程项目。作业规格分析
规格BUG
- THREAD_EFFECTS 容易遗漏
synchronized方法的lock()规格。
没有其它规格问题被发现。
规格 bug 产生的原因
完成工程的顺序错了。应当先设计架构，细化为规格，在实现具体的代码。否则在代码实现后人工撰写规格似乎意义不大——这项工作可以用自动化的方式完成。
在构建完代码后再研究规格，容易产生：先入为主，想当然等思维定势。似乎这样的方法在“利用”人的思维缺陷，而非帮助人避开这些问题。 之后的代码构建过程中应当注意设计和代码构建的顺序。前置条件
``` * @REQUIRES: graphMatrix!=null; taxiGUI!=null; 0<=ID<100; time>0; _lights!=null; taxiCAL!=null; * graphMatrix.length==80; * (\all int i;0<=79; graphMatrix[i].length==80); * _lights.repOK() == true; * _taxiGUI.repOK() == true; * taxiCAL.repOK() == true;```1. 先写基本需求。2. 分行列详细需求。3. 利用repOK()。4. 限定严格的边界条件。5. 使用逻辑表达式
后置条件
```* (\this.type == rq.type && rq.startPosition == \this.startPosition && rq.endPosition == this.endPosition && rq.startWindowTime == this.startWindowTime)==>\result == true; * (!(\this.type == rq.type && rq.startPosition == \this.startPosition && rq.endPosition == this.endPosition && rq.startWindowTime == this.startWindowTime))==>\result == false; ```1. 构建代码运行分支。2. 按分支构建前件与后件。3. 考虑异常情况。4. 使用`==`。5. 不过于纠结如何用逻辑表达式表示函数调用。
基本思路和体会
JSF写得越接近纯bool表达式越好，在没有自动化逻辑检测工具的情况下，这样的方式在互测中比较占优势。
写在后面
LSP设计原则
本系统中涉及到继承的主要有两类：Request和Taxi。
注意到这两个类的主要的public方法在重载时都不改变原有方法的EFFECTS，而是在原有方法的基础上进行扩展，这使得外部调用者在调用子类public方法时得到的效果包含了调用父类相同方法的效果，这就使得外部调用任何父类出现的地方都可以使用子类来代替,并不会导致使用相应类的程序出现错误。 在实际实现的过程中也是以父类来统一管理不同的子类对象的，如TaxiHandler中的taxiList为Taxi数组，但却管理了Sutaxi和Taxi。 举例 Sutaxi -> Taxi
- public synchronized boolean setRequest (Request rq, TaxiStatusPackage p)
public synchronized boolean setRequest(Request rq, TaxiStatusPackage p) { if(super.setRequest(rq, p) == true) { curRequestPackage = new ArrayList (); Request temp = rq.clone(); requestHistory.add(temp ); rqToTSPListMap.put(temp.toString()+","+rq.startWindowTime, curRequestPackage); return true; }else return false; } 可见，其返回值相关的约束条件与父类相同，但是增添了一些SuTaxi本身所需的功能。不影响Taxi约束。
接口
如何保证类的封装行驶一个很复杂的问题，这里讨论一种特殊情况的解决方式：在某个类执行完某些请求后其他类要执行后续步骤，但其他类又不应属于执行某请求的类。
例如： 出租车在更新位置之后要让请求知道其是否进入了请求抢单范围，而在我的设计中，出租车不应该负责与请求的这类交互操作。如何解决？——接口。 代码样例如下：- TaxiHandler
//初始化出租车列表时for (int i=0;i<=29;i++) { TaxiCAL tempTC = new TaxiCAL(map, taxiGUI.getOriGraphMatrix(), taxiGUI); tempTC.setGraph(1); taxiList[i] = new SuTaxi(i, startTime, matrixMap, tempTC, _lights, _taxiGUI) //接口写法， 保证了封装性。。 { @Override /** * @REQUIRES: e!=null; curTime>0; * @MODIFIES: taxiIDMap; this.curRequestPackage; taxiGUI; * @EFFECTS: * (\all Request rq; \old(taxiIDMap).containsKey(rq); rq.isWindowTime(curTime)&&rq.isNear(e.point)) ==>(call \this.getBill())&&(taxiIDMap.get(rq).contains(e.ID)) * (e.statusCode == 1 || e.statusCode == 3) ==> \this.curRequestPackage.contains(e) * @THREAD_EFFECTS: * \lock(rwl.readLock()) // 消极锁保证效率 */ public void afterMove(TaxiStatusPackage e, long curTime) { //在这里可以直接调用TaxiHandler的成员变量，而this.object则调用了Taxi对象的成员变量（方法同理） if(e.statusCode==2) { rwl.readLock().lock(); try { for(Map.Entry > entry : taxiIDMap.entrySet()) { Request iter = entry.getKey(); if(iter.isWindowTime(curTime)&&iter.isNear(e.point)) { if(!entry.getValue().contains(e.ID)) { this.getBill(); } entry.getValue().add(e.ID); } } }finally { rwl.readLock().unlock(); } }else if(e.statusCode == 1 || e.statusCode == 3) { this.curRequestPackage.add(e); } taxiGUI.SetTaxiStatus(e.ID, e.point, e.statusCode); } }; this.taxiGUI.SetTaxiType(i, 1); } Taxi中预留了空接口：
/** * @REQUIRES: NONE * @MODIFIES: NONE * @EFFECTS: NONE */public void afterMove(TaxiStatusPackage e, long curTime) { }