key
KeY-2.12.2 (2023-11-10)
Repositori ini adalah rumah dari kunci prover teorema interaktif untuk verifikasi formal dan analisis program Java. Key hadir sebagai aplikasi GUI mandiri, yang memungkinkan Anda untuk memverifikasi kebenaran fungsional program JAVA sehubungan dengan spesifikasi formal yang diformulasikan dalam bahasa pemodelan Java JML. Selain itu, kunci juga dapat digunakan sebagai perpustakaan misalnya untuk eksekusi program simbolik, penalaran urutan pertama, atau pembuatan kasus uji.
Untuk informasi lebih lanjut, lihat
java.util.IdentityHashMap ,LinkedListVersi kunci saat ini adalah 2.12.2, dilisensikan di bawah GPL V2.
Jangan ragu untuk menggunakan templat proyek untuk memulai menggunakan kunci:
Folder ini menyediakan proyek yang dikelola lulusan mengikuti tata letak folder standar Maven. Ada beberapa subproyek di folder ini. Secara umum, setiap key.*/ Subproyject berisi komponen inti kunci. Komponen tambahan dan opsional ada di keyext.*/ Folder. File build.gradle adalah skrip build root yang menggambarkan ketergantungan dan tugas build umum untuk semua subproyek.
key.util , key.core dan key.ui adalah basis untuk produk "Pepatah Kunci". Perawatan khusus diperlukan jika Anda berencana untuk melakukan perubahan di sini.
Dengan asumsi Anda berada di direktori file ReadMe ini, Anda dapat membuat versi yang dapat dilalui dan dapat digunakan dengan salah satu perintah ini:
Dengan ./gradlew key.ui:run Anda dapat menjalankan antarmuka pengguna kunci langsung dari repositori. Gunakan ./gradlew key.ui:run --args='--experimental' untuk mengaktifkan fitur eksperimental.
Gunakan ./gradlew classes untuk mengkompilasi kunci, yang termasuk menjalankan javacc dan antlr. Demikian juga, gunakan ./gradlew testClasses Jika Anda juga ingin mengkompilasi kelas tes junit.
Uji instalasi Anda dengan ./gradlew test . Ketahuilah bahwa ini biasanya akan memakan waktu beberapa jam untuk diselesaikan. Dengan ./gradlew testFast , Anda dapat menjalankan suite tes yang lebih ringan yang harus diselesaikan dalam beberapa menit.
Anda dapat memilih kasus uji tertentu dengan argumen --tests . Wildcard diperbolehkan.
./gradlew :key. < subproject > :test --tests " <class>.<method> " Anda dapat men-debug kunci dengan menambahkan opsi --debug-jvm , kemudian melampirkan debugger di localhost:5005 .
Anda dapat membuat satu jar-versi, alias toples gemuk , dari kunci dengan
./gradlew :key.ui:shadowJar File ini dihasilkan di key.ui/build/libs/key-*-exe.jar .
Distribusi dibangun dengan
./gradlew :key.ui:installDist :key.ui:distZip Distribusi dapat diuji dengan menelepon key.ui/install/key/bin/key.ui dan distribusi key.ui/build/distributions .
Distribusi memberi Anda potensi menggunakan file jar tunggal.
Kualitas dinilai secara otomatis menggunakan Sonarqube pada setiap permintaan tarik. Hasil penilaian (lulus/gagal) dapat diperiksa di bagian cek PR.
Aturan dan Gerbang Kualitas dikelola oleh Alexander Weigl [email protected] saat ini.
Lebih banyak pedoman dan dokumentasi untuk pengembangan utama dapat ditemukan di bawah DOCS.
Untuk laporan bug, silakan gunakan pelacak masalah atau kirim surat ke [email protected].
Untuk diskusi, Anda mungkin ingin berlangganan dan menggunakan milis [email protected] atau menggunakan diskusi github.
Jangan ragu untuk mengirimkan permintaan tarik melalui GitHub. Permintaan tarik dinilai menggunakan tes otomatis, pemformatan dan pemeriksa sumber statis, serta tinjauan manual oleh salah satu pengembang. Lebih banyak pedoman dan dokumentasi untuk pengembangan utama dapat ditemukan di bawah 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.
