formulog
1.0.0
TL; DR: เขียนโปรแกรมการวิเคราะห์โปรแกรม SMT (ผู้บริหารสัญลักษณ์, หมากฮอสประเภทการปรับแต่ง ฯลฯ ) ในภาษาที่มีลักษณะคล้ายดาต้าล็อกที่ดีที่สุด
Datalog ได้พิสูจน์แล้วว่าเป็นภาษาที่มีประโยชน์สำหรับการใช้การวิเคราะห์โปรแกรมที่หลากหลาย แต่การวิเคราะห์ที่ใช้การแก้ปัญหา SMT ไม่สามารถเขียนได้อย่างง่ายดายใน Datalog รุ่นดั้งเดิม สูตรกำหนดให้เติมเต็มช่องว่างนี้โดยการเพิ่ม Datalog ด้วยวิธีการสร้างและเหตุผลเกี่ยวกับสูตร SMT รวมถึงการเขียนโปรแกรมการทำงานลำดับแรกเพื่อให้ชีวิตง่ายขึ้น
ทำไมต้องเขียนการวิเคราะห์ตาม SMT ของคุณในสูตร?
สนใจ? สำหรับข้อมูลเพิ่มเติมตรวจสอบเอกสารสูตร (ยังมีอยู่ในไดเรกทอรี DOCS) รวมถึงเคล็ดลับในการเริ่มต้นและการอ้างอิงภาษา เพื่อให้เข้าใจถึงสิ่งที่เกี่ยวข้องกับการสร้างการวิเคราะห์แบบอิง SMT แบบไม่สำคัญในสูตรให้ตรวจสอบบทช่วยสอนของเราเกี่ยวกับการใช้ตัวตรวจสอบประเภทการปรับแต่งในสูตร
การมีส่วนร่วมในโครงการนี้ยินดีต้อนรับมากที่สุด! กรุณาเปิดปัญหา GitHub จากนั้นเชื่อมโยงคำขอดึงไป คำขอดึงจะต้องอยู่ในรูปแบบ Google Java ก่อนที่จะถูกรวมเข้าด้วยกัน หากต้องการฟอร์แมตรหัสของคุณให้เรียกใช้ mvn spotless:apply ; นอกจากนี้คุณยังสามารถตรวจสอบว่ารหัสของคุณเป็นไปตามที่สอดคล้อง (โดยไม่ต้องฟอร์แมตใหม่) โดยใช้ mvn spotless:check
สูตรถูกปล่อยออกมาภายใต้ใบอนุญาต Apache 2.0
โครงการนี้ใช้ห้องสมุดบุคคลที่สาม คุณสามารถสร้างรายการไลบรารีเหล่านี้และดาวน์โหลดใบอนุญาตที่เกี่ยวข้องด้วยคำสั่งนี้:
mvn license:download-licenses
เนื้อหาที่สร้างขึ้นสามารถพบได้ใน target/generated-resources/
