規格化設計的一個重要目的是爲了將模塊的功能,約束經過抽象和層次分類來表達清楚,方便用戶與開發者的信息交流,與結構化設計有着密不可分的關係。
程序設計的演變大體能夠分紅如下三個過程:算法
1. 20世紀60年代之前,計算機剛剛投入實際使用,軟件設計每每只是爲了一個特定的應用而在指定的計算機上設計和編制,採用密切依賴於計算機的機器代碼或彙編語言,軟件的規模比較小,不多使用系統化的開發方式,此時的代碼更多的是私人性質的,知足我的要求的程序less
2. 60年代中期,大容量、高速度的計算機出現,隨之出現的是代碼量急劇提高,複雜度急劇增加、程序可靠性問題突出的問題。結果化程序設計隨之提出,它要求程序設計時以模塊爲單位,每一個模塊專職本身的工做,而要在模塊間交流,在開發者和用戶,開發者和開發者之間交流,就只須要相應接口便可;分佈式
3. 80年代,面向對象的設計開始在業界大行其道,相比於單純的結構化設計,面向對象的設計從審視問題的角度上就有了差別,程序發生了從圍繞「行爲」執行到圍繞「客體」執行的變化,隨之而來的,就是封裝性地提升,可重用性的提升,能夠說,面向對象進一步實現告終構化設計,是結構化設計更進一步的實現。說明是類型定義和操做描述,體是操做的具體實現。(具體的例子就是C++,Java等面嚮對象語言的類說明與類實現的分離。)解決方案設計只關注說明,實現時引用或者設計體。體的更改、置換不影響規格說明,保證了可移植性。支持多機系統,但要一樣環境。此時產生了劃時代的面向對象技術。在結構化越加明確的同時,開發者與設計者,開發者與用戶,開發者與開發者之間的交流,就須要「抽象」來實現,由於彼此間不須要關心對方的實現方法,而只須要知道這個模塊的接口有什麼要求,會改什麼,能作什麼就行。經過規格化抽象,咱們就能將這種交流變得高效,同時也下降了維護和修改的難度。oop
4.基於構件開發:標準化的軟件構件如同硬件IC,可插拔,使用者只用外特性,不計內部實現。Web Services:軟件就是服務。分佈式,跨平臺,鬆耦合。測試
程序設計語言的第二次分離催生了規格化設計的誕生,規格化優勢不少,故獲得了人們的重視。優化
Effects不完整 | 77行:@THREAD_EFFECTS: this.MS; |
Requires不完整 | 176行:@REQUIRES:id!=null; |
無規格bugui
Modified不完整 | 59行:@MODIFIES: System.out,this.output,this.rl;缺乏 |
Effects邏輯錯誤 | 196行:String s=a+" "+b+" "+0; 「=」應爲「==」 |
沒有JSF | 有兩個新增方法沒寫JSF |
一方面是由於從第九次做業開始,不少的方法都是沿用的以前的做業,而以前已經寫好的方法從新加上規格會致使有一些本末倒置的意味,而且課下發放的JSF並不能徹底解決咱們對於規格的理解,因此在編寫程序規格時不免出現一些問題,歸結緣由仍是不熟練以及缺少相似的思想。至於新增的方法沒有寫JSF仍是由於本身先寫了方法自己,而非老師說的先寫規格再寫代碼,至於Requires,Modified和Effects的不完整就純屬於本身的粗枝大葉。沒有什麼可辯解的,但願這幾回做業可以培養本身之後寫註釋寫規格的習慣,而且可以寫的儘可能簡潔準確。this
1 /** 2 *@REQUIRES:id!=null; 3 *@EFFECTS: 4 * \result==squad[id]; 5 */ 6 public Taxi get(int id){ 7 return this.squad[id]; 8 }
對於id來說除了不爲null還應當知足內部條件,改進爲:spa
/** *@REQUIRES:id!=null,0<=id<=99; *@EFFECTS: * \result==squad[id]; */ public Taxi get(int id){ return this.squad[id]; }
/** *@REQUIRES: r!=null; *@MODIFIES: this.SRC,this.DST,this.status,this.WaitCount; *@EFFECTS: * SRC==r.GetSrc(); * DST==r.GetDst(); * status==TAKING; * WaitCount==0; */ public void getOrder(Request r){ this.SRC=r.GetSrc(); this.DST=r.GetDst(); this.status=TaxiStatus.TAKING; this.WaitCount=0; }
r不只應當不爲null,還應當是一個Request對象,改進爲:線程
/** *@REQUIRES: r!=null,r instanceof Request; *@MODIFIES: this.SRC,this.DST,this.status,this.WaitCount; *@EFFECTS: * SRC==r.GetSrc(); * DST==r.GetDst(); * status==TAKING; * WaitCount==0; */ public void getOrder(Request r){ this.SRC=r.GetSrc(); this.DST=r.GetDst(); this.status=TaxiStatus.TAKING; this.WaitCount=0; }
/** *@REQUIRES: s!=null,s=TAKING||s=WAITING||s=SERVING||s=STOP; *@MODIFIES: this.status; *@EFFECTS: * status==s; */ public void SetStatus(TaxiStatus s){ this.status=s; }
應改進爲:
/** *@REQUIRES: s!=null,s==TAKING||s==WAITING||s==SERVING||s==STOP; *@MODIFIES: this.status; *@EFFECTS: * status==s; */ public void SetStatus(TaxiStatus s){ this.status=s; }
@REQUIRES:num instanceof int&& num==1||num==3
應改進爲:
@REQUIRES:num instanceof int&&(num==1||num==3)
@REQUIRES:taxis instanceof Taxi[]
應細緻描述,改進爲:
@REQUIRES:\all int i;0<=i<taxis.length;taxis[i] instanceof Taxi
/** *@MODIFIES: this.Shot; *@EFFECTS: * (\all int i,j,k;0<=i,j<80,0<=k<100,Shot[i][j][k]!=-1)==>(Shot[i][j][k]==-1); */ public void Clear(){ for(int i=0;i<80;i++){ for(int j=0;j<80;j++){ for(int k=0;k<100;k++){ if(this.Shot[i][j][k]!=-1){ this.Shot[i][j][k]=-1; } else{ break; } } } } }
/** *@MODIFIES: System.out; *@EFFECTS: * true==>(do the things below in an endless loop)==>(wait())==>(dispatch()); */ public void run(){ while(true){ try { synchronized(this.MS){ this.MS.wait(); this.dispatch(); } //System.out.println(System.currentTimeMillis()); } catch (Throwable e) { System.out.println("Error in Scheduler"); System.exit(0); } } }
應改進爲:
/** *@MODIFIES: System.out; *@EFFECTS: * true==>(do the things below in an endless loop)==>(wait())==>(dispatch()); *@THREAD_EFFECTS: this.MS; */ public void run(){ while(true){ try { synchronized(this.MS){ this.MS.wait(); this.dispatch(); } //System.out.println(System.currentTimeMillis()); } catch (Throwable e) { System.out.println("Error in Scheduler"); System.exit(0); } } }
/** *@MODIFIES: this.light,this.lightmap; *@EFFECTS: * Change the lights */ public void Change(){ for(int i=0;i<80;i++){ for(int j=0;j<80;j++){ if(Main.light[i][j]==1){ Main.light[i][j]=2; guigv.lightmap[i][j]=1; Main.TG.SetLightStatus(new Point(i,j),1); } else if(Main.light[i][j]==2){ Main.light[i][j]=1; guigv.lightmap[i][j]=2; Main.TG.SetLightStatus(new Point(i,j),2); } } } }
應改進爲:
/** *@MODIFIES: this.light,this.lightmap; *@EFFECTS: * (\all int i,j,k;0<=i,j<80,light[i][j]>0)==> * ((light[i][j]==1)==>(light[i][j]==2&&lightmap[i][j]==1)&&(light[i][j]==2)==>(light[i][j]==1&&lightmap[i][j]==2)); */ public void Change(){ for(int i=0;i<80;i++){ for(int j=0;j<80;j++){ if(Main.light[i][j]==1){ Main.light[i][j]=2; guigv.lightmap[i][j]=1; Main.TG.SetLightStatus(new Point(i,j),1); } else if(Main.light[i][j]==2){ Main.light[i][j]=1; guigv.lightmap[i][j]=2; Main.TG.SetLightStatus(new Point(i,j),2); } } } }
對於我我的的程序來說,功能bug和規格bug其實沒有什麼彙集關係,可是這種狀況出現的緣由主要是由於是先寫完的代碼才寫的規格,致使兩個描述多是不一致的,可是從整個程序的設計來考慮,當一個方法的規格複雜時,必然須要更多的篇幅和代碼來進行實現,出現bug的概率也會越大。
做業次數 | 功能性bug | 規格bug | 功能bug分析 | 規格bug分析 | 相關性/彙集關係 |
第九次 | 2 | 2 | 信用越界/初始化缺失 | 缺乏某些requires和effects | 無 |
第十次 | 1 | 0 | 右轉等燈了 | 無 | 無 |
第十一次 | 3 | 3 | LoadFile指令沒有記錄,出租車沒有指定,真假時間混用出錯, | =應爲==,忘記某些規格 | 無 |
首先對於JSF這塊,有一些不明白爲什麼不在課程剛剛開始的時候就進行訓練,而在需求逐漸增長的這個時刻開始要求,你們每每面對着既要改需求,又要書寫JSF的雙重考驗,不過從長遠來看,規格訓練是必要的,只不過我認爲這個不該該做爲互測中扣分的點。規格書寫主觀性很強,不少同窗功能完成的很好卻被扣了不少規格的分,像我這樣的因爲以爲本身規格寫的不夠好,寫的也很煎熬,因此在測試他人的時候就沒有太過嚴格,感受差很少就沒有扣分,可是沒想到測試個人狠人連我JSF裏少打了一個=都發現了,而且依次檢查了我全部的Modified,惟一缺失的一個也被就出來了,我以爲這是否有些本末倒置了,不過既然是本身的確錯了,就得認,可是當本身看到互測結果是一大堆規格的時候內心仍是不舒服的,費了很大勁寫的功能,能讓本身的出租車跑不少請求,優化BFS算法,結果弄了半天輸在了JSF上了。說實話最近幾回的OO做業寫起來不難,可是心情的確不太好。不過OO總算也要結束了,你們也該歇歇了,查BUG的戾氣過重,變成線上查BUG線下約架了。能夠增長一個互測加分環節,說出別人代碼的一個優勢,給測試者加一分,這樣你們都很開心,整個六系會陷入互相吹捧互相讚美的大好環境中。既然那麼多人爲了分數,那開心點豈不是更好。