Generating libraries of highly correct and safe functions by using proof-based formal methods

Abstract

Bu tezde, büyük ölçekli yazılım oluşturabilmek için kullanılabilecek yüksek düzeyde doğruluğa sahip ve güvenilir fonksyonların formal tanımlarından oluşan bir kütüphane üretildi. Büyük programların doğruluğunu ve güvenliğini ispatlamak zor olmasına ragmen, eğer kendisinin bileşenlerinin doğruluğu ve/veya güvenliği önceden gösterilebilirse bu işlem yapılabilir. Benzer bir yaklaşım STL'nin pek çok kullanışlı küçük ölçekli prosedürler ve fonksiyonlar sağladığı C++'ta kullanılmaktadır. Yazılım doğruluğunu kontrol etmek için en güçlü yöntemlerden biri formal yöntemleri kullanmaktır. Bu araştırmada, programların özelliklerini yazmak ve onların tanımlanan özellikler açısından doğru ve güvenli olduğunu ispatlamak için Athena isimli bir teorem ispatlayıcı kullanılmıştır. Aksiyomatik tanımlar ve ispatlar prefix notasyonu ile karşılaştırıldığında daha okunabilir ve kısa ifadelerin yazılmasını sağlayan infix notasyonunda yapılmıştır. Athena'da CODEGEN adı verilen bir program, aksiyomlar ve teoremlerden kod üretmek için kullanılabilmektedir. Fakat bu program sadece prefix notasyonundaki tanımlarla çalışır. Onun infix notasyonlarla çalışmasını mümkün kılmak için aksiyomatik tanımları infix notasyonundan prefix notasyonuna dönüştüren bir program Java'da yazılmıştır. Son olarak bu tezde infix notasyonuyla bellek tanımı yapılmış ve böylelikle bellekte güncelleme yapan programların üretilmesi sağlanmıştır.

In this thesis, a specification library of highly correct and safe functions which can be used to compose large scale software is constructed. Although it is hard to prove the correctness and safety of large programs, it can be done if the correctness and/or safety of its components are shown beforehand. A similar approach is used in C++ where STL provides many useful small-scale procedures and functions. One of the strongest methods to verify software correctness is to use formal methods. In this research, Athena has been used as a theorem prover to write specifications of programs and prove that they are correct and safe with respect to the given specifications. The axiomatic definitions and the proofs are written in infix notation which makes them more readable and shorter with respect to the prefix notation. In Athena a program called CODEGEN can be used to extract code from the axioms and theorems. But it only works with the definitions in the prefix notation. In order to make it work with the infix definitions, a program that converts axiomatic definitions in infix notation to prefix notation is implemented in Java. The last contribution of this thesis is to define memory by using the infix notation to make it possible to generate code that updates memory locations.