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].
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.
Baieztapen metodo erabilienen artean hurrengoak daude:
Tony Hoarek garaturiko metodoaren logika erabiltzen duen programa jakin baten sartzen diren datuak programaren aurrebaldintzak betetzen badituzte, irteerako datuek postbaldintzak ere beteko dituzte.
Programa baten postbaldintza izanik eta atzerantz operatuz programa horren aurrebaldintzak lortuko direla dio aurrebaldintza aske ahulenaren baieztapenak.
Indukzio matematikoan oinarrituriko baieztapen teknika honen arabera, S propietate jakin batzuk eta propietate horiekin frogatu nahi den P proposizioa izanik:
| Autoritate kontrola |
|
|---|
Datuak: Q1049183
Multimedia: Formal methods / Q1049183