การตรวจสอบอย่างเป็นทางการและผู้ช่วยพิสูจน์

การตรวจสอบอย่างเป็นทางการเป็นการยืนยันว่าซอฟต์แวร์ตรงตามข้อกำหนด โดยใช้การพิสูจน์ทางคณิตศาสตร์ที่ตรวจสอบโดยเครื่องจักรได้; ผู้ช่วยพิสูจน์คือเครื่องมือที่สร้างและตรวจสอบการพิสูจน์ดังกล่าว

Definition

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

Scope

หัวข้อนี้ครอบคลุมการตรวจสอบแบบนิรนัยและการพิสูจน์ทฤษฎีเชิงโต้ตอบ: ผู้ช่วยพิสูจน์ที่อิงตามทฤษฎีประเภท (type theory) หรือตรรกะอันดับสูง (higher-order logic) (เช่น Coq, Isabelle, Lean และ Agda), แนวทาง LCF ในการพิสูจน์ที่น่าเชื่อถือ, พื้นฐานของข้อเสนอในฐานะประเภท (propositions-as-types), การทำให้การพิสูจน์เป็นอัตโนมัติและกลยุทธ์, และสิ่งประดิษฐ์ที่ได้รับการตรวจสอบที่เป็นจุดเด่น รวมถึงคอมไพเลอร์และเคอร์เนลของระบบปฏิบัติการ

Core questions

• จะพิสูจน์ความถูกต้องเชิงฟังก์ชันการทำงานได้อย่างสมบูรณ์และตรวจสอบด้วยเครื่องจักรได้อย่างไร?
• เหตุใดผู้ช่วยพิสูจน์จึงน่าเชื่อถือ และฐานการประมวลผลที่เชื่อถือได้คืออะไร?
• การติดต่อกันของ Curry-Howard เชื่อมโยงการพิสูจน์และโปรแกรมอย่างไร?
• ต้องทำอย่างไรจึงจะตรวจสอบระบบจริง เช่น คอมไพเลอร์และเคอร์เนลได้?

Key theories

แนวทาง LCF ในการพิสูจน์ที่น่าเชื่อถือ

Edinburgh LCF ของ Gordon, Milner และ Wadsworth ได้นำเสนอเคอร์เนลการพิสูจน์ขนาดเล็กที่เชื่อถือได้ ซึ่งทฤษฎีบททั้งหมดจะต้องผ่าน เพื่อให้แม้แต่การทำงานอัตโนมัติที่ซับซ้อนก็ไม่สามารถสร้างการพิสูจน์ที่ไม่ถูกต้องได้

คอมไพเลอร์ที่ได้รับการตรวจสอบ (CompCert)

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

เคอร์เนลระบบปฏิบัติการที่ได้รับการตรวจสอบ (seL4)

Klein และเพื่อนร่วมงานได้สร้างการพิสูจน์ความถูกต้องเชิงฟังก์ชันการทำงานที่ตรวจสอบโดยเครื่องจักรได้สำหรับไมโครเคอร์เนล seL4 ซึ่งแสดงให้เห็นถึงการตรวจสอบแบบครบวงจรของซอฟต์แวร์ระบบระดับต่ำ

Clinical relevance

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

History

การพิสูจน์ทฤษฎีเชิงโต้ตอบเริ่มต้นด้วย Edinburgh LCF ในทศวรรษ 1970 ซึ่งภาษาเมตา ML และเคอร์เนลที่เชื่อถือได้ได้กำหนดรูปแบบของระบบในภายหลัง ผู้ช่วยที่อิงตามทฤษฎีประเภท เช่น Coq และ Agda และระบบตรรกะอันดับสูง เช่น Isabelle/HOL ได้พัฒนาขึ้นในช่วงทศวรรษต่อมา ซึ่งนำไปสู่สิ่งประดิษฐ์ที่ได้รับการตรวจสอบที่เป็นจุดเด่น: คอมไพเลอร์ CompCert (2009) และเคอร์เนล seL4 (2009)

Debates

ต้นทุนของการตรวจสอบเทียบกับความมั่นใจที่ได้รับ

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

Key figures

• Robin Milner
• Michael Gordon
• Xavier Leroy
• Gerwin Klein
• Robert Harper

Seminal works

• gordon1979
• leroy2009
• klein2009
• harper2016

Frequently asked questions

ผู้ช่วยพิสูจน์คืออะไร?

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

การตรวจสอบโปรแกรมแตกต่างจากการทดสอบอย่างไร?

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