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 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&#x3C;int&#x3E;`), multzoak (adb. `set&#x3C;int&#x3E;`) eta mapak (`map&#x3C;int,int&#x3E;`). Horrez gain, array *aldagarriak ere eskaintzen dira* (adb. `array&#x3C;int&#x3E;`).

## 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.
```java
method max(arr:array) 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  max >= arr[j]));
 // Return-ek array-ko elementu baten balio bera eduki behar du
 ensures (exists j : int :: j>=0 && j =0 && j max >= arr[j]);
  // Oraingoz ikusitako elementu bat max baino handiagoa da
  invariant (exists j:int :: j>=0 && j 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:

```java
method batuAndZero(ns:array) returns (batu:nat)
  requires ns != null
  requires forall i :: 0  ns[i] >= 0
  modifies ns 
{
  var i:int := 0;
  var arr:array := ns; // parametroak ezin direlako esleitu
  batu := 0;
  //
  while(i = 0` esleipenean mantentzen dela ezarri. Aurrebaldintzatik, intuizioz, `` mantentzen da begiztan `` 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, `` esleipen erredundantea kendu edo `` 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:

```java
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 
## Kanpo estekak