key

คีย์ - โปรแกรมตรวจสอบโปรแกรม Java Deductive

ที่เก็บนี้เป็นบ้านของคีย์ทฤษฎีบททฤษฎีบทแบบโต้ตอบสำหรับการตรวจสอบอย่างเป็นทางการและการวิเคราะห์โปรแกรม Java คีย์มาเป็นแอปพลิเคชั่น GUI แบบสแตนด์อโลนซึ่งช่วยให้คุณตรวจสอบความถูกต้องในการทำงานของโปรแกรม Java ที่เกี่ยวข้องกับข้อกำหนดที่เป็นทางการที่กำหนดไว้ในภาษา Java แบบจำลอง JML ยิ่งไปกว่านั้นคีย์ยังสามารถใช้เป็นไลบรารีเช่นสำหรับการดำเนินการโปรแกรมสัญลักษณ์การให้เหตุผลการสั่งซื้อครั้งแรกหรือการสร้างกรณีทดสอบ

สำหรับข้อมูลเพิ่มเติมอ้างอิง

• หน้าแรกที่สำคัญ
• หนังสือสำคัญ
• เอกสารสำคัญของนักพัฒนาซอฟต์แวร์
• เรื่องราวความสำเร็จของคีย์:
  • ข้อผิดพลาดอย่างรุนแรงที่ค้นพบในกิจวัตรการเรียงลำดับ JDK (Timsort)
  • การตรวจสอบ java.util.IdentityHashMap
  • Google Award สำหรับการวิเคราะห์ข้อผิดพลาดใน LinkedList

คีย์เวอร์ชันปัจจุบันคือ 2.12.2 ซึ่งได้รับอนุญาตภายใต้ GPL V2

อย่าลังเลที่จะใช้เทมเพลตโครงการเพื่อเริ่มต้นใช้คีย์:

• สำหรับโครงการตรวจสอบ
• ใช้เป็นห้องสมุด
• ใช้เป็นแบ็กเอนด์การดำเนินการเชิงสัญลักษณ์

ความต้องการ

• ฮาร์ดแวร์:> = 2 gb ram
• ระบบปฏิบัติการ: Linux/UNIX, MacOSX, Windows
• Java 17 หรือใหม่กว่า
• ทางเลือกคีย์สามารถใช้ประโยชน์จากไบนารีต่อไปนี้:
  • SMT Solvers:
    • Z3
    • CVC5
    • CVC4
    • เจ้าหญิง

เนื้อหาของโฟลเดอร์คีย์

โฟลเดอร์นี้จัดทำโครงการที่มีการจัดการ Gradle ตามเลย์เอาต์โฟลเดอร์มาตรฐานของ Maven โฟลเดอร์ย่อยมีหลายโครงการในโฟลเดอร์นี้ โดยทั่วไปแล้วทุก key.*/ โครงการย่อยมีองค์ประกอบหลักของคีย์ ส่วนประกอบเพิ่มเติมและเป็นทางเลือกอยู่ใน keyext.*/ โฟลเดอร์ ไฟล์ build.gradle เป็นสคริปต์บิลด์รูทที่อธิบายถึงการพึ่งพาและงานบิลด์ทั่วไปสำหรับโครงการย่อยทั้งหมด

key.util , key.core และ key.ui เป็นฐานสำหรับผลิตภัณฑ์ "Key Prover" จำเป็นต้องมีการดูแลเป็นพิเศษหากคุณวางแผนที่จะเปลี่ยนแปลงที่นี่

รวบรวมและเรียกใช้คีย์

สมมติว่าคุณอยู่ในไดเรกทอรีของไฟล์ readme นี้คุณสามารถสร้างเวอร์ชันที่เรียกใช้และปรับใช้ได้ด้วยหนึ่งในคำสั่งเหล่านี้:

1. ด้วย ./gradlew key.ui:run คุณสามารถเรียกใช้ส่วนต่อประสานผู้ใช้ของคีย์ได้โดยตรงจากที่เก็บ ใช้ ./gradlew key.ui:run --args='--experimental' เพื่อเปิดใช้งานคุณสมบัติการทดลอง

2. ใช้ ./gradlew classes เพื่อรวบรวมคีย์ซึ่งรวมถึงการเรียกใช้ Javacc และ Antlr ในทำนองเดียวกันให้ใช้ ./gradlew testClasses หากคุณต้องการรวบรวมคลาสทดสอบ Junit

3. ทดสอบการติดตั้งของคุณด้วย ./gradlew test โปรดทราบว่าสิ่งนี้มักจะใช้เวลาหลายชั่วโมงกว่าจะเสร็จสมบูรณ์ ด้วย ./gradlew testFast คุณสามารถเรียกใช้ชุดทดสอบที่มีน้ำหนักเบามากขึ้นซึ่งควรทำให้เสร็จภายในไม่กี่นาที

   คุณสามารถเลือกกรณีทดสอบเฉพาะด้วยอาร์กิวเมนต์ --tests ทดสอบ อนุญาตให้ใช้สัญลักษณ์แทน

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

   คุณสามารถดีบักคีย์ได้โดยเพิ่มตัวเลือก --debug-jvm จากนั้นแนบตัวดีบักที่ localhost:5005

4. คุณสามารถสร้าง jar-version, aka 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

   การแจกแจงให้คุณมีศักยภาพในการใช้ไฟล์ JAR เดียว

การพัฒนากุญแจ

• คุณภาพจะถูกประเมินโดยอัตโนมัติโดยใช้ Sonarqube ในแต่ละคำขอดึง ผลลัพธ์ของการประเมิน (ผ่าน/ล้มเหลว) สามารถตรวจสอบได้ในส่วนการตรวจสอบของ PR

  กฎและประตูคุณภาพได้รับการดูแลโดย Alexander Weigl [email protected] ในปัจจุบัน

• แนวทางเพิ่มเติมและเอกสารประกอบสำหรับการพัฒนาที่สำคัญสามารถพบได้ภายใต้คีย์ DOCs

ปัญหาและรายงานข้อผิดพลาด

• สำหรับรายงานข้อผิดพลาดโปรดใช้ตัวติดตามปัญหาหรือส่งอีเมลไปที่ [email protected]

• สำหรับการอภิปรายคุณอาจต้องการสมัครสมาชิกและใช้รายชื่อผู้รับจดหมาย [email protected] หรือใช้การอภิปราย GitHub

มีส่วนร่วมในคีย์

อย่าลังเลที่จะส่งคำขอดึงผ่าน GitHub การร้องขอแบบดึงจะได้รับการประเมินโดยใช้การทดสอบอัตโนมัติการจัดรูปแบบและตัวตรวจสอบแหล่งกำเนิดแบบคงที่รวมถึงการตรวจสอบด้วยตนเองโดยหนึ่งในนักพัฒนา แนวทางเพิ่มเติมและเอกสารประกอบสำหรับการพัฒนาที่สำคัญสามารถพบได้ภายใต้คีย์ 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.