Biçimsel Doğrulama ve Kanıt Asistanları
Biçimsel doğrulama, yazılımın kendi spesifikasyonunu karşıladığını makine tarafından kontrol edilmiş matematiksel kanıtlarla ortaya koymaktadır; kanıt asistanları ise bu tür kanıtları oluşturan ve kontrol eden araçlardır.
Tanım
Biçimsel doğrulama, bir sistemin biçimsel bir spesifikasyonu karşıladığına dair titiz, makine tarafından kontrol edilmiş bir kanıtın oluşturulmasıdır ve kanıt asistanı, bir kullanıcının bu tür kanıtları geliştirmesine yardımcı olan ve geçerliliklerini mekanik olarak kontrol eden bir yazılımdır.
Kapsam
Bu konu, tümdengelimsel doğrulamayı ve etkileşimli teorem kanıtlamayı kapsamaktadır: tip teorisi veya yüksek dereceli mantığa dayalı kanıt asistanları (Coq, Isabelle, Lean ve Agda gibi), güvenilir kanıta yönelik LCF yaklaşımı, önermeler-tip olarak temeli, kanıt otomasyonu ve taktikleri ile derleyiciler ve işletim sistemi çekirdekleri dahil olmak üzere dönüm noktası niteliğindeki doğrulanmış yapıtlar incelenmektedir.
Temel sorular
- Tam işlevsel doğruluk nasıl kanıtlanabilir ve makine tarafından kontrol edilebilir?
- Kanıt asistanları neden güvenilirdir ve güvenilir bilgi işlem tabanı nedir?
- Curry-Howard yazışması kanıtları ve programları nasıl birbirine bağlar?
- Derleyiciler ve çekirdekler gibi gerçek sistemleri doğrulamak için neler gerekmektedir?
Temel kuramlar
- Güvenilir kanıta yönelik LCF yaklaşımı
- Gordon, Milner ve Wadsworth'un Edinburgh LCF'si, tüm teoremlerin geçmesi gereken küçük, güvenilir bir kanıt çekirdeği sunmuştur, böylece karmaşık otomasyon bile hatalı kanıtlar üretememektedir.
- Doğrulanmış derleyici (CompCert)
- Leroy'un CompCert'i, üretilen kodun kaynak programın semantiğini iyileştirdiğine dair makine tarafından kontrol edilmiş bir teoremle, bir kanıt asistanında doğruluğu kanıtlanmış bir C derleyicisidir.
- Doğrulanmış işletim sistemi çekirdeği (seL4)
- Klein ve meslektaşları, seL4 mikro çekirdeği için işlevsel doğruluğun makine tarafından kontrol edilmiş bir kanıtını üretmiş, düşük seviyeli sistem yazılımlarının uçtan uca doğrulanmasını göstermişlerdir.
Klinik önem
Mekanize doğrulama, kritik yazılımlar için mevcut en yüksek güvenceyi sağlamakta, test tabanlı güven yerine kanıtlanmış garantilere sahip derleyiciler, çekirdekler ve kriptografik kütüphaneler üretmektedir. Kanıt asistanları ayrıca matematiğin kendisini biçimselleştirmek için de giderek daha fazla kullanılmaktadır.
Tarihçe
Etkileşimli teorem kanıtlama, 1970'lerde Edinburgh LCF ile başlamış olup, ML meta dili ve güvenilir çekirdeği sonraki sistemleri şekillendirmiştir. Coq ve Agda gibi tip teorisi tabanlı asistanlar ve Isabelle/HOL gibi yüksek dereceli mantık sistemleri sonraki on yıllarda olgunlaşmış ve CompCert derleyicisi (2009) ile seL4 çekirdeği (2009) gibi dönüm noktası niteliğindeki doğrulanmış yapıtlarla sonuçlanmıştır.
Tartışmalar
- Doğrulama maliyeti ile elde edilen güvence
- Büyük sistemlerin makine tarafından kontrol edilmiş kanıtlarını oluşturmak muazzam bir çaba gerektirmekte, bu da tam doğrulamanın nerede haklı olduğu, daha hafif yöntemlerin nerede yeterli olduğu ve ne kadar kanıtın otomatikleştirilebileceği konusunda tartışmalara yol açmaktadır.
Öne çıkan isimler
- Robin Milner
- Michael Gordon
- Xavier Leroy
- Gerwin Klein
- Robert Harper
İlgili konular
Temel eserler
- gordon1979
- leroy2009
- klein2009
- harper2016
Sıkça sorulan sorular
- Kanıt asistanı nedir?
- Kanıt asistanı, bir kullanıcının biçimsel kanıtları etkileşimli olarak oluşturduğu, sistemin ise her adımı mekanik olarak kontrol ettiği bir yazılımdır; böylece tamamlanmış bir kanıt, küçük, iyi incelenmiş bir çekirdeğe kadar güvenilirdir.
- Bir programı doğrulamak, onu test etmekten nasıl farklıdır?
- Test etme, seçilen girdilerdeki davranışı kontrol eder ve yalnızca hataların varlığını ortaya çıkarabilirken, biçimsel doğrulama, spesifikasyonun izin verdiği tüm girdiler için doğruluğu kanıtlar ve belirtilen hataların yokluğunu tesis eder.