Lankide:Igorermua10/Proba orria

Informatikan, bereziki software ingeniaritzan eta hardware ingeniaritzan, metodo formala software sistemen eta hardware sistemen egiaztapenerako, zehaztapenerako eta garapenerako teknika matematiko zehatzen multzoa da^[1].

Ingeniaritzan, analisi matematiko egoki bat erabiltzeak diseinuaren fidagarritasunarekin eta sendotasunarekin lagundu dezake, horregatik dira hain erabilgarriak metodo formalak^[2].

Historia[aldatu | aldatu iturburu kodea]

1967. urtean, Robert Floyd zientzialari informatikoak erdi mailako baieztapen metodoa garatu zuen. Metodoaren helburua programa informatikoen propietateak aztertzea da. Hori lortzeko, metodo honek operazio ezberdinen semantika seinu logikoen bidez definitzen zuen.

Ondoren, Tony Hoare zientzialari britaniarrak Floydek garaturiko metodoa perfekzionatu zuen metodo axiomatikoa sortu ahal izateko. Aldaketa handiena “inbariantzaren” kontzeptuaren agerpena izan zen.

Geroago, 1976an Edsger Dijkstra zientzialari informatikoak “prebaldintza aske ahulena” metodo formala aurkeztu zuen. Metodo honekin, Floyden eta Dijsktraren baieztapenak bateratzea eta perfekzionatzea lortu zuen holandarrak. Metodo formalaren ideia nagusia ariketa baten postbaldintzetatik abiaturik ariketaren prebaldintzak lortzea zen, Hoarek eta Floydek ezinezkotzat jo zutena hain zuzen ere^[3].

Metodo Formalen Abantailak[aldatu | aldatu iturburu kodea]

-Sistemaren ulerpen hobea lortzen da.

- Bezeroarekiko komunikazioan bereziki lagungarria gertatzen da, metodo formalei esker erabiltzailearen eskakizunen deskripzio argi bat lor daitekeelako.

-Sistema era zehatzagoan definitzen da.

-Ariketa jakin baten zehaztasunetarako sistema egokia dela matematikoki konprobatzeko aukera eskaintzen du.

-Programaren xehetasunak kontuan izanik kalitate handiagoko softwarea lortzen da .

-Produktibitatea handiagotzeko erabilgarria da^[3].

Metodo Formalen Desabantailak[aldatu | aldatu iturburu kodea]

-Metodo formalen aplikazioa bermatzen duten erreminten garapena oso konplexua da eta horretaz gain, metodoa erabiliz lortzen diren programak ez dira erosoak ezta erabilterrazak erabiltzaileentzat.

-Inbestitzaileek oro har ez dute errealitate industriala ezagutzen.

-Industriaren eta mundu akademikoaren arteko kolaborazioa eskasa da.

-Metodo formalen erabilpenak produktu bat garatzeko orduan prozesu osoa moteldu eta honen kostu finala garestitu egiten du^[3].

Baieztapen metodoak[aldatu | aldatu iturburu kodea]

Baieztapen metodo erabilienen artean hurrengoak daude:

E/S baieztapenak[aldatu | aldatu iturburu kodea]

Tony Hoarek garaturiko metodoaren logika erabiltzen duen programa jakin baten sartzen diren datuak programaren aurrebaldintzak betetzen badituzte, irteerako datuek postbaldintzak ere beteko dituzte^[3].

Prebaldintza aske ahulena[aldatu | aldatu iturburu kodea]

Programa baten postbaldintza izanik eta atzerantz operatuz programa horren prebaldintzak lortuko direla dio prebaldintza aske ahulenaren baieztapenak^[3].

Indukzio estrukturala[aldatu | aldatu iturburu kodea]

Indukzio matematikoan oinarrituriko baieztapen teknika honen arabera, S propietate jakin batzuk eta propietate horiekin frogatu nahi den P proposizioa izanik :

-S metodoen kasu tribialentzat P proposizioa betetzen dela frogatzen du^[3].

-Onartzen du P betetzen dela N baino txikiagoa edo berdina den Sren elementu kopuruarentzat^[3].

-Frogatzen du Sren N+1 elementuarentzat P proposizioa betetzen dela^[3].