key

キー - 演ductiveジャバプログラム検証者

このリポジトリは、Javaプログラムの正式な検証と分析のためのインタラクティブ定理プロバーキーの本拠地です。キーは、Javaモデリング言語JMLで定式化された正式な仕様に関して、Javaプログラムの機能的正しさを検証できるスタンドアロンGUIアプリケーションとして提供されます。さらに、キーは、シンボリックプログラムの実行、一次推論、またはテストケース生成のためのライブラリとしても使用できます。

詳細については、参照してください

• キーホームページ
• キーブック
• 主要な開発者ドキュメント
• キーのサクセスストーリー：
  • JDKソーティングルーチン（TIMSORT）で発見された深刻なバグ、
  • java.util.IdentityHashMapの検証、
  • LinkedListのバグを分析したGoogle賞

キーの現在のバージョンは2.12.2で、GPL V2でライセンスされています。

プロジェクトテンプレートを自由に使用して、キーを使用して開始してください。

• 検証プロジェクト
• ライブラリとして使用します
• シンボリック実行バックエンドとして使用します

要件

• ハードウェア：> = 2 GB RAM
• オペレーティングシステム：Linux/Unix、MacOSX、Windows
• Java 17以降
• オプションで、キーは次のバイナリを利用できます。
  • SMTソルバー：
    • Z3
    • CVC5
    • CVC4
    • お姫様

キーフォルダーのコンテンツ

このフォルダーは、Mavenの標準フォルダーレイアウトに続いて、Gradle-Managedプロジェクトを提供します。このフォルダーにはいくつかのサブプロジェクトがあります。一般に、すべてのkey.*/サブプロジェクトには、キーのコアコンポーネントが含まれています。追加およびオプションのコンポーネントはkeyext.*/フォルダーにあります。ファイルbuild.gradle 、すべてのサブプロジェクトの依存関係と共通ビルドタスクを説明するルートビルドスクリプトです。

key.util 、 key.core 、 key.ui 、製品「キープロバー」のベースです。ここで変更を行う予定がある場合は、特別な注意が必要です。

コンパイルしてキーを実行します

このreadmeファイルのディレクトリにあると仮定すると、これらのコマンドのいずれかを使用して実行可能で展開可能なバージョンを作成できます。

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. キーの単一の瓶バージョン、別名ファットジャーを作成できます

   ./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でzippedされます。

   分布により、単一のJARファイルを使用する可能性があります。

キーの開発

• 品質は、各プルリクエストでSonarqubeを使用して自動的に評価されます。評価の結果（合格/失敗）は、PRのチェックセクションで検査できます。

  ルールと品質のゲートは、現在Alexander [email protected]によって維持されています。

• キー開発のためのより多くのガイドラインとドキュメントは、Key-Docsの下で見つけることができます。

問題とバグレポート

• バグレポートについては、問題トラッカーを使用するか、[email protected]にメールを送信してください。

• ディスカッションについては、メーリングリストの[email protected]を購読して使用するか、githubディスカッションを使用することをお勧めします。

キーに貢献します

Github経由でPullリクエストをお気軽に送信してください。プル要求は、自動テスト、フォーマット、静的ソースチェッカー、および開発者の1人による手動レビューを使用して評価されます。キー開発のためのより多くのガイドラインとドキュメントは、Key-Docsの下で見つけることができます。

ライセンスの発言

 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.