【IT168 技術文章】面向對象分析和設計的原則之一就是應當盡可能地把過程設想往后推。我們大多數人只在實現方法之前遵守這一規則。一旦確定了類及其接口并該開始實現方法時，我們就轉向了過程設想。那么到底有沒有別的選擇?和大多數語言一樣，編寫 Java 代碼時，我們需要為計算每個方法的結果一步一步地提供過程。

就其本身而言，過程化表示法只是說 如何做某事，卻不曾說過我們正在設法做 什么。在動手之前了解我們想要取得的結果，這可能會有用，但是 Java 語言沒有提供顯式地將這種信息合并到代碼中的方法。

Java 建模語言(JML)將注釋添加到 Java 代碼中，這樣我們就可以確定方法所執行的內容，而不必說明它們如何做到這一點。有了 JML，我們就可以描述方法預期的功能，無需考慮實現。通過這種方法，JML 將延遲過程設想的面向對象原則擴展到了方法設計階段。

JML 為說明性的描述行為引入了許多構造。這些構造包括模型字段、量詞、斷言的可見度范圍、前提條件、后置條件、不變量、合同繼承以及正常行為與異常行為的規范。這些構造使得 JML 的功能變得非常強大，但是沒必要理解或使用所有這些構造，也沒必要馬上使用所有的構造。您可以從簡單的起點開始逐步學習和使用 JML。

在本文中，我們將采取循序漸進的方法來學習 JML。我們將從概述使用 JML 的好處入手，重點講述它對開發和編譯過程的影響。接下來，我們將討論用于前提條件、后置條件、模型字段、量化、副作用和異常行為的 JML 構造。在這個過程中，示例會顯示每種 JML 構造的動機。在本文結尾處，您將對 JML 的工作原理有個概念性的理解，并能將它應用到您自己的程序中。

JML 概述

使用 JML 來說明性地描述所希望的類和方法的行為，可以顯著地改善整個開發過程。將建模表示法添加到 Java 代碼中，其好處包括以下幾點：

能更加精確地描述代碼所完成的任務

能有效地發現和糾正錯誤

能減少隨著應用程序的進展而引入錯誤的機會

能較早地發現客戶沒有正確使用類

能產生始終與應用程序代碼保持同步的精確文檔

JML 注釋始終位于 Java 注解(comment)內部，因此它們不會對進行正常編譯的代碼產生影響。當我們想將類的實際行為與其 JML 規范進行比較時，可以使用開放源碼 JML 編譯器。用 JML 編譯器編譯過的代碼如果沒有做到規范中規定它應該做的事，那么該代碼在運行時會拋出 JML 異常。這不僅能捕獲代碼中的錯誤，還能確保文檔(JML 注釋格式)與代碼保持同步。

在以下幾節中,我將使用開放源碼 Jakarta 公共集合組件(Jakarta Commons Collection Component，JCCC)的 PriorityQueue 接口和 BinaryHeap 類來說明 JML 的特性。

需求和職責

本文的源代碼包括了 JCCC 的 PriorityQueue 接口。 PriorityQueue 接口包含了方法特征符，這些特征符指定了參數和返回值的數據類型，但是沒有說明任何有關方法行為的內容。我們希望能指定 PriorityQueue 的語義，這樣的話實現它的所有類就能以預期的方式運作(在沒有行為規范的情況下，我們最終會得到一個實現了 PriorityQueue 接口的堆棧類，或者其它某種非常規的情況)。

請研究 PriorityQueue 中 pop() 方法。優先級隊列對 pop() 有什么需求呢?有三個基本需求。首先，除非隊列中至少有一個元素，否則不應該調用 pop() 。其次，它應當返回隊列中優先級最高的元素。最后，它應當除去從隊列中返回的元素。

清單 1 演示了表示第一個需求的 JML 注釋：

清單 1. pop() 方法需求的 JML 注釋

1 /*@2 3 @ public normal_behavior4 5 @ requires ! isEmpty();6 7 @*/8 9 Object pop()throwsNoSuchElementException;10

如前面所述，JML 注釋是寫在 Java 注解內部的。包含 JML 的多行注解是以字符 /*@ 開頭的。JML 忽略行中所有作為第一個非空格字符的 @ 符號。JML 還可以寫在以 //@ 開頭的單行注解內部。

這里 JML 中 public 關鍵字的意義和在 Java 語言中的意義是一樣的。 public 表示該 JML 規范對于應用程序中的其它所有類都是可見的。公共規范只能涉及公共方法和成員變量。JML 還允許規范擁有 private 、 protected 或 package 級別的作用域。JML 的作用域規則與 Java 語言中的相應規則類似。

normal_behavior 關鍵字表示該規范描述了 pop() 正常返回而沒有拋出異常的情況。隨后我們將討論如何確定異常行為。

前提條件和后置條件

JML 關鍵字 requires 用于前提條件。 前提條件(precondition)指的是在調用方法之前必須要滿足的條件。清單 1 指出 pop() 的前提條件是 isEmpty() 返回 false ;也就是說，隊列中至少要包含一項。

方法的 后置條件(postcondition)指定該方法的職責;也就是說，當方法返回時，后置條件應當是 true。在我們的示例中， pop() 應當返回隊列中擁有最高優先級的元素。我們希望指定該后置條件，這樣 JML 就可以在運行時檢查它。要做到這一點，我們需要清楚已經添加到優先級隊列中的所有值，以便確定 pop() 應當返回哪一個值。我們可以考慮將一個成員變量添加到 PriorityQueue 以便在隊列中存儲這些值，但是這里有兩個問題：

PriorityQueue 是一個接口，因此它應當與不同的實現(比如二進制堆、Fibonacci 堆或日歷隊列)兼容。 PriorityQueue 的 JML 注釋不應當描述任何有關實現的內容。

作為接口， PriorityQueue 只能包含靜態成員變量。

JML 用 模型字段的概念解決了這一兩難局面。

模型字段

模型字段類似于只能在行為規范中使用的成員變量。下面有一個在 PriorityQueue 中使用的模型字段聲明示例：

//@ public model instance JMLObjectBag elementsInQueue;

該聲明指出有一個模型字段 elementsInQueue ，其數據類型為 JMLObjectBag (屬于 JML 的 bag 數據類型)。 instance 關鍵字表示：即使該字段是在接口中進行聲明的，也要在實現 PriorityQueue 的類的每個實例中分別放置該字段的非靜態副本。和所有 JML 注釋一樣， elementsInQueue 的聲明出現在 Java 注解中，因此 elementsInQueue 不能用于正規的 Java 代碼中。沒有哪個對象會在運行時包含 elementsInQueue 字段。

elementsInQueue 包含了添加到優先級隊列的值。清單 2 顯示了 pop() 的規范是如何利用 elementsInQueue 的：

清單 2. pop() 的后置條件中所使用的模型字段

1 /*@2 3 @ public normal_behavior4 5 @ requires ! isEmpty();6 7 @ ensures8 9 @ elementsInQueue.equals(((JMLObjectBag)10 11 @ \old(elementsInQueue))12 13 @ .remove(\result)) &&14 15 @ \result.equals(\old(peek()));16 17 @*/18 19 Object pop()throwsNoSuchElementException;20 21

ensures 關鍵字指出其后跟的是 pop() 返回時必須滿足的后置條件。 \result 是 JML 關鍵字，它等于 pop() 所返回的值。 \old() 是 JML 函數，在調用 pop() 之前它返回其參數所具有的值。

ensures 子句包含兩個后置條件。第一個指出將 pop() 所返回的值從 elementsInQueue 中除去。第二個指出返回值和 peek() 返回的值一樣。

類級不變量

我們已經看到 JML 允許我們指定方法的前提條件和后置條件。它還允許我們指定類級不變量。類級不變量是這樣的條件：即在類中每個方法的入口和出口處這些條件都必須為 true。例如， //@ public instance invariant elementsInQueue != null; 是 PriorityQueue 的不變量，這就是說，在實現 PriorityQueue 的類的構造函數返回之后， elementsInQueue 無論何時都不能是 null。

總結

以上是生活随笔為你收集整理的java jml_JML 入门的全部內容，希望文章能夠幫你解決所遇到的問題。

如果覺得生活随笔網站內容還不錯，歡迎將生活随笔推薦給好友。