Wikiproiektu:EHU-Wikipedia 2017/Probalekua/Proba orria1

Espezifikazio formala matematikak eskeintzen duen lengoaia formala erabiliz, algoritmo baten exekuzioa dokumentatzean datza. Dokumentazio honek programa deskribatzeaz gain, analizatu egiten du, sarrerako datuen eta irteerako emaitzen arteko erlazioa adieraziz .

Asertzioak

Algoritmoaren azterketa lerroz lerro burutzen da, lerroaren aurreko eta ondorengo egoera dokumentatuz asertzioak erabiliz. Asertzioak algoritmoko egoera batean aldagaien zein espresio betetzen duten adieratzen dute. 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 adieratzen du. Besteei tarteko asertzioak deritze.

Ezaugarriak

Espezifikazio zuzen bat egokia, anbiguotasun gabea, osoa eta ahal denik eta laburrena izan behar da. Horrez gain, honako ezaugarri hauek espezifikazioa trinkotzen dute:

• Asertzio batetik aurrera erraz eraikitzeko ahalmena
• Akatsak erraz konpontzeko ahalmena
• Etorkizuneko aldaketei egokitzeko erraztasuna
• Erabilgarritasuna
• Algoritmoko bi asertzioen arteko erlazioa aurkitzeko erraztazuna (komunikagarritasuna)
• Eraginkortasuna

Erabilpenak

Algoritmoaren espezifikazioa emanik, bere zuzentasuna froga daiteke inplementazioa baino lehen. Prozedura honek programaren arazoak aurkitzea ahalbidetzen du inplementazioan inbertitu gabe. Kontuan hartu behar da espezifikazioak ez dakarrela kodearen inplementazioa, inplementazioaren garapenean laguntzen duela baizik, ez baitu adierazten nola egin, baizik eta zer egin.

Adibideak

Hurrengo adibidean, kode 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\}$