Kiểm định hình thức và Trợ lý chứng minh

Kiểm định hình thức thiết lập, bằng chứng minh toán học được máy tính kiểm tra, rằng phần mềm đáp ứng đặc tả của nó; trợ lý chứng minh là các công cụ xây dựng và kiểm tra các chứng minh đó.

Definition

Kiểm định hình thức là việc xây dựng một chứng minh chặt chẽ, được máy tính kiểm tra rằng một hệ thống thỏa mãn một đặc tả hình thức, và trợ lý chứng minh là phần mềm giúp người dùng phát triển các chứng minh đó và kiểm tra tính hợp lệ của chúng một cách cơ học.

Scope

Chủ đề này bao gồm kiểm định suy diễn và chứng minh định lý tương tác: các trợ lý chứng minh dựa trên lý thuyết kiểu hoặc logic bậc cao (như Coq, Isabelle, Lean và Agda), phương pháp LCF để chứng minh đáng tin cậy, nền tảng mệnh đề-như-kiểu, tự động hóa chứng minh và các chiến thuật, cũng như các tạo phẩm đã được kiểm định mang tính bước ngoặt bao gồm trình biên dịch và nhân hệ điều hành.

Core questions

• Làm thế nào để chứng minh và kiểm tra bằng máy tính tính đúng đắn chức năng đầy đủ?
• Tại sao các trợ lý chứng minh đáng tin cậy, và cơ sở tính toán đáng tin cậy là gì?
• Sự tương ứng Curry-Howard kết nối các chứng minh và chương trình như thế nào?
• Cần những gì để kiểm định các hệ thống thực tế như trình biên dịch và nhân?

Key theories

Phương pháp LCF để chứng minh đáng tin cậy

Edinburgh LCF của Gordon, Milner và Wadsworth đã giới thiệu một nhân chứng minh đáng tin cậy nhỏ mà tất cả các định lý phải đi qua, để ngay cả tự động hóa phức tạp cũng không thể tạo ra các chứng minh không hợp lệ.

Trình biên dịch đã được kiểm định (CompCert)

CompCert của Leroy là một trình biên dịch C được chứng minh là đúng trong một trợ lý chứng minh, với một định lý được máy tính kiểm tra rằng mã được tạo ra tinh chỉnh ngữ nghĩa của chương trình nguồn.

Nhân hệ điều hành đã được kiểm định (seL4)

Klein và các đồng nghiệp đã tạo ra một chứng minh được máy tính kiểm tra về tính đúng đắn chức năng cho vi nhân seL4, thể hiện việc kiểm định đầu cuối của phần mềm hệ thống cấp thấp.

Clinical relevance

Kiểm định cơ giới hóa mang lại sự đảm bảo cao nhất cho phần mềm quan trọng, tạo ra các trình biên dịch, nhân và thư viện mật mã với các đảm bảo đã được chứng minh thay vì sự tin cậy dựa trên thử nghiệm. Các trợ lý chứng minh cũng ngày càng được sử dụng để hình thức hóa chính toán học.

History

Chứng minh định lý tương tác bắt đầu với Edinburgh LCF vào những năm 1970, với siêu ngôn ngữ ML và nhân đáng tin cậy đã định hình các hệ thống sau này. Các trợ lý dựa trên lý thuyết kiểu như Coq và Agda và các hệ thống logic bậc cao như Isabelle/HOL đã trưởng thành trong những thập kỷ tiếp theo, đỉnh điểm là các tạo phẩm đã được kiểm định mang tính bước ngoặt: trình biên dịch CompCert (2009) và nhân seL4 (2009).

Debates

Chi phí kiểm định so với sự đảm bảo đạt được

Việc xây dựng các chứng minh được máy tính kiểm tra cho các hệ thống lớn đòi hỏi nỗ lực rất lớn, gây ra tranh luận về việc kiểm định đầy đủ được biện minh ở đâu so với nơi các phương pháp nhẹ hơn là đủ, và bao nhiêu chứng minh có thể được tự động hóa.

Key figures

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

Seminal works

• gordon1979
• leroy2009
• klein2009
• harper2016

Frequently asked questions

Trợ lý chứng minh là gì?

Trợ lý chứng minh là phần mềm trong đó người dùng xây dựng các chứng minh hình thức một cách tương tác trong khi hệ thống kiểm tra cơ học từng bước, để một chứng minh hoàn chỉnh đáng tin cậy đến một nhân nhỏ, được xem xét kỹ lưỡng.

Kiểm định một chương trình khác với việc kiểm thử nó như thế nào?

Kiểm thử kiểm tra hành vi trên các đầu vào được chọn và chỉ có thể tiết lộ sự hiện diện của lỗi, trong khi kiểm định hình thức chứng minh tính đúng đắn cho tất cả các đầu vào được phép bởi đặc tả, thiết lập sự vắng mặt của các lỗi được chỉ định.