Java PathFinder 是 NASA 項目的結果。它主要是在 NASA 軟件模型研究中心開發的，現在仍然在使 用。Java PathFinder 項目是一個軟件模型檢查的可行性研究，開始於 1999 年。從那時起它便開始了通 往學術研究和工業之路，它甚至在實際太空船缺陷檢測中也發揮過作用。
Java PathFinder 是一個用來驗證可執行 Java bytecode 程序的系統。它的基本形式是用作顯式聲明 軟件模型檢查程序的 Java 虛擬機 (JVM)，從系統上探測程序所有可能的執行路徑，以避免死鎖或未處理 異常之類的情況發生。與傳統的調試程序不同，Java PathFinder 報告導致缺陷的整個執行路徑。Java PathFinder 特別適合在多線程的程序中發現很難測試的並發缺陷。
入門要入門，首先需要設置您的環境。驗證環境設置正確之後，您將准備獲得 Java PathFinder 源文 件，然後從 NetBeans 中構建並運行它。
本文檔中的說明是從 Windows 用戶的角度提出的。Solaris 和 Linux 用戶應該針對其平台在適用的 地方替換路徑名、安裝程序名等。
設置環境構建和運行 Java PathFinder 之前，您需要安裝幾個附加組件。完成此操作的最簡單方法是 下載所有組件，然後按照下文列出的順序安裝它們。
下載組件
注意： 安裝說明假設您將所有組件下載到 C:\tmp 中。
Java 2 SDK 標准版本 1.4.2 或 1.5.0 或更高版本（如果尚未安裝）。
http://java.sun.com/j2se/1.5.0/download.jsp
注意： 下面的說明假設您下載了 Windows 版本的 JDK。
NetBeans 4.1 IDE（如果您未安裝 NetBeans）
http://www.netbeans.info/downloads/download.php?type=4.1rc1
注意： 如果您沒有打算進行 J2EE 開發，則可以下載 NetBeans 4.1 RC 安裝程序 (netbeans-4_1- rc1-windows.exe) 版本。
Java PathFinder Convenience Libraries
http://sourceforge.net/project/showfiles.php? group_id=136825&package_id=151191&release_id=323978
這個文件是 jpf-lib.zip，它包含 Java PathFinder 所需的 .jar 文件。
安裝組件
下載所有組件之後，按照下面的說明安裝它們。
如果您尚未安裝 1.4.2 或 1.5.0 或更高版本的 JDK，則安裝 Java 2 SDK：
轉到下載 JDK 的 C:\tmp 目錄，然後雙擊 jdk-1_5_0_02-windows-i586-install.exe 文件即可啟動 JDK 的安裝。按照 JDK 安裝程序給出的說明來安裝 JDK。
如果您尚未安裝 NetBeans，則安裝 NetBeans IDE：
轉到下載 NetBeans 的 C:\tmp 目錄，然後雙擊 netbeans-4_1-rc1-windows.exe 文件即可啟動 NetBeans 的安裝。按照 NetBeans 安裝程序給出的說明來安裝 NetBeans。
您已經具有構建 Java PathFinder 所需的環境了，現在開始准備啟動 NetBeans、獲得 Java PathFinder 源代碼、從源中構建 Java PathFinder 並從 NetBeans 中運行所有 Java PathFinder。
啟動 NetBeans
要啟動 NetBeans，請雙擊桌面上的 NetBeans 4.1 圖標。如果您在 Solaris 或 Linux 上，則通過在 終端窗口中鍵入 netbeans 來啟動 NetBeans。
獲得 Java PathFinder 源代碼
下一步是配置 NetBeans IDE 以從 sourceforge.net CVS 存儲庫中檢索 Java PathFinder 源代碼。
在 NetBeans IDE 中，從主菜單中選擇 Versioning > CVS > Check Out，如下面的圖 1 所示 。
圖 1 Versioning > CVS > Check Out
選擇 Versioning > CVS > Check Out 菜單項之後，您將看到“Enabling Advanced CVS Command Options”對話框，如圖 2 所示。
圖 2 Enabling Advanced CVS Command Options
如果您以後不想看到這個對話框，則轉到前面並勾選上圖 2 中所示的“Do Not Show This Dialog Box Again”標簽旁邊的復選框，然後按 Check Out 按鈕。
接下來您將看到“CVS Checkout”對話框。在這個屏幕上您需要輸入幾個值。在此屏幕上應該輸入以 下每個值。
Working Directory: <source path where to place Java PathFinder source files>
記住這個目錄路徑，之後您需要再次輸入它
CVS Server Type: pserver
CVS Server Name: cvs.sourceforge.net
Port: 2401
User Name: anonymous
Repository Path: /cvsroot/javapathfinder
選擇“Use Built-in CVS Client”
Password:<此處不填>
保留 Modules 和 Revision 字段為空
Module(s):<此處不填>
Revision or Tag:<此處不填>
CVS Checkout 窗體的外觀類似於下圖 3 中所示的窗體外觀。
圖 3 CVS Checkout
如果您在 Password 字段和 Login 按鈕下面看到“You are not logged in.”消息，則您需要登錄。 如果您看到這個消息，則立即按 Login 按鈕。標簽將更改為“You are logged in”，如上圖 3 所示。
我的開發環境中的 CVS Checkout 窗體如下圖 4 所示。
圖 4 已登錄的 CVS Checkout
完成 CVS Checkout 窗體之後，顯示“you are logged in”，然後按“Ok”按鈕。
按“Ok”按鈕之後，CVS Checkout 窗體將消失，您將注意到 NetBeans IDE 底部的輸出窗口將顯示運 行 CVS 簽出的 VCS Output。這個 VCS Output 窗口中的輸出非常類似於下面圖 5 中所示的輸出。
圖 5 VCS Output 窗口
完成 CVS 簽出之後， VCS Output 窗口底部的狀態消息將顯示已經完成簽出。
安裝 Java PathFinder Convenience Libraries
您的系統上已經存在 Java PathFinder 源的文件夾了，下一步將是解壓縮 jpf-lib.zip 文件。
指定 CVS Checkout 的工作目錄時，NetBeans 在該工作目錄中已創建了 javapathfinder 文件夾。這 個 javapathfinder 文件夾包含一個 lib 文件夾。PathFinder 的 build.xml 可在 lib 文件夾中找到以 下三個 .jar 文件：bcel.jar、fast-MD5.jar 和 xercesImpl.jar。將 jpf-lib.zip 的內容解壓縮到 javapathfinder 文件夾。
在 NetBeans 中設置 Java PathFinder 項目
現在您的系統上已經存在 Java PathFinder 源文件了，下一步將創建用於構建和運行 Java PathFinder 的 NetBeans 項目。
從主菜單中選擇 File > New Project，如下圖 6 所示。
圖 6 創建一個新項目
選擇 File > New Project 菜單項之後，將出現 New Project 向導，如圖 7 所示。
圖 7 New Project 向導
在 New Project 向導中，選擇 General 項目類別和 Java Project with Existing Ant Script 項目 類型，如上圖 7 所示。然後按 Next 按鈕。這將出現 New Project 向導的第二個屏幕。在此窗體上，指 定項目文件、Ant 構建腳本的位置，並提供項目名稱和項目文件夾。
對於 Location 字段，浏覽到之前告知 NetBeans 下載 Java PathFinder 源文件時指定的工作目錄， 然後選擇“javapathfinder”目錄作為 Java PathFinder 源文件所在的位置。NetBeans IDE 將自動查找 Ant 構建腳本並指定項目名稱和項目文件夾。您可以接受 NetBeans 為項目名稱和項目文件夾選擇的默認 值，如果願意也更改它們。
下圖 8 顯示的屏幕快照示例中是我在開發環境中所使用的值，以及 NetBeans 為項目名稱和項目文件 夾自動填充的默認值。
圖 8 項目名稱和位置
選擇項目名稱和位置之後，按 Next 按鈕。這將把您帶到 New Project 向導的 Build and Run Actions 窗體。您將注意到 NetBeans 會自動將 Ant 構建目標映射到 NetBeans 操作。下圖 9 顯示了 NetBeans 自動選擇映射的示例。
圖 9 Build and Run Actions
按 Next 按鈕接受默認的映射。（注意：通過只選擇一個下拉框並選擇另一個 Ant 構建目標，可以更 改默認映射中的任何一個。）
按 Next 按鈕之後，將顯示 New Project 向導的 Source Package Folders 窗體。在該窗體上，為您 的項目指定源目錄。要添加源包文件夾，單擊該窗體 Source Package Folder 部分中的 Add Folder 按 鈕。浏覽到之前在 CVS 窗體中指定為 Working Directory 的目錄，然後打開 javapathfinder 目錄。然 後，選擇並打開 src 文件夾。之後，按向導的 Test Package Folders 部分中的 Add Folder 按鈕添加 測試包文件夾。浏覽到之前在 CVS 窗體中指定為 Working Directory 的目錄，然後打開 javapathfinder 目錄。然後，選擇並打開 test 文件夾。
要在該窗體上設置的最後一項是 Source Level。通過選擇 Source Level 下拉框並選擇 JDK 1.4 將 源級別設置為 JDK 1.4。
Source Package Folders 向導的外觀類似於下圖 10 所示的向導外觀。
圖 10 Source Package Folders
按 Next 按鈕轉到 Java Sources Classpath 窗體。在該窗體上，您告知 NetBeans 查找三個附加組 件（BCEL、Xerces 和 MD5）的位置，編輯器將使用這些組件執行各種任務，如語法檢查、代碼完成和導 入聲明。這三個組件的 .jar 文件位於 javapathfinder/lib 文件夾中。
在該窗體上添加三個組件中的每個組件。我為開發環境添加這三個組件之後的屏幕示例如圖 11 所示 。
圖 11 Java Sources Classpath
添加三個組件之後，按 Finish 按鈕。
您現在將注意到在 NetBeans 項目窗口中顯示了新項目。NetBeans 項目窗口的外觀類似於圖 12 中所 示的窗口外觀。
圖 12 NetBeans 項目窗口
現在，您已經成功地在 NetBeans 中創建並配置了 Java PathFinder 項目。接下來准備在 NetBeans 中構建並運行 Java PathFinder。
在 NetBeans 中構建和運行 Java PathFinder 項目
在 NetBeans 項目窗口中，右鍵單擊新創建的 Java PathFinder 項目。您可以選擇構建將編譯 Java PathFinder 項目的項目，也可以選擇運行構建項目並運行 Java PathFinder 測試套件的項目。
在項目窗口中右鍵單擊 Java PathFinder 項目時，您將看到的選項如下圖 13 所示。
圖 13 運行 Java PathFinder 項目
選擇圖 13 中所示的“Run Project”運行項目。如果 Java PathFinder 項目尚未構建，則這會啟動 構建該項目並在構建之後運行測試套件。您將注意到 NetBeans IDE 底部的輸出窗口將顯示構建和運行 Java PathFinder 項目的結果。構建和運行 Java PathFinder 項目的 NetBeans 輸出窗口的示例如下。
圖 14 NetBeans Output 窗口
這就是擁有在 NetBeans 中構建和運行 Java PathFinder 的環境的全部內容。是不是很簡單？
