Dafny Nedir:
Dafny hatasız kod yazmayı kolaylaştırmak için tasarlanmıştır. Java gibi birçok programlama dilinde uygulamada bir çok hata içermesine rağmen syntax hatası olmadığından uygulamayı başarıyla compile edebiliyoruz. Uygulamayı çalıştırdığımızda ise index out of bounds, null dereferences, division by zero, infinite gibi bir çok runtime hata ile ve istenmediği halde infinite loop gibi mantıksal bazı hatalar ile karşılaşıyoruz işte Dafny programlama dili bu sorunun çözülebilmesi amacıyla geliştirilmiştir.
Dafny aynı zamanda programcının yapmak istediği şeyi doğrular,programcı fonksiyonun nasıl bir sonuç beklendiği belirtilerek dafny nin bu fonksiyon için doğrulama yapmasını sağlar.
Bu ek bilgileri sağlayarak geliştirilen yazılım çalışma anında hata vermez ve hatasız kod yazılabilmesini sağlar.
Dafny Github’da Microsoft mühendisleri tarafından açık kaynak kodlu geliştirilen bir programlama dilidir.
Henüz çok yeni bir dil olduğu için kaynak ve topluluk çok kısıtlı ve ve karşılaşılan sorunlara çözüm bulmak çok zor olabiliyor, Stackoverflow’a açtığım bir soruya ise maalesef kimseden cevap gelmedi.
Diğer bir dezavantajı ise programlama dilinin hedefi runtime error ile karşılaşmamak olduğundan programlama dili dışarıdan input alamıyor.
Girilen input’un eğer bir hata var ise hatasını runtime (çalışma zamanında) handle etmek zorunda olduğumuzdan programa diline girdileri dummy (statik) bir şekilde veriyoruz.
Bu programlama dilinde exception olmadığından tabiki hataya olanak verebilecek disk I/O yada network gibi işlemlerini de gerçekleştiremiyoruz.
Programlama yaparken önemli olan akış şemasını düzgün planlamak ve neleri kontrol etmemiz gerektiğini bilmek. Bu kontrolleri Dafny dilinin verifier’ı nasıl doğruluyorsa bizim için ,programcılar olarak bizim de yazdığımız kodu kafamızda Dafny gibi doğrulayıp sağlam temeller üzerine oturtarak yazmamız gerekiyor. Aksi taktirde program benim bilgisayarımda çalışıyordu seninkinde neden çalışmıyor? sorusuyla karşı karşıya kalabiliriz.
Şimdi Dafny ile programlamaya giriş yapalım.
Genel:
Atama işlemi için kullanılan işaret: :=
Koşullarda eşitlik için: == kullanılır
Tüm whitespace ve yorumlar ( // ve /**/ ) görmezden gelinir.
if koşulunda tek ifade olsa bile süslü parantez { } zorunludur.
Lokal değişken ataması var x: int := 5;
Değiştirmek için var x := 5;
Çoklu değişken atama var x, y, z: bool := 1, 2, true;
Ön Koşul (requires) ve Bitiş Koşulları (ensures):
Bitiş koşulu ensures kelimesiyle bildirilir. Bitiş koşulu ile metot bittiğinde hangi koşulun sağlanacağını bildirir ve garanti ederiz.
Örnekler:
ensures 0 <= y ensures 0 <= x ==> x == y //x pozitif ise x=y olmalıdır
Ön koşullar ise requires kelimesiyle bildirilir. Bu şekilde metoda gelen parametrelerin istenilen koşula uygun olup olmadığı kontrol edilebilir.
İddialar (Assertions)
assert kelimesi ile bildirilir.
Örnek:
method Abs(x: int) returns (y: int)
ensures 0 <= y
{
if x < 0
{ return -x; }
else
{ return x; }
}
method Testing()
{
var v := Abs(3);
assert 0 <= v;
}
assert 0 <= v; yerine assert v == 3;
yazdığımızda her ne kadar doğru gibi görünse de dafny metodu çağırdığımızda içinde ne olduğunu önemsemediğinden ve hata verir.
Burada önemli olan v nin 0 dan büyük olmasıdır..
Diğer dikkat edilmesi gereken nokta ise burada assert 0 <= v;
kodu Abs metodunun bitiş koşulunu yani ensures 0 <= y den başka bir şey bilmiyor oluşudur. Yani metodun içinde abstract işlemi yapıldığını bilmemektedir.
Fonksiyonlar (Functions)
Sadece bir ifade (expression) içerebilir.
requires,decreases … içerebilir
Örnek:
function abs(x: int): int{
if x < 0 then -x else x
}
method Testing() {
assert abs(3) == 3;
}
Yine metodlardan faklı olarak bu şekilde kullanımda metodun içini unutmaz ve assert abs(3) == 3; koşulu sağlanır.
Fonksiyonlar compile olmuş programın bir parçası değillerdir sadece kodumuzu sağlamamıza yardımcı olurlar.
Fonksiyonlarda metodlardan farklı olarak bitiş koşulu olmasa bile assert kodu anlayabilmekte ve assert abs(-3) > 0; gibi bir koşulu onaylayabilmektedir.
Döngü Sabitleri (Loop Invariants)
invariant kelimesiyle bildirilir döngü index’inin aralığını doğrulamak için kullanılır.
decreases değişkenin her döngüde azalacağını belirtir.
Arrayler
Arrayler belirtilirken ensures kelimesiyle array’in dışına çıkılmayacağının garantisi verilir.
Yüklemler (Predicates)
predicate kelimesiyle belirtilir Her zaman boolean değer döndüren fonksiyonlardır.
sorted gibi bir predicate yazıldıktan sonra requires sorted(a) gibi bir ön koşul yazılabilir
Framing
Memory den okuma izni verir.
reads kelimesi ile erişilecek olan yer belirtilir.
Lemmas
2 farklı kod verify edilirken ve bu 2 kod birbirinin doğrulamasını gerektirdiği nadir durumlarda lemmalar kullanılabilir.
Yararlanılan ve okunması gereken kaynaklar:
Getting Started with Dafny: A Guide
Dafny Tutorial
Online Compiler
Download Compiler