Dafny

Dafny on kompileeritud programmeerimiskeel, millesse on sisseehitatud staatiline programmitõendaja, mis kontrollib programmide funktsionaalset õigsust. Ta ühendab peamiselt kahte programmeerimise paradigmat (imperatiivset ja funktsionaalset stiili) ja sisaldab ka piiratult objektorienteeritud programmeerimise tuge. Funktsioonide hulka kuuluvad üldised klassid, induktiivandmete tüübid ja variatsioon eraldusloogikast, mida teatakse kaudselt dünaamilisete raamidena (implicit dynamic frames), et põhjendada kõrvalmõjusid .

Dafnyt kasutatakse laialdaselt õppimiseks ning lihtsa täpsustuse ja kontrollimise sissejuhatuse andmiseks. Ta põhineb automaatse teoreemi tõestamisel (automated theorem proving), et eemaldada tõestamiskohustused ehk vältida inimese sekkumist. Programmi kirjutades tõendab Dafny jooksvalt koodi ja märgib kõik vead. Dafny kasutab Boogie vahenduskeelt.

Ajalugu

Keele tegi Rustan Leino, kes töötab Microsoft Researchis. Enne Dafnyt arendas Leino välja ESC/Modula-3 ja ESC/Java tööriistad ja keele Spec#. Esimesena ilmus Dafny aastal 2009, stabiilne versioon aastal 2017.

Näited

Kõige lihtsam viis alustamiseks on kasutada rise4fun, kus ei pea midagi alla laadima ja saab Dafnyt koos õpetusega proovida. Kuigi Dafnyt saab jooksutada ka käsurealt, siis eelistatum viis on kasutada Microsoft Visual Studio 2010t, kus Dafny tõendaja jookseb taustal, samal ajal kui programmeerija muudab koodi.

Meetodid

Dafny meenutab tüüpilisi vajalikke programmeerimiskeeli paljudel viisidel. Dafny keeles on meetodid, muutujad, tüübid, tsüklid, tingimuslaused, massiivid, täisarvud ja muud. Üks tavalisemaid ühikuid igas Dafny programmis on meetod, mida teistes keeltes võidakse kutsuda protseduurideks või funktsioonideks. Meetodit kirjutatakse nii:

method Abs(x: int) returns (y: int)
{
   ...
}

Siin on näha, et meetodi nimi on Abs ja see võtab sisse ühe täisarvulise parameetri x-i ja tagastab ühe täisarvu y-i. Tüüpe on vaja kirjutada nii igale parameetrile kui ka tagastatavale väärtusele. Tüübid järgnevad igale nimele peale koolonit (:). Kui on mitu parameetrit või tagastatavat väärtust, siis neid eraldatakse komaga.

method MultipleReturns(x: int, y: int) returns (more: int, less: int)
{
   more := x + y;
   less := x - y;
   // comments: are not strictly necessary.
}

Meetodi kehaosa on loogeliste sulgude vahel. See koosneb väidete seeriast, näiteks tingimuslausetest, tsüklitest ja teiste meetodite kutsetest. Määramised ei kasuta mitte "=", vaid ":=" ja võrdusi näidatakse "==".  Lihtsa väite järel peab olema semikoolon (;) ning kahe kaldjoonega (//) märgitakse kommentaari.

Eel- ja posttingimused

Tõeliselt eriliseks muudab Dafny see, et tal on võimalus märkida meetodid nende käitumise järgi. Nendega saab Dafny kindlaks teha, et meetod teeb seda, mida peab. Kõige tavalisem viis märkida meetodit on eeltingimuste (requires) ja posttingimustega (ensures).

method MultipleReturns(x: int, y: int) returns (more: int, less: int)
   requires 0 < y
   ensures less < x < more
{
   more := x + y;
   less := x - y;
}

Siin on näha, miks tagastatavatele väärtustele antakse nimed, et nende poole oleks kerge meetodi posttingimustes ja eeltingimustes pöörduda. Eeltingimus kontrollib, et y ei oleks negatiivne ega null. Posttingimus kontrollib, et less oleks väiksem kui x ja x oleks väiksem kui more.

Väited

On veel üks versioon meetodi märkus – väide (assert). Erinevalt eel- ja posttiingimustest väide asetatakse kusagile meetodi keskele. Peale väite võtmesõna järgneb assert'ile tõeväärtus ja semikoolon.

method Testing()
{
   assert 2 < 3;
}

Dafny tagastab tõese väärtuse, kuna kaks on alati väiksem kolmest. Väitel on mitu kasutust, kuid peamine on kontrollida, et oodatav on tõesti tõene. Seda on hea kasutada ka eelmise meetodi tagastatava väärtuse kontrollimiseks.

// use definition of Abs() from before.
method Testing()
{
   var v := Abs(3);
   assert 0 <= v;
}