sturdy

ความทนทานเวอร์ชัน Haskell ไม่ได้รับการดูแลอีกต่อไป โครงการที่ทนทานได้รับการปรับปรุงใหม่ใน Scala และมีให้ที่ https://gitlab.rlp.net/plmz/sturdy.scala

แข็งแรง

Sturdy เป็นห้องสมุดเพื่อสร้างการวิเคราะห์แบบคงที่ใน Haskell การวิเคราะห์แบบคงที่เป็นเครื่องมือที่สร้างข้อมูลเกี่ยวกับโปรแกรมคอมพิวเตอร์โดยไม่ต้องใช้โปรแกรม ตัวอย่างของการวิเคราะห์แบบคงที่คือหมากฮอสประเภทตัวค้นหาข้อผิดพลาด (เช่น Java findbugs) การวิเคราะห์ความปลอดภัย (เช่นการวิเคราะห์ taint) และการวิเคราะห์ที่ใช้สำหรับการเพิ่มประสิทธิภาพคอมไพเลอร์

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

มีความทนทานต่อตัวประกอบล่ามและล่ามบทคัดย่อ (การวิเคราะห์แบบคงที่) ลงใน ล่ามทั่วไป ล่ามทั่วไปนี้ได้รับการกำหนดพารามิเตอร์โดยอินเทอร์เฟซที่มีการดำเนินการดั้งเดิมที่อธิบายความหมายของภาษาเช่น try catch และ finally ก็มีข้อยกเว้น ล่ามคอนกรีตและบทคัดย่อจากนั้นสร้างอินสแตนซ์ล่ามทั่วไปโดยใช้อินเทอร์เฟซเหล่านี้ การปรับโครงสร้างองค์กรนี้ไม่เพียง แต่แยกข้อกังวลที่แตกต่างกันในการดำเนินการวิเคราะห์แบบคงที่ แต่ยังทำให้การพิสูจน์ความสมบูรณ์ง่ายขึ้น รายละเอียดเพิ่มเติมสามารถพบได้ในกระดาษ ICFP ของเรา

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

เริ่มต้น

ในการสร้างให้ติดตั้งเครื่องมือสร้างสแต็กและเรียกใช้ stack build จากไดเรกทอรีรากของโครงการ

ปัจจุบันโครงการที่ทนทานมีล่ามคอนกรีตและนามธรรมและล่ามทั่วไปสำหรับภาษาต่อไปนี้:

• PCF เป็นภาษาการทำงานที่มีลำดับสูงกว่า
• ในขณะที่ ภาษาที่จำเป็นด้วยเงื่อนไขและในขณะที่ลูป
• Scheme ภาษาที่ใช้งานได้ในตระกูล Lisp
• Stratego ภาษาสำหรับการแปลงโปรแกรม
• Lambdajs การเป็นตัวแทนระดับกลางสำหรับ JavaScript
• Jimple , Java bytecode ที่เหมาะสำหรับการวิเคราะห์แบบคงที่ (ทำงานอยู่ระหว่างดำเนินการ)

ในการเรียกใช้การทดสอบของภาษาเฉพาะให้ใช้ stack test sturdy-$(lang) เช่น

 stack test sturdy-pcf

สิ่งพิมพ์

อัลกอริทึม FixPoint ที่ใช้ Combinator สำหรับล่ามบทคัดย่อขนาดใหญ่
Sven Keidel, Sebastian Erdweg, Tobias Hombücher
การประชุมนานาชาติเกี่ยวกับการเขียนโปรแกรมการทำงาน (ICFP) ACM, 2023. [PDF]

สื่อล่ามที่เป็นนามธรรมแบบแยกส่วนสำหรับ webAssembly
Katharina Brandl, Sebastian Erdweg, Sven Keidel, Nils Hansen
การประชุมยุโรปเกี่ยวกับการเขียนโปรแกรมเชิงวัตถุ (ECOOP) ACM, 2023. [PDF]

วิธีการที่เป็นระบบในการตีความนามธรรมของการแปลงโปรแกรม
Sven Keidel และ Sebastian Erdweg
การตรวจสอบการตรวจสอบแบบจำลองและการตีความนามธรรม (VMCAI) Springer, 2020. [PDF]

ส่วนประกอบที่ดีและนำกลับมาใช้ใหม่สำหรับการตีความนามธรรม
Sven Keidel และ Sebastian Erdweg
การเขียนโปรแกรมเชิงวัตถุระบบภาษาและแอปพลิเคชัน (OOPSLA) ACM, 2019 [PDF] [พูดคุย]

การพิสูจน์ความสมบูรณ์แบบองค์ประกอบของล่ามนามธรรม
Sven Keidel, Casper Bach Poulsen และ Sebastian Erdweg
การประชุมนานาชาติเกี่ยวกับการเขียนโปรแกรมการทำงาน (ICFP) ACM, 2018 [PDF] [พูดคุย]

กิตติกรรมประกาศ

โครงการที่แข็งแรงเป็นความพยายามร่วมกันของคนต่อไปนี้ (ตามลำดับตัวอักษร):

Casper Bach Poulsen, Jente Hidskes, Matthijs Bijman, Sarah Müller, Sebastian Erdweg, Sven Keidel, Tobias Hombücher, Wouter Raateland