【IT168 技術(shù)文章】面向?qū)ο蠓治龊驮O(shè)計(jì)的原則之一就是應(yīng)當(dāng)盡可能地把過程設(shè)想往后推。我們大多數(shù)人只在實(shí)現(xiàn)方法之前遵守這一規(guī)則。一旦確定了類及其接口并該開始實(shí)現(xiàn)方法時(shí)，我們就轉(zhuǎn)向了過程設(shè)想。那么到底有沒有別的選擇?和大多數(shù)語言一樣，編寫 Java 代碼時(shí)，我們需要為計(jì)算每個(gè)方法的結(jié)果一步一步地提供過程。

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

Java 建模語言(JML)將注釋添加到 Java 代碼中，這樣我們就可以確定方法所執(zhí)行的內(nèi)容，而不必說明它們?nèi)绾巫龅竭@一點(diǎn)。有了 JML，我們就可以描述方法預(yù)期的功能，無需考慮實(shí)現(xiàn)。通過這種方法，JML 將延遲過程設(shè)想的面向?qū)ο笤瓌t擴(kuò)展到了方法設(shè)計(jì)階段。

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

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

JML 概述

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

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

能有效地發(fā)現(xiàn)和糾正錯(cuò)誤

能減少隨著應(yīng)用程序的進(jìn)展而引入錯(cuò)誤的機(jī)會(huì)

能較早地發(fā)現(xiàn)客戶沒有正確使用類

能產(chǎn)生始終與應(yīng)用程序代碼保持同步的精確文檔

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

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

需求和職責(zé)

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

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

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

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

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

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

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

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

前提條件和后置條件

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

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

PriorityQueue 是一個(gè)接口，因此它應(yīng)當(dāng)與不同的實(shí)現(xiàn)(比如二進(jìn)制堆、Fibonacci 堆或日歷隊(duì)列)兼容。 PriorityQueue 的 JML 注釋不應(yīng)當(dāng)描述任何有關(guān)實(shí)現(xiàn)的內(nèi)容。

作為接口， PriorityQueue 只能包含靜態(tài)成員變量。

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

模型字段

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

//@ public model instance JMLObjectBag elementsInQueue;

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

elementsInQueue 包含了添加到優(yōu)先級隊(duì)列的值。清單 2 顯示了 pop() 的規(guī)范是如何利用 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 關(guān)鍵字指出其后跟的是 pop() 返回時(shí)必須滿足的后置條件。 \result 是 JML 關(guān)鍵字，它等于 pop() 所返回的值。 \old() 是 JML 函數(shù)，在調(diào)用 pop() 之前它返回其參數(shù)所具有的值。

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

類級不變量

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

總結(jié)

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

如果覺得生活随笔網(wǎng)站內(nèi)容還不錯(cuò)，歡迎將生活随笔推薦給好友。