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 balio duen eta marko dinamikoki inplizituak 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, VSCOMP'10, COST'11 eta VerifyThis'12).

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 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 erabiltzen duena.

Datu-motak

Dafny-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

Dafny-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

Dafny-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

Dafny-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.

Kanpo estekak

• Datuak: Q48989398