key

鑰匙 - 演繹Java程序驗證者

該存儲庫是對Java程序進行正式驗證和分析的交互式定理供應密鑰的所在地。 Key是獨立的GUI應用程序，它使您可以驗證Java程序在Java建模語言JML中提出的正式規格的功能正確性。此外，密鑰還可以用作庫，例如符號程序執行，一階推理或測試案例生成。

有關更多信息，請參閱

• 關鍵主頁
• 關鍵書
• 關鍵開發人員文檔
• 鑰匙的成功案例：
  • 在JDK分類常規（Timsort）中發現的嚴重錯誤，
  • java.util.IdentityHashMap的驗證，
  • Google分析LinkedList中的錯誤獎

當前版本的KEY為2.12.2，根據GPL V2許可。

隨意使用項目模板開始使用密鑰開始：

• 用於驗證項目
• 用作圖書館
• 用作符號執行後端

要求

• 硬件：> = 2 GB RAM
• 操作系統：Linux/Unix，MacOSX，Windows
• Java 17或更新
• 可選地，鑰匙可以利用以下二進製文件：
  • SMT求解器：
    • Z3
    • CVC5
    • CVC4
    • 公主

關鍵文件夾的內容

該文件夾在Maven的標准文件夾佈局之後提供了一個由Gradle管理的項目。該文件夾中有幾個子項目。通常，每個key.*/ subproject包含鍵的核心組件。其他和可選的組件在keyext.*/文件夾。文件build.gradle是root構建腳本，描述了所有子項目的依賴關係和常見的構建任務。

key.util ， key.core和key.ui是產品“密鑰供體”的基礎。如果您打算在此處進行更改，則需要特殊護理。

編譯和運行鍵

假設您位於此REDME文件的目錄中，則可以使用其中一個命令創建可運行且可部署的版本：

1. 使用./gradlew key.ui:run您可以直接從存儲庫運行鍵的用戶界面。使用./gradlew key.ui:run --args='--experimental'以實現實驗特徵。

2. 使用./gradlew classes來編譯密鑰，其中包括運行JavACC和ANTLR。同樣，如果您還想編譯JUNIT測試類，請使用./gradlew testClasses 。

3. 使用./gradlew test測試安裝。請注意，這通常需要幾個小時才能完成。使用./gradlew testFast ，您可以在幾分鐘內運行更輕巧的測試套件。

   您可以選擇具有--tests參數的特定測試用例。允許通配符。

   ./gradlew :key. < subproject > :test --tests " <class>.<method> "

   您可以通過添加--debug-jvm選項來調試鍵，然後在localhost:5005 。

4. 您可以使用單個罐子轉換，又稱fat jar的鑰匙

   ./gradlew :key.ui:shadowJar

   該文件是在key.ui/build/libs/key-*-exe.jar中生成的。

5. 分佈構建

   ./gradlew :key.ui:installDist :key.ui:distZip

   可以通過調用key.ui/install/key/bin/key.ui進行測試，並在key.ui/build/distributions中進行zy。

   該分佈使您有可能使用單個JAR文件。

開發密鑰

• 在每個拉的請求下使用Sonarqube自動評估質量。可以在PR的“檢查”部分中檢查評估結果（通過/失敗）。

  目前，Alexander Weigl [email protected]維護了規則和質量大門。

• 有關關鍵開發的更多指南和文檔，可以在密鑰內部找到。

問題和錯誤報告

• 有關錯誤報告，請使用問題跟踪器或發送郵件到[email protected]。

• 為了討論，您可能需要訂閱並使用郵件列表[email protected]或使用github討論。

為關鍵做出貢獻

隨時通過GitHub提交拉動請求。使用自動測試，格式和靜態源檢查器以及其中一位開發人員的手動審查評估拉力請求。有關關鍵開發的更多準則和文檔可以在鑰匙單位下找到。

許可註釋

 This is the KeY project - Integrated Deductive Software Design
Copyright (C) 2001-2011 Universität Karlsruhe, Germany
						Universität Koblenz-Landau, Germany
						and Chalmers University of Technology, Sweden
Copyright (C) 2011-2024 Karlsruhe Institute of Technology, Germany
						Technical University Darmstadt, Germany
						Chalmers University of Technology, Sweden

The KeY system is protected by the GNU General Public License.
See LICENSE.TXT for details.