Espezifikazio formala (informatika)

**Espezifikazio formala** matematikak eskaintzen duen lengoaia formala erabiliz, algoritmo baten zeregina dokumentatzean datza. Horretarako begizta edo egitura errekurtsiboen exekuzioen ondorioz lortutako emaitzen konputazio-egoerak lengoaia formalean zehazten dira, era horretan programak dokumentatzen dira. Dokumentazio horiek programen zeregina deskribatzean sarrerako datuen eta irteerako emaitzen arteko erlazioa adierazten dute.Espezifikazioa lehen mailako lengoaia logiko edo matematikoan idatzi ohi da, eguneroko hizkuntzek dituzten anbiguotasun eta zehaztasun gabeziak ekiditeko. Hala ere, espezifika daiteke lengoaia informalak diren eguneroko hizkuntzekin, aholkatzen ez den arren, horretarako oso ondo zehaztu behar baitira erabili beharreko terminoak, hizkuntzaren anbiguotasuna saihestuz.

## Espezifikazio formalaren premia 
Sistema elektronikoak darabiltzaten gailuak programatzeko orduan, oso garrantzitsua da algoritmoaren espezifikazioa burutzea. Programa ondo dokumentatuz gero, erroreak gertatzeko arriskuak murrizten dira, programaren exekuzio zuzena ezinbestekoa delako erabiltzailearentzako. Gainera, badaude exekuzio erroreak barkaezinak diren kasuak, adibidez: operazio militar edo kirurgikoak, finantza eta burtsa mundua...

## Algoritmoa espezifikatzearen abantailak 
Idatzitako kodea anbiguotasunik gabeko lengoaia batean dokumentatzean, sarrera, irteera eta zeregina zein diren zehazten da, erabilitako lengoaia dakien beste edozeinek kodeak zehazki zer egiten duen jakin dezan ahalbidetuz. Esaterako, software-ingeniari batek sarean zabal dezake garatutako kodea beste edozein pertsonarentzako eta erabiltzaileak espezifikazioa irakurrita jakin dezake programak zer egingo duen programa bera exekutatu gabe.

Bestalde, algoritmoaren egiaztapen formala burutzeko ezinbestekoak dira espezifikazio formalak, algoritmoaren konputazio-egoera batetik besterako pausuak frogatu ahal izateko, lehenik egoerak zeintzuk diren zehaztu behar baitira. Gainera, algoritmoaren espezifikazioa emanik, bere zuzentasuna inplementazioa baino lehen froga daiteke. Prozedura honek programak eduki ditzakeen erroreak aurkitzea ahalbidetzen du inplementazioari ekin baino lehen. Espezifikazioak ez du adierazten emaitza *nola* lortzen den, baizik eta *zein* den emaitza.
* Asertzio batetik aurrera erraz eraikitzeko ahalmena
* Akatsak erraz konpontzeko ahalmena
* Etorkizuneko aldaketei egokitzeko erraztasuna
* Erabilgarritasuna
* Algoritmoko bi asertzioen arteko erlazioa aurkitzeko erraztasuna (komunikagarritasuna)
* Eraginkortasuna

## Adibideak 
### 1. adibidea: 
Hurrengo adibidean, kode zati sinple baten espezifikazioa ageri da, esleipen batena. Aurrebaldintza,  \varphi -rekin adierazi ohi dena, *true* da, edozein kasutarako funtzionatuko duelako kode puxka honek. Postbaldintzak,  \psi -rekin adierazi ohi denak, lerro horren exekuzio ostean programaren egoera dokumentatzen du. Kasu honetan, **x**-ren balioa 5 izango da.

 \{ \varphi \} \equiv \{ \textstyle{\it{true}} \} 

 x := 5  

 \{ \psi \} \equiv \{ x = 5 \} 

### 2. adibidea: 
Oraingo honetan aldaketa mordoa daude lehenengo adibidearekiko. Alde batetik *while* blokea dugu, *while*-aren ostean datorren baldintza betetzen den bitartean behin eta berriz exekutatuko den algoritmo zatia adieraziz. Bestalde, algoritmoak ez du edozein egoeratan funtzionatuko nahi bezala, aurrebaldintza ez baita  \textstyle{true} . Horrez gain, **x** eta **y** parametroak dauzkagu. Honek esan nahi du emaitza **x** eta **y**-ren menpekoa izango dela. Aldagai hauek  \varphi  aurrebaldintzak mugatzen ditu eta exekuzioan esleitzen zaizkie balioak.

 \{ \varphi \} \equiv \{ x \geq 0 \land y > 0 \} 

 z := x  

 \textstyle{while} \left( z \geq  y  \right) \, \textstyle{loop}

 z := z - y 

 \textstyle{end} \, \, \textstyle{loop} 

 \{ \psi \} \equiv \{ z = x \% y \} 

non % modulu funtzioaren sinboloa den.

Adibide honek argi erakusten du zein den aurrebaldintza ez betetzearen arazo bat. Adibidez, **y** negatiboa edo **0** izanez gero, programa begizta infinitu batean sartuko litzateke, eta **x** negatiboa izanez gero, balio bera itzuliko luke, kasu gehienetan emaitza okerra izanik.

## Software bidezko espezifikazioa 
Gaur egun existitzen dira espezifikazioa burutzen edo garatzen laguntzen duten software-tresnak eta notazioak. Notazio erabilien artean daude Z notazioa, VDM notazioa eta TLA+ notazioa. Tresna erabilienen artean Dafny dago. Programa hau konpiladoreak bezala interprete moduan aritzen da eta kodearen zuzentasun funtzionala aztertzen du.

## Bibliografia 
* Javier Alvez Gimenez, Xabier Arregi Iparragirre, Jose Gaintzarain Ibarmia, Paqui Lucio Carrasco, Montse Maritxalar Anglada. *Programen espezifikazio, egiaztapen eta eratorpen formala*. Udako Euskal Unibertsitatea. 2016. ISBN:978-84-8438-590-5

## Erreferentziak 
## Ikus, gainera 
* Egiaztapen formala (informatika)
* Logika konputazional

## Kanpo estekak