Java建模語言是否可執行？

我學習軟件工程課程，在那裏我看到了JML的使用。下面是一段代碼示例：Java建模語言是否可執行？

//@ requires f >= 0.0 
public float sqrt(float f) { 
    return f/2; 
}

它說正式的JML規範是可執行的！

我的問題是，當我們調用與F = -4這個sqrt函數，這段代碼給出錯誤或拋出一個異常，或給予任何警告？我在我的電腦上試過它，它運行良好並打印出-2。那麼這意味着JML是可執行的？爲什麼我們不使用評論來做到這一點？誰能解釋一下？

感謝

來源

2013-05-28 yrazlik

好，這裏是代碼，我問一些有關的代碼。我不明白downvote！ – yrazlik

JML不是Java的一部分。這是一個由研究人員聯盟設計的擴展，但沒有官方的支持。因此，JML註釋不被Java編譯器考慮，但你可以編譯一個特殊的編譯器JML標註的Java程序，使得可執行規範將被考慮在內。例如，JML4C。

來源

2013-05-28 21:43:38

謝謝，這有幫助 – yrazlik

你是不是做的平方根（Math.sqrt(f)，見http://docs.oracle.com/javase/6/docs/api/java/lang/Math.html#sqrt(double)），用2（f/2）劃分。所以這沒什麼不妥。你需要的是使用Math.sqrt（...），如果這是我認爲你需要查看你的方法的名稱。

來源

2013-05-28 21:37:53

其實在這裏並不重要。我只是想知道這一點：我給出了一個函數的前提條件，即參數必須> = 0，但是我用參數<0調用它，它可以工作。如果JML是可執行的，爲什麼會出現這種情況？爲什麼沒有錯誤或警告？ – yrazlik

哦，那麼在這種情況下，我認爲你錯過了行末的最後一個';'。 –

那麼，這個代碼本身不會爲你創建的任何警告。存在各種工具，這使得使用JML規格，例如：

jmlrac：執行
ESC/Java2的：靜態驗證;編譯時證明合同未有違反
jmldoc：javadoc樣式的文件
jmlc：斷言檢查編譯
jmlunit：單元測試工具

除此之外，JML規範，如果正確使用，向外國讀者/代碼維護人員展示程序員的意圖。

來源

2013-05-28 21:46:19 McMannus

Java建模語言是否可執行？

回答

相關問題