规格化设计的调研
随着50年代高级语言的出现，编译技术不断完善，涌现出多种流派的语言，其中就有里程碑式的Pascal语言；进入70年代，由于众多语言造成的不可移植、难于维护，Ada程序设计语言诞生了，强调大型系统可读性胜于可写性，Ada程序自成清晰的文档；经过80年代计算机硬件和操作系统的改善，程序设计重点从算法和数据结构实现技术向规模说明方向转移。从空间的角度观察, 广义上来说, 软件规格说明描述的是整个软件系统；狭义来说, 软件规格说明描述的是软件系统的组成部件。从时间的角度来观察, 广义来说, 软件规格说明方法适用于整个软件生命周期； 狭义上来说, 软件规格说明方法仅适用于软件生命周期的特定阶段。规格化设计可以提高程序的可读性，也可以提高阅读效率，便于以后的修改。
规格bug
可能是我运气太好了，这几次都没被扣规格的bug……
改进写法
1. 前置条件
1.1 忽略前置条件
previous
public int[][] getMatrix(Point dst){
/**
*@ REQUIRES: None
*@ MODIFIES: visited, dist
*@ EFFECTS: normal_behaver
\result == the shortest distance between point(x,y) from point(x2,y2) ;
*/
}late
public int[][] getMatrix(Point dst){
/**
*@ REQUIRES: !tmp.empty
*@ MODIFIES: visited, dist
*@ EFFECTS: normal_behaver
\result == the shortest distance between point(x,y) from point(x2,y2) ;
*/
}1.2 前置条件不全
previous
private void chooseTaxi(){
/* *
*@ REQUIRES: None
*@ MODIFIES: \this.TarTaxi;
*@ EFFECTS: \any int i=0;i<this.list.size;i++:!list.get(i).getTaxiState().equals(TaxiState.STOP)==> \target = list.get(i);
*/
}late
private void chooseTaxi(){
/* *
*@ REQUIRES: \this.taxi!=null&&\this.taxi is sorted by credit;
*@ MODIFIES: \this.TarTaxi;
*@ EFFECTS: \any int i=0;i<this.list.size;i++:!list.get(i).getTaxiState().equals(TaxiState.STOP)==> \target = list.get(i);
*/
}1.3 范围错误
previous
public void taxiControl(int n) {
/**
*@REQUIRES: n>0 && n<100
*@MODIFIES: None;
*@EFFECTS: ......
*/
}late
public void taxiControl(int n) {
/**
*@REQUIRES: n>=0 && n<100
*@MODIFIES: None;
*@EFFECTS: ......
*/
}1.4 自然语言
previous
private int loadMap(BufferedReader Reader) throws IOException{
/*
@ REQUIRES: in this method we load the map
@ MODIFIES: Map[][]
@ EFFECTS: \any char!=0&&char!=1 ==>System.out&&System.exit
\any somewhere not cross road but has light ==>System.out&&System.exit
*/
}late
private int loadMap(BufferedReader Reader) throws IOException{
/*
@ REQUIRES: File(path).exist
@ MODIFIES: Map[][]
@ EFFECTS: \any char!=0&&char!=1 ==>System.out&&System.exit
\any somewhere not cross road but has light ==>System.out&&System.exit
*/
}1.5 格式错误
previous
public void run(Taxi t){
/*
@ REQUIRES: \t.status.equals(TaxiStatus.SERVING);
@ MODIFIES: None
@ EFFECTS: ......
*/
}late
public void run(Taxi t){
/**
@ REQUIRES: t.status.equals(TaxiStatus.SERVING);
@ MODIFIES: None
@ EFFECTS: ......
*/
}2. 后置条件
2.1 自然语言
previous
public synchronized void changeRoute() {
/*
@ REQUIRES: None
@ MODIFIES: None
@ EFFECTS: get the minimum flow and change the route
*/
}late
public synchronized void changeRoute() {
/*
@ REQUIRES: None
@ MODIFIES: None
@ EFFECTS: \result = this.route = this.map.minRoute(this.position, point);
*/
}2.2 后置条件不全
previous
private int getDir(Point from, Point to){
/*
@ REQUIRES: None
@ MODIFIES: None
@ EFFECTS: (to.getX() - from.getX() > 0) \return = 0;//D
(to.getX() - from.getX() < 0) \return = 1;//U
(to.getY() - from.getY() > 0) \return = 2;//R
(to.getY() - from.getY() < 0) \return = 3;//L
*/
}late
private int getDir(Point from, Point to){
/*
@ REQUIRES: None
@ MODIFIES: None
@ EFFECTS: (to.getX() - from.getX() > 0) \return = 0;//D
(to.getX() - from.getX() < 0) \return = 1;//U
(to.getY() - from.getY() > 0) \return = 2;//R
(to.getY() - from.getY() < 0) \return = 3;//L
\return = 4;
*/
}2.3 没有体现modified的改变
previous
public void run() {
/*
@ REQUIRES: None
@ MODIFIES: system， r, position. credit, state, req, route, timer
@ EFFECTS: \this.state = 2&&\this.reqList.isEmpty==>\this.lastposition = \old.this.position;\this.position = getNextPos();t+=0.2+checkLight(lastposition, position, p);
\this.state = 2&&!\this.reqList.isEmpty==>\this.lastposition = \old.this.position;\this.position = getNextRoute();t+=0.2+checkLight(lastposition, position, p);
\this.state = 1||\this.state = 3==>this.lastposition = \old.this.position;\this.position = getNextRoute();t+=0.2+checkLight(lastposition, position, p);
\this.state = 0 ==> t+=0.2+checkLight(lastposition, position, p);
*/
}2.4 不符合格式规定
previous
public boolean repOK() {
/*
@ REQUIRES: None
@ MODIFIES: None
@ EFFECTS: (this.map==null||this.map.length==0) \result = false;
\result = true;
*/
}late
public boolean repOK() {
/*
@ REQUIRES: None
@ MODIFIES: None
@ EFFECTS: (this.map==null||this.map.length==0) ==> \result == false;
(this.map!=null&&this.map.length!=0) ==> \result == true;
*/
}2.5 忽略后置条件
心得体会
这个规格也不知道该说点什么，都是写完代码看着复制粘贴，改改格式，然后基本也都是电工课解决的hhh可能之后3次要认真一点了
我一直很佛，对自己的程序和别人的程序都是随便测几个，虽然这不是对学术负责的态度？但是觉得吧几天写出来的东西怎么也会有错，至少我是这么认为自己的。自从ifttt自暴自弃，我就没被报过bug（除了第一次出租车的loadfile有点问题，主要还是自暴自弃吧）可能是大难不死必有后福？不过OO倒是让我知道了要更热爱生活，不然除了黑黢黢的屏幕，什么都不剩了。