OO绗笁鍗曞厓鎬荤粨
Posted
tags:
篇首语：本文由小常识网(cha138.com)小编为大家整理，主要介绍了OO绗笁鍗曞厓鎬荤粨相关的知识，希望对你有一定的参考价值。
鏍囩锛?a href='http://www.mamicode.com/so/1/person' title='person'>person 绫诲瀷 杩涘叆 man expect inf lse ora sign
JML绠€浠嬶細
The Java Modeling Language (JML) is a behavioral interface specification language that can be used to specify the behavior of Java modules. It combines the design by contract approach of Eiffel and the model-based specification approach of the Larch family of interface specification languages, with some elements of the refinement calculus.
浣跨敤 JML 鏉ヨ鏄庢€у湴鎻忚堪鎵€甯屾湜鐨勭被鍜屾柟娉曠殑琛屼负锛屽彲浠ユ樉钁楀湴鏀瑰杽鏁翠釜寮€鍙戣繃绋嬨€?/span>
JML琛ㄨ揪寮忥細
| 琛ㄨ揪寮?/span> | 鍚箟 |
|---|---|
| esult | 鏂规硶杩斿洖鍊?/span> |
| old() | 琛ㄧず杩涘叆鏂规硶鏃跺埢鏌愪釜鏁版嵁鐨勫€?/span> |
| (forall ; ; ) | 鍏ㄧО閲忚瘝 |
| (exists ; ; ) | 瀛樺湪閲忚瘝 |
| a==>b | a鎺ㄥ嚭b |
| sum | 缁欏畾鑼冨洿鍐呰〃杈惧紡鐨勫拰 |
| um_of | 鎸囧畾鍙橀噺涓弧瓒崇浉搴旀潯浠剁殑鍙栧€间釜鏁?/span> |
JML宸ュ叿閾撅細
-
OpenJML锛岄潤鎬佹鏌ュ櫒锛屽JML璇硶杩涜妫€鏌?/span>
-
JMLUnit锛屽彲浠ュ熀浜嶫ML娉ㄩ噴鐨刯ava鏂囦欢鐢熸垚JUnit娴嬭瘯
-
SMTSolver锛屽湪閫昏緫灞傞潰銆佸浠ｇ爜瀹炵幇褰㈠紡鍖栭獙璇併€?/span>
銆€銆€銆€銆€銆€
2.閮ㄧ讲JMLUnitNG/JMLUnit锛岄拡瀵笹roup鎺ュ彛鐨勫疄鐜?strong>鑷姩鐢熸垚娴嬭瘯鐢ㄤ緥锛屽苟缁撳悎瑙勬牸瀵圭敓鎴愮殑娴嬭瘯鐢ㄤ緥鍜屾暟鎹繘琛岀畝瑕佸垎鏋?/span>
灏濊瘯浜嗚窇鍚勭鏍峰瓙鐨凪yGroup锛岃櫧鐒惰В鍐充簡鐩綍鍜岀被闂磋皟鐢ㄧ瓑绛変竴澶у爢鎶ラ敊锛屼絾杩樻湁涓€浜涙姤閿欎笉鐭ラ亾鎬庝箞瑙ｅ喅锛屾瘮濡備笅闈㈣繖涓細
鏈€鍚庡啓浜嗕釜绠€鍗曟牱渚嬶細
package test;
?
public class MyGroup {
?
/*@ public instance model non_null int id;
@ public instance model non_null int[] people;
@*/
?
private int[] people_;
private int id_;
?
public MyGroup(int id) {
people_ = new int[100];
id_ = id;
}
?
//@ ensures
esult == id;
public /*@pure@*/ int getId() {
return id_;
}
?
/*@ also
@ public normal_behavior
@ requires obj != null && obj instanceof MyGroup;
@ assignable
othing;
@ ensures
esult == (((MyGroup) obj).getId() == id);
@ also
@ public normal_behavior
?
@ requires obj == null || !(obj instanceof MyGroup);
@ assignable
othing;
@ ensures
esult == false;
@*/
public /*@pure@*/ boolean equals(Object obj) {
if (!(obj instanceof MyGroup)) {
return false;
}
return (((MyGroup) obj).getId() == id_);
}
}
缁撴灉濡備笅锛?/span>
缁撳悎鎴戠殑绠€鍗曟牱渚嬪拰澶т浆浠殑姝ｇ粡鏍蜂緥锛屽彲浠ョ湅鍑虹敓鎴愬ぇ閮ㄥ垎鏄壒娈婃儏鍐?杈圭晫鏁版嵁銆傝櫧鐒惰窇鍑烘潵浜嗭紝浣嗕笉鐭ラ亾涓轰粈涔坈onstructor娴嬭瘯涓嶉€氳繃锛燂紵锛熸€讳箣jmlunitng瀹炲湪鏄竴鍓骞存病缁存姢鐨勬牱瀛愶紝鎰熻瀹炵敤鎬у緢灏忥紙閫?/span>
3.鎸夌収浣滀笟姊崇悊鑷繁鐨勬灦鏋勮璁?/span>锛岀壒鍒垎鏋愯嚜宸辩殑妯″瀷鏋勫缓绛栫暐
绗竴娆′綔涓?/span>锛氱被鏋勯€犱笌jml鐩稿悓锛屽鍣ㄧ粺涓€浣跨敤ArrayList锛屾悳绱㈢畻娉曚娇鐢╠fs銆?/span>
绗簩娆′綔涓?/span>锛氬姞鍏roup绫伙紝瀹瑰櫒浠嶇劧鐢ˋrrayList锛坆ug淇涓凡淇敼锛夛紝鎼滅储绠楁硶浣跨敤骞舵煡闆嗐€?/span>
绗笁娆′綔涓?/span>锛氬鍔燫elationship绫伙紝鐢ㄤ簬澶勭悊minPath銆傚鍣ㄥ鍔燞ashMap銆俶inpath浣跨敤bellman-ford绠楁硶锛宻tronglinked鐢ㄤ袱娆fs锛宐locksum鐢ㄥ苟鏌ラ泦銆?/span>
鎬讳綋鏉ヨ鏄寜jml鏉ヨ璁℃灦鏋勩€?/span>
4.鎸夌収浣滀笟鍒嗘瀽浠ｇ爜瀹炵幇鐨刡ug鍜屼慨澶嶆儏鍐?/span>
绗竴娆′綔涓?/span>锛氬己娴?鍒嗭紝鍑虹幇浜嗚秴鏃跺拰bug锛屾妸isCircle浠巄fs鏀规垚骞舵煡闆嗗悗杩囦簡銆?/span>
绗簩娆′綔涓?/span>锛氳繕鏄己娴嬩腑鍑虹幇浜嗚秴鏃跺拰bug锛屽崄鍒嗛毦杩?(
绗竴涓秴鏃跺師鍥犳槸contains鍜実etperson閮芥槸閲嶅鐢ㄧ殑锛屽叏閮ㄦ敼鎺夊悗杩囦簡鍥涗釜鐐广€?/span>
绗簩涓秴鏃跺師鍥犳槸getPerson鐢ˋrrayList锛屽湪璁捐棰戠箒鏌ユ壘鐨勫湴鏂归兘澧炲姞浜咹ashMap涔嬪悗鍙樻垚WA銆?/span>
绗竴涓猙ug鏄痳elationSum鐨凧ML鐞嗚В閿欎簡銆傚洜涓鸿瘎娴嬫彁绀烘槸expect 1 get 0锛屼竴鐩翠互涓烘槸isCircle骞舵煡闆嗗啓閿欎簡锛宒e浜嗗彂鐜板啓鐨勫畬鍏ㄦ病閿欍€備箣鍚庯紝鍦╣ithub涓婂彂鐜颁簡澶т浆鐨勮瘎娴嬫満锛堟劅璋㈠ぇ浣級锛岃嚜宸变慨鏀逛簡涓嬶紝鐬棿鍙戠幇浜哹ug……鍏蜂綋闂鏄病鎶婅嚜宸卞拰鑷繁鐨勫叧绯荤畻杩涘幓锛岃€屼笖绠楃殑涓嶆槸group閲岀殑鏄墍鏈変汉鐨剆um銆?/span>
绗簩涓猙ug鏄繕浜嗚€冭檻<1111銆?/span>
绗笁娆′綔涓?/span>锛氬己娴嬫湁bug锛岃繕娌′慨澶嶏紝浣嗘瘮璧峰墠涓ゆ鐨勬儴鐘惰繕鏄湁杩涙鐨勩€俶inpath鐢ㄤ簡Bellman-Ford銆俿tronglinked鐢ㄤ簡dfs锛屾湁bug……
绠楁硶鏁堢巼鍜孞ML缁嗚妭鏂归潰閮藉嚭鐜颁簡涓ラ噸闂锛屽湪debug杩囩▼涓姞娣变簡瀵笿ML鐨勭悊瑙ｃ€?/span>
5.闃愯堪瀵硅鏍兼挵鍐欏拰鐞嗚В涓婄殑蹇冨緱浣撲細
以上是关于OO绗笁鍗曞厓鎬荤粨的主要内容，如果未能解决你的问题，请参考以下文章