一、规格化设计
规格化设计与编程语言的发展是密切相关的。
在最开始的时候，人们的编程思想还停留在完全以机器的角度进行编程。在上个世纪六七十年代以前，编程都是通过机器语言与汇编语言，这两种语言在逻辑上与功能上都是从机器的角度思考这个问题。而且，编程语言的描述也不是很通俗易懂：机器语言的机器码、汇编语言的汇编指令，都是需要理解计算机体系结构才能学会并精通的。这样在计算机发展的初期因为编程量尚不算大，问题并不算大。然而，在上个世纪六十年代，随着编程的代码量的增多，通过这两种语言来编程就变成了非常麻烦而且容易出错的事情。由此，面向对象的编程语言登上舞台。
但是，即便如此，代码量仍在不断增加。由此导致一些面向过程语言中的goto语句导致的面条式代码，极大的限制了程序的规模。为了解决这个问题，人们提出采取“自顶向下、逐步细化、模块化”的指导思想。结构化程序设计本质上还是一种面向过程的设计思想,但通过“自顶向下、逐步细化、模块化”的方法,将软件的复杂度控制在一定范围内,从而从整体上降低了软件开发的复杂度。
我认为规格化设计的起源应该是在这里。正是模块化编程，使得每个函数有了“固定输入就有固定输出”的概念。由此，伴随着大规模的代码，通过规格化设计可以快速地使程序设计研发人员理解一个方法的用途与使用方法。伴随着第二次软件危机，软件的可移植性得到增强，并提出了面向对象的概念。由此一来，随着软件的可移植性的增强，每个对象中方法的使用与功能的阐述势必得以增强。规格化设计相比在这是也得到了飞速的发展。
我的父亲的工作有时也涉及到软件研发。他告诉我，在他们研发一套软件的时候，设计软件的人员与软件编程人员往往不是一拨人。通常都是设计软件的人先通过规格化设计将软件的属性与方法都确定下来，经过讨论审批没有问题，才交由编程人员去实现。曾经看到过这样一句话：“40%到50%软件项目的工作量花在了可以避免的返工上面”，所以在开发前完善软件架构是十分有必要的，所以规格化设计是很有必要的。
二、规格bug
这三次都没有被报规格bug。
三、规格不好的写法举例
1、前置条件
（1）
/**
* @REQUIRES: guigv.light != null
* @MODIFIES: none
* @EFFECTS :
* (int i , j , 0<=i , j<80 ) => guigv.lightmap[i][j] == guigv.lightmap[i][j] == 1? 2 : 1;
*/
private void changeLignt() {
这个方法用来改变路灯方向的。所以没有传参，应不写guigv.light!=null。
（2）
/**
* @REQUIRES: path == file
* @MODIFIES: none
* @EFFECTS :
* (/load map /load flow /load taxi /load request) == true
*/
public void load(String path) {
这个方法用来加载地图。这里应该写成“path == file.getAbsolutePath()”。
（3）
/**
* @REQUIRES: none
* @MODIFIES: none
* @EFFECTS :
* this /output in file == true
*/
private void output(int type , Taxi t) throws IOException {
这个方法将运行的出租车信息输出到文件。在这个方法中，并没有提及type不等于1、2、3之外的数的处理方法，所以前置条件应该加上“(type==1)||(type==2)||(type==3)”。
（4）
/**
* @REQUIRES: r == /normal
* @MODIFIES: none
* @EFFECTS :
* r + -> == rlist
*/
public synchronized void addR(Request r) {
这个方法将一个请求加入调度队列。前置条件应该改为“r!=null;”。
（5）
/**
* @REQUIRES: invalid == false
* @MODIFIES: this./all
* @EFFECTS :
* this./all exp(choose taxi)->taxi.do
*/
public void run() {
run（）方法在执行的时候为了程序的正确执行，前置条件应该为None，然后在方法内部写invalid==true的时候应该怎么处理。
2、后置条件
（1）
/**
* @REQUIRES: guigv.light != null
* @MODIFIES: none
* @EFFECTS :
* (int i , j , 0<=i , j<80 ) => guigv.lightmap[i][j] == guigv.lightmap[i][j] == 1? 2 : 1;
*/
private void changeLignt() {
这里应该把“guigv.lightmap[i][j]==1?2:1”用小括号括起来，不然容易有误解。
（2）
/**
* @REQUIRES: light.init == true
* @MODIFIES: guigv.light[x][y]
* @EFFECTS :
* if(x,y) == cross_road => /result == true;
*/
public boolean judgex(int x , int y) {
其一是不必写if，而且应该是“\result”而不是“/result”；其二是应专门写一个函数用来检测这个路口是不是交叉路口，而不是利用一个自然语言“cross_road”。
（3）
/**
* @REQUIRES: s != null
* @MODIFIES: none
* @EFFECTS :
* \result == match regEx
*/
public boolean check(String s) {
这个方法用于检测一个字符串是否匹配一个正则表达式。这里应该将“==”的右半部分改为“Matcher.matches()”。
（4）
/**
* @REQUIRES: none
* @MODIFIES: none
* @EFFECTS :
* this /output in file == true
*/
private void output(int type , Taxi t) throws IOException {
这个方法将运行的出租车信息输出到文件。在@Effects中应该写上什么时候抛出一个IOException。
（5）
/**
* @REQUIRES: r == /normal
* @MODIFIES: none
* @EFFECTS :
* r + -> == rlist
*/
public synchronized void addR(Request r) {
这个方法将一个请求加入调度队列。后置条件不能完整地反映这个方法的功能。应改为“rlist.size == \old(rlist.size)+1;\exist int i;0<=i<rlist.size;rlist.get(i).equals(r)==true;”。
四、设计撰写规格的思路与体会
思路就是先想清楚这个方法的功能具体是什么，然后根据这个方法的逻辑写出后置条件，然后规范前置条件并根据后置条件写修改内容。
在写方法规格的时候，感觉一旦一个方法比较复杂，规格就不好写，其后置条件的布尔表达式就极为麻烦。后来为了简化这些后置条件，就增加的方法的数量。这样写完后，发现确实如同老师说的一样，方法基本没有超过70行的。我感觉，除了那些重复的部分比较多的、分支条件比较复杂的方法，一个能准确规格化的方法基本都不会太长。而且，在写完规格后，在写方法的时候思路清晰了很多，基本不会出现忘记实现的功能。
原文：https://www.cnblogs.com/liaowang99/p/9108585.html