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.^[1]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.^[1]

Abantaila hauek gehien bat enpresetan hauteman daitezke, non softwarea sortzerakoan, programaren zuzentasuna frogatuz ez den galduko denborarik programaren "debugging"-a (arazketa) egiten, denbora eta, hortaz, dirua aurreztuz.

Asertzioak

Algoritmoaren espezifikazioa lerroz lerro burutzen da, lerroaren aurreko eta ondorengo egoera dokumentatuz. Horretarako asertzioak erabiltzen dira. Asertzioak lengoaia logiko baten bidez idatzitako espresioak dira eta espresio horiek beteko dituzten konputazio-egoeren multzoa finkatzen dute. Beste era batera esanda, algoritmoaren konputazio-egoera konkretu batean aldagaiek zein baldintza betetzen duten adierazten dute (ikus. 1. adibidea). Algoritmo osoaren lehen asertzioari, oraindik hasi baino lehenagoko egoera adierazten duenari, aurrebaldintza deitzen zaio, eta programak ondo funtzionatzeko baldintzak ezartzen ditu. Bukaerakoari, postbaldintza deritzo eta programaren emaitza adierazten du. Besteei tarteko asertzioak deritze.

Asertzioek, lengoaia logikoek bezala, sintaxia eta semantika dute. Espresioak idazteko aldagaiak (x, y, z, t...), konstanteak (a, b, c...), eta aldagai bakoitzari dagozkion funtzioak (+, −, <, ≠, ∧, ∨, besteak beste) erabiltzen dira, eta erabilitako semantika lengoaia logikoen semantika da.

Ezaugarriak

Espezifikazio zuzen bat egokia, anbiguotasun gabea, osotua eta ahalik eta laburrena izan behar da. Horrez gain, honako ezaugarri hauek bete behar dituzte espezifikazioek:^[2]

• 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, ${\displaystyle \varphi }$-rekin adierazi ohi dena, true da, edozein kasutarako funtzionatuko duelako kode puxka honek. Postbaldintzak, ${\displaystyle \psi }$-rekin adierazi ohi denak, lerro horren exekuzio ostean programaren egoera dokumentatzen du. Kasu honetan, x-ren balioa 5 izango da.

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

${\displaystyle x:=5}$

${\displaystyle \{\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 ${\displaystyle \textstyle {true}}$. Horrez gain, x eta y parametroak dauzkagu. Honek esan nahi du emaitza x eta y-ren menpekoa izango dela. Aldagai hauek ${\displaystyle \varphi }$ aurrebaldintzak mugatzen ditu eta exekuzioan esleitzen zaizkie balioak.

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

${\displaystyle z:=x}$

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

${\displaystyle z:=z-y}$

${\displaystyle \textstyle {end}\,\,\textstyle {loop}}$

${\displaystyle \{\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.^[3] 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^[1]

Erreferentziak

1. Programen espezifikazio, egiaztapen eta eratorpen formala. Udako Euskal Unibertsitatea 2016 ISBN 978-84-8438-590-5. PMC 974392192. (Noiz kontsultatua: 2020-07-05).
2. https://en.wikipedia.org/wiki/Formal_specification
3. (Ingelesez) «Dafny: A Language and Program Verifier for Functional Correctness» Microsoft Research (Noiz kontsultatua: 2020-07-05).

Ikus, gainera

• Egiaztapen formala (informatika)
• Logika konputazional

Kanpo estekak

• Datuak: Q1437424