OO第三阶段总结

1.使用自然语言：
/**
@REQUIRES：gui不为空
*/
改正：
/**
*@REQUIRES：gui!=null;
*/

2.前置条件不为布尔表达式“
/**
*@REQUIRES: 0<=x<=79;
*           0<=y<=79;
*/ 
改正：
/**
*@REQUIRES: 0<=x<=79 && 0<=y<=79;
*/              

3.构造方法参数没有约束：
public LightMap(TaxiGUI gui,Map map) {
/**
*@REQUIRES:None;
*/
}
改正：
public LightMap(TaxiGUI gui,Map map) {
/**
*@REQUIRES:map!=null && gui!=null;
*/
}

4.缺少对数字范围判断：
public boolean waitpass(int x,int y) {
/**
*@REQUIRES:None;
*/
}
改正：
public boolean waitpass(int x,int y) {
/**
*@REQUIRES:0<=x<=79 && 0<=y<=79;
*/
}

5.参数约束不全：
public void setflow(int x1,int y1,int value){
/**
*@REQUIRES:0<=x1<=79 && 0<=y1<=79;
*/
}
改正：
public void setflow(int x1,int y1,int value){
/**
*@REQUIRES:0<=x1<=79 && 0<=y1<=79 && 0<=value<=1000;
*/
}

1.线程控制未加锁：
public synchronized int state() {
/**
*@EFFECTS:
*    \result==state;
*/     
}
改正：
public synchronized int state() {
/**
*@EFFECTS:
*    \result==state;
* @THREAD_REQUIRES:
*      \locked();
* @THREAD_EFFECTS:
*      \locked(\this);
*/     
}

2.后置条件不为布尔表达式：
public int demens(int x,int y) {
/**
*@EFFECTS:
*        \result=x*80+y;
*/
}
改正：
public int demens(int x,int y) {
/**
*@EFFECTS:
*        \result==x*80+y;
*/
}

3.后置条件不全面：
public Map(TaxiGUI gui) throws FileNotFoundException {
/** 
*@EFFECTS:
*    \this.flow==flow;
*    \this.map==map;
*    \this.gui==gui;
*/
}
改正：
public Map(TaxiGUI gui) throws FileNotFoundException {
/** 
*@EFFECTSS:
*    \this.flow==flow;
*    \this.map==map;
*    \this.gui==gui;
*    \this.name==name;
*/
}
        

4.使用自然语言：
public int demens(int x,int y) {
/**
*@EFFECTS:
*   返回x*80+y;
*/
    return x*80+y;
}
改正：
public int demens(int x,int y) {
/**
*@EFFECTS:
*   \result=x*80+y;
*/
    return x*80+y;
}

5.出现如果--否则语句描述：
public boolean repOK() {
/** 
* @EFFECTS:
*     (map==null)==>\result=false;
*      else ==>\result=true;
*/ 
    if(lightmap==null ) return false;
    return true;        
}
改正：
public boolean repOK() {
/** 
* @EFFECTS:
*      \result==!(map==null);
*/ 
    if(lightmap==null ) return false;
    return true;        
}