Metodo formalak

Informatikan, bereziki software ingeniaritzan eta hardware ingeniaritzan, metodo formalak 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

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 zeinu 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 “aurrebaldintza 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 aurrebaldintzak lortzea zen, Hoarek eta Floydek ezinezkotzat jo zutena hain zuzen ere.

Metodo formalen abantailak

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.

Metodo formalen desabantailak

Metodo formalen aplikazioa bermatzen duten erreminten garapena oso konplexua da eta, horretaz gain, metodoa erabiliz lortzen diren programak ez dira erosoak ezta erabilerrazak ere 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 horren kostu finala garestitu egiten du.

Baieztapen metodoak

Baieztapen metodo erabilienen artean hurrengoak daude:

E/S baieztapenak

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

Aurrebaldintza aske ahulena

Programa baten postbaldintza izanik eta atzerantz operatuz programa horren aurrebaldintzak lortuko direla dio aurrebaldintza aske ahulenaren baieztapenak.

Indukzio estrukturala

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.
Onartzen du P betetzen dela N baino txikiagoa edo berdina den Sren elementu kopuruarentzat.
Frogatzen du Sren N+1 elementuarentzat P proposizioa betetzen dela.