一、规格化的发展历史
最早的程序设计都是面向机器，从一开始使用的机器语言，到后面的汇编语言，都是面向机器的语言，编写困难也容易出错。随着需求的发展，程序的编写从面向机器走向面向过程，但由于goto语句导致的面条式代码，极大的限制了程序的规模，“软件危机”产生，程序设计的思想又经历了几次革命，“结构化程序设计”作为解决软件危机的方案被提出来了，这个概念通过“自顶向下、逐步细化、模块化”的方法降低程序的复杂度，但需求永远发展的更快，又产生了第二次软件危机，这次软件危机主要体现在可扩展性和可维护性上面，在这种背景下，面向对象的思想开始流行起来，从面向过程到面向对象，人们意识到了，为了保证程序的正确性和提升精简程度，同时注重后续维护和扩展的需求，要对整体程序进行更好的统筹规划，规格化就是辅助人类达到这个目标的一个极好的工具。
二、写法改进
因为这几次作业都没有被报规格方面的bug，我就直接列举一些自己需要改进的规格写法了。
1.前置条件不完善、后置条件使用自然语言
/**
* @REQUIRES: None;
* @MODIFIES: None;
* @EFFECTS: return state string;
*/
⬇
⬇
⬇
/**
* @REQUIRES: \this.mode>=0&&\this.mode<=3;
* @MODIFIES: None;
* @EFFECTS: (\result="stop") ==> (mode == 3);
* (\result="in service") ==> (mode == 0);
* (\result="waiting to serve") ==> (mode == 2);
* (\result="picking up passenger") ==> (mode == 1);
*/
2.前置条件不全面
/**
* @REQUIRES: None;
* @MODIFIES: \this.loacte;
* @EFFECTS: (\this.locate[i][j] == 1) ==> (\old.this.locate[i][j] == 2);
* (\this.locate[i][j] == 2) ==> (\old.this.locate[i][j] == 1);
*/
⬇
⬇
⬇
/**
* @REQUIRES: (i>=0)&&(i<80)&&(j>=0)&&(j<80);
* @MODIFIES: \this.loacte;
* @EFFECTS: (\this.locate[i][j] == 1) ==> (\old.this.locate[i][j] == 2);
* (\this.locate[i][j] == 2) ==> (\old.this.locate[i][j] == 1);
*/
3.前置及后置条件不全面
/**
* @REQUIRES: None;
* @MODIFIES: None;
* @EFFECTS: (mode == 2)&&(resttimer == 0);
*/
⬇
⬇
⬇
/** * @REQUIRES: re!=null; * @MODIFIES: \this.r;this.mode;this.resttimer; * @EFFECTS: (\this.mode == 2)&&(\this.resttimer == 0)&&(this.r == re); */
4.构造方法也应当约束传入的参数
/**
* @REQUIRES: None;
* @MODIFIES: this;
* @EFFECTS: (\this.start == s)&&(this.recordpath == rp)&&(this.end == e)&&(this.time == t);
*/
⬇
⬇
⬇
/** * @REQUIRES: (s != null)&&(rp != null)&&(e != null)&&(t != null); * @MODIFIES: this; * @EFFECTS: (\this.start == s)&&(this.recordpath == rp)&&(this.end == e)&&(this.time == t); */
5.后置条件使用自然语言
/**
* @REQUIRES: p != null;
* @MODIFIES: \this.pos;
* @EFFECTS:set this.pos to p;
*/
⬇
⬇
⬇
/** * @REQUIRES: p != null; * @MODIFIES: \this.pos; * @EFFECTS:(\this.pos == p); */
三、总结归纳
刚开始在得知要写规格的时候心里是比较烦又觉得这个没什么用，但是几次作业下来也算是明白了规格的意义，在扩展的时候有时会忘了当时写这个方法的时候有什么限制条件，此时规格就能提醒我，一份小作业尚且如此，大型工程想必是更加需要这种规范来保证多人合作的效率和准确性了。
