规格化设计的发展历史
在计算机的早期发展中，软件开发没有可以遵循的系统方法，往往只有源代码而没有软件说明书等文档，因此这段时期的软件通用性时很有限的。后来到了20世纪60年代，软件开始被广泛使用，软件开发依然没有规范化，而软件的需求也越来越复杂，使得程序维护难度大大增加。为了解决这一难题，人们认真思考后形成了新的程序开发要求：即程序除了拥有良好的性能和正常的功能外，还应该具有良好的可读性的可拓展性，并易于后期的维护。1968年北约软件工程大会上提出来软件工程的概念。之后普遍开始关注软件开发过程的研究，在这期间确定了一系列重要的文档规范，这些规范在后来的发展中形成了软件开发之中的规格化设计。
规格化设计作为一种契约化编程手段，它要求开发者使用抽象和规格的方法设计程序，保证了程序的易维护性、高效性以及可拓展性，对于大型的软件开发大有裨益，因此受到了人们的重视。
作业BUG分析
三次作业都没有被报规格bug。
五个不好的前置条件和后置条件写法以及改进
1 五个不好的前置条件写法以及改进：
a)前置条件考虑不充分，未对allTaxi数组内元素加以限制。
Input(Queue reqs,TaxiGUI gui,Map map,Taxi[]allTaxi){
/**
* @REQUIRES:
* reqs!=null;
* gui!=null;
* map!=null;
* allTaxi!=null;
改进写法：
Input(Queue reqs,TaxiGUI gui,Map map,Taxi[]allTaxi){
/**
* @REQUIRES:
* reqs!=null;
* gui!=null;
* map!=null;
* allTaxi!=null;
* (\all int i;0<=i<=99;allTaxi[i]!=null);
b)使用自然语言。
public void openFile(String name) {
/**
* @REQUIRES:文件存在
改进写法：
public void openFile(String name) {
/**
* @REQUIRES:FILE(name).exists==true;
c)未对参数取值范围加以限制。
synchronized void setStatus(int status) {
/**
* @REQUIRES:status!=null;
改进写法：
synchronized void setStatus(int status) {
/**
* @REQUIRES:status!=null;
* status==0||status==1||status==2||status==3;
d)未考虑数组为null的情况。
synchronized Request removeFirst() {
/**
* @REQUIRES:None;
改进写法：
synchronized Request removeF() {
/**
* @REQUIRES:this.reqQueue!=null;
e)冗余的前置条件（方法内对文件路径不存在的情况作了相应的处理，因此不必再前置条件中加以限制）。
public void mapLoader(String fileName) {
/**
* @REQUIRES:File(fileName).exist;
改进写法：
public void loading(String fileName) {
/**
* @REQUIRES:None;
2 五个不好的后置条件写法以及改进：
a)使用自然语言。
public static void fileWriter(String file,String str){
/**
* @REQUIRES:
* file！=null;
* File(file).exist;
* @MODIFIED: File(file);
* @EFFECTS: write str to end of File(file);
*/
改进写法：
public static void fileIn(String fileName,String str){//写字符串str写到文件File(fileName)中
/**
* @REQUIRES:
* File(fileName).exist==true;
* @MODIFIED: File(fileName);
* @EFFECTS: File(fileName)!=\old(File(fileName));
*/
b)后置条件为布尔表达式，不应用‘=’。
public boolean getArrived(){
/**
* @REQUIRES:None;
* @MODIFIES:None;
* @EFFECTS:\result=this.arrived;
*/
改进写法：
public boolean getArrived(){
/**
* @REQUIRES:None;
* @MODIFIES:None;
* @EFFECTS:\result==this.arrived;
*/
c)后置条件表述不清晰。
void setReachable() {
/**
* @REQUIRES:
* map!=null;
* @MODIFIES:
* \this.reachable;
* @EFFECTS:
* (\all point p;point q.reaches(q)||p.reaches(q);reachable[p.x][p.y].contains(q);
*/
改进写法：
void setReachable() {
/**
* @REQUIRES:
* map!=null;
* @MODIFIES:
* \this.reachable;
* @EFFECTS:
* (\all point p,q;q.reaches(q)==true&&p.reaches(q)==true;reachable[p.x][p.y].contains(q)==true
* &&reachable[q.x][q.y].contains(p)==true;
*/
d)使用自然语言。
String SPFA(point src,point des,Vector<point>[][] reachable) {
/**
* @REQUIRES:src!=null&&src.inMap==true;
* des!=null&&des.inMap==true;
* @MODIFIES: None;
* @EFFECTS:\result==String(shortest path from src to des);
*/
改进写法：
String SPFA(point src,point des,Vector<point>[][] reachable) {
/**
* @REQUIRES:src!=null&&src.inMap;
* des!=null&&des.inMap;
* @MODIFIES: None;
* @EFFECTS:\result！=null&&\result.length()>=0;
*/
e)未书写exception_behavior。
void initMap(String name,TaxiGUI gui) {
/**
* @REQUIRES:
* name!=null;
* gui!=null;
* File(filename).exist;
* @MODIFIES:
* \this.map;
* \this.numMap;
* @EFFECTS:
* \all int i;0<=i<80;this.map[i]==readLine(name);
* !MapReadSucceed==>output error information
*/
改进写法：
void initMap(String name,TaxiGUI gui) {
/**
* @REQUIRES:
* name!=null;
* gui!=null;
* File(filename).exist;
* @MODIFIES:
* \this.map;
* @EFFECTS:normal_behavior
* \all int i;0<=i<80;this.map[i]==readLine(name);
* !MapReadSucceed==>exceptional_behavior (WrongFormatException);
*/
聚焦关系
由于部分规格是在代码实现后才书写的，所以在我的这三次作业中，功能bug和规格bug没有聚集关系。
心得体会
在书写规格前，我会先思考方法需要实现的功能，之后再分析方法调用时默认满足的条件、用户能够感觉到的数据修改以及执行后系统满足的状态，最后将这些信息体现在规格中。
良好的规格给我们阅读代码提供了便利，提高了代码的可读性，使得bug的定位以及后期的代码重构不那么复杂。在写规格的过程中，能够理清思路，减少了因为逻辑错乱而产生的bug，达到事半功倍的效果。这几次作业中我写出的代码规格依然存在表意不明，逻辑不清等问题，所以在以后的代码书写中，我还应该对代码的规格书写多加练习。