Dafny
Dafny C# lengoaiara bideratuta dagoen eta aurrebaldintzen, postbaldintzen, begizta-inbarianteen eta borne-funtzioen bidez espezifikazio formala bermatzen duen programazio lengoaia konpilatu inperatiboa da. Lengoaiak nagusiki paradigma funtzional eta inperatiboen ideiak konbinatzen ditu, eta objektuetara bideratutako programaziorako euskarri mugatu bat eskaintzen du. Lengoaiaren ezaugarrien artean hauek dira aipagarrienak: klase generikoak, esleipen dinamikoa, datu-mota induktiboak eta banaketa-logikaren aldakuntza bat, alboko efektuekin arrazoitzeko[1] balio duen eta marko dinamikoki inplizituak[2] izena duena. Dafny lengoaia Rustan Leinok sortu zuen Microsoft Research-en ESC/Modula-3, ESC/Java eta Spec#-en garapenean lan egin ondoren. Dafny irakaskuntzan oso erabilia da eta softwarearen egiaztapeneko txapelketetan maiz agertzen da (adb. VSTTE'08[3], VSCOMP'10[4], COST'11[5] eta VerifyThis'12[6]).
Dafny | |
---|---|
![]() | |
Paradigma | inperatiboa, funtzionala |
Diseinatzailea | K. Rustan M. Leino |
Garatzailea | Microsoft Research |
Agerpena | 2009 |
Kaleratze Egonkorra | 2.0.0 (2007-09-23) |
Lizentzia | MIT License |
Webgunea | http://research.microsoft.com/dafny |
Dafny espezifikazio formalerako eta egiaztapenerako sarrera erraz bat eskaintzeko diseinatu zen. Dafny-k aurretik sortutako hainbat erremintaren ildoari jarraitzen dio, erreminta horien artean SPARK/Ada, ESC/Java, Spec#, Whiley, Why3[7] eta Frama-C daude. Erreminta horiek teoremen frogapen automatikoaren menpe daude frogapenak egin ahal izateko, adibidez, giza parte-hartze handiagoa behar duten mota dependenteetan onarritutakoak (adb. Idris, Agda). Dafny-n idatzitako programak konpilatzeko Boogie lengoaia bitartekaria erabiltzen da, Z3 teoremen frogatzaile automatikoa[8] erabiltzen duena.
Datu-motak
aldatuDafny-k albo ondorioak izan ditzaketen inplementazioetarako metodoak eta zehaztapenetan erabiltzeko funtzio puruak eskaintzen ditu. Metodoak while estilo inperatibo ezaguna jarraitzen duten sententzietaz osatuta daude, eta, funtzio baten gorputza, aldiz, adierazpen bat besterik ez da. Metodo batean albo-ondorioak dituen edozein sententzia (adb. array parametroko elementu bat esleitzea) kontuan hartu behar da modifies
klausulan alda daitezkeen parametroak adieraziz. Dafny-k, halaber, bilduma aldaezin mota batzuk eskaintzen ditu. Horien artean segidak (adb. seq<int>
), multzoak (adb. set<int>
) eta mapak (map<int,int>
). Horrez gain, array aldagarriak ere eskaintzen dira (adb. array<int>
).
Ezaugarri inperatiboak
aldatuDafny-k Hoare-ren logikaren ideietan oinarritutako programa inperatiboen probak onartzen ditu. Hurrengo kode-zatiak Dafny-ren hainbat ezaugarri erakusten ditu, besteak beste, aurrebaldintzen, postbaldintzen, begizten inbarianteen eta begizten borne-adierazpenen erabilera.
method max(arr:array<int>) returns(max:int)
// Array-ak gutxienez elementu bat eduki behar du
requires arr!=null && arr.Length > 0;
// Return ezin da array-ko edozein elementu baino txikiagoa izan
ensures (forall j :int :: (j >= 0 && j < arr.Length ==> max >= arr[j]));
// Return-ek array-ko elementu baten balio bera eduki behar du
ensures (exists j : int :: j>=0 && j < arr.Length && max==arr[j]);
{
max:=arr[0];
var i:int :=1;
//
while(i < arr.Length)
// Gehienez arr.Length-era iritsi (begizta amaitzean i==arr.Length erakusteko behar da)
invariant (i<=arr.Length);
// Oraingoz max baino handiagoa den elementurik ez da topatu
invariant (forall j:int :: j>=0 && j<i ==> max >= arr[j]);
// Oraingoz ikusitako elementu bat max baino handiagoa da
invariant (exists j:int :: j>=0 && j<i && max == arr[j]);
// i == arr.Length denean amaitu
decreases (arr.Length-i);
{
// Elementu handiago bat topatu ezkero max eguneratu
if(arr[i] > max){max := arr[i];}
// Array-ko hurrengo elementura igaro
i := i + 1;
}
}
Adibide honek array bateko elementu handiena lortzen du. Metodo honen aurrebaldintza eta postbaldintza requires
eta ensures
klausulekin ematen dira hurrenez hurren. Era berean, begiztaren inbariantea eta borne-adierazpena invariant
eta decreases
klausulekin ematen dira hurrenez hurren.
Begizten inbarianteak
aldatuDafny-n begizten inbarianteen tratamendua Hoare-ren logika tradizionalarekiko desberdina da. Begizta batean eraldatutako aldagaiak tratatzeko modua dela eta, begizta baino lehen aldagaiari buruz ezagututako informazio gehiena baztertu egiten da. Aldagai horien propietateak frogatzeko behar den informazioa esplizituki adierazi behar da begiztaren inbariantean. Aitzitik, begiztan aldatzen ez diren aldagaiek aldez aurretik zuten informazio guztia mantentzen da. Honako kode zati honetan argi ikus daiteke:
method batuAndZero(ns:array<int>) returns (batu:nat)
requires ns != null
requires forall i :: 0 <= i < ns.Length ==> ns[i] >= 0
modifies ns
{
var i:int := 0;
var arr:array<int> := ns; // parametroak ezin direlako esleitu
batu := 0;
//
while(i < arr.Length) {
batu := batu + arr[i];
arr[i] := arr[i];
i := i + 1;
}
}
Kode honek egiaztapenean huts egiten du Dafny-k ezin baitu (batu + arr[i]) >= 0
esleipenean mantentzen dela ezarri. Aurrebaldintzatik, intuizioz, forall i :: 0 <= i < arr.Length ==> arr[i] >= 0
mantentzen da begiztan arr[i] := arr[i];
NOP bat delako. Hala ere, esleipen horrek Dafny-k arr
aldagai aldagarri bat bezala tratatzea eta, ondorioz, hari buruz begiztaren aurretik zuen informazioa baztertzea eragiten du. Programa hori Dafny-n egiaztatzeko, arr[i] := arr[i];
esleipen erredundantea kendu edo invariant forall i :: 0 <= i < arr.Length ==> arr[i] >= 0
buklearen inbariantea gehitu dezakegu.
Dafny-k, halaber, analisi estatiko mugatua erabiltzen du begizta sinpleen inbarianteak inferitzeko, ahal denean. Aurreko adibidean, invariant i >= 0
begiztaren inbariantea ere beharrezkoa dela dirudi i
aldagaia begiztaren barruan aldatzen delako. Barne-logikak inbariante hori behar duen arren, Dafny-k automatikoki inferitzen du eta, beraz, kode-mailan ez da jarri beharrik.
Proba ezaugarriak
aldatuDafny-k egiaztapen-laguntzaile gisa erabiltzeko bultzatzen duten ezaugarriak ditu. function
edo method
baten barruko propietate sinpleen frogapenak (lehen azaldu dugun bezala) ohikoak dira horrelako tresnentzat eta, horrez gain, Dafny-k function
baten eta bestearen arteko propietateen frogapena ere onartzen du. Frogarako laguntzaile batentzat ohikoa den bezala, frogapen horiek induktiboak izaten dira askotan. Hipotesi induktiboak aplikatzeko mekanismo gisa metodoen aipamena erabiltzeak, agian, Dafny ez-ohikoa izatea eragiten du. Hona hemen horren adibide bat:
datatype List = Nil | Link(data:int,next:List)
function batu(l:List): int {
match l
case Nil => 0
case Link(d,n) => d + batu(n)
}
predicate isNatList(l:List) {
match l
case Nil => true
case Link(d,n) => d >= 0 && isNatList(n)
}
ghost method NatBatuLemma(l:List, n:int)
requires isNatList(l) && n == batu(l)
ensures n >= 0
{
match l
case Nil =>
// Automatikoki burutua
case Link(data,next) => {
// Hipotesi induktiboa aplikatu
NatBatuLemma(next,batu(next));
// Dafny-k dakiena aztertu
assert data >= 0;
}
}
}
Hemen, NatBatuLemma-k
batu
() eta isNatList()-en
arteko propietate erabilgarri bat frogatzen du ( isNatList(l) ==> (batu(l) >= 0)
dela, alegia). Lemak eta teoremak kodetzeko ghost method
bat erabiltzea da era estandarra, Dafny-n, indukziorako errekurtsioa erabiliz (gehienetan, indukzio estrukturala). Kasuen azterketa match
sententziak erabiliz egin ohi da eta kasu ez-induktiboak gehienetan automatikoki burutzen dira. Egiaztatzaileak, behar denean, function
edo predicate
baten edukietarako sarbide osoa izan behar du. Horrek ondorioak izaten ditu sarbide-aldagailuekin batera erabiltzen denean. Zehazki, function
baten edukiak protected
aldatzailea erabiliz ezkutatzeak haren zein propietate ezar daitezken muga dezake.
Erreferentziak
aldatu- ↑ Leino, K. Rustan M.. (2010). Clarke, Edmund M. ed. «Dafny: An Automatic Program Verifier for Functional Correctness» Logic for Programming, Artificial Intelligence, and Reasoning (Springer Berlin Heidelberg) 6355: 348–370. doi: . ISBN 978-3-642-17510-7. (Noiz kontsultatua: 2020-03-31).
- ↑ Smans, Jan; Jacobs, Bart; Piessens, Frank. (2009). Drossopoulou, Sophia ed. «Implicit Dynamic Frames: Combining Dynamic Frames and Separation Logic» ECOOP 2009 – Object-Oriented Programming (Springer Berlin Heidelberg) 5653: 148–172. doi: . ISBN 978-3-642-03012-3. (Noiz kontsultatua: 2020-03-31).
- ↑ Leino, K. Rustan M.; Monahan, Rosemary. (2010). Leavens, Gary T. ed. «Dafny Meets the Verification Benchmarks Challenge» Verified Software: Theories, Tools, Experiments (Springer Berlin Heidelberg) 6217: 112–126. doi: . ISBN 978-3-642-15056-2. (Noiz kontsultatua: 2020-03-31).
- ↑ Klebanov, Vladimir; Müller, Peter; Shankar, Natarajan; Leavens, Gary T.; Wüstholz, Valentin; Alkassar, Eyad; Arthan, Rob; Bronish, Derek et al.. (2011). Butler, Michael ed. «The 1st Verified Software Competition: Experience Report» FM 2011: Formal Methods (Springer Berlin Heidelberg) 6664: 154–168. doi: . ISBN 978-3-642-21436-3. (Noiz kontsultatua: 2020-03-31).
- ↑ Bormer, Thorsten; Brockschmidt, Marc; Distefano, Dino; Ernst, Gidon; Filliâtre, Jean-Christophe; Grigore, Radu; Huisman, Marieke; Klebanov, Vladimir et al.. (2012). Beckert, Bernhard ed. «The COST IC0701 Verification Competition 2011» Formal Verification of Object-Oriented Software (Springer Berlin Heidelberg) 7421: 3–21. doi: . ISBN 978-3-642-31761-3. (Noiz kontsultatua: 2020-03-31).
- ↑ (Ingelesez) Huisman, Marieke; Klebanov, Vladimir; Monahan, Rosemary. (2015-11). «VerifyThis 2012: A Program Verification Competition» International Journal on Software Tools for Technology Transfer 17 (6): 647–657. doi: . ISSN 1433-2779. (Noiz kontsultatua: 2020-03-31).
- ↑ «Why3» why3.lri.fr (Noiz kontsultatua: 2020-03-31).
- ↑ de Moura, Leonardo; Bjørner, Nikolaj. (2008). Ramakrishnan, C. R. ed. «Z3: An Efficient SMT Solver» Tools and Algorithms for the Construction and Analysis of Systems (Springer Berlin Heidelberg) 4963: 337–340. doi: . ISBN 978-3-540-78799-0. (Noiz kontsultatua: 2020-03-31).