Programen espezifikazio, egiaztapen eta eratorpen formala
UPV/EHUrekin koedizioan argitaratua
Gaur egun, software fidagarria, hau da errorerik gabea, sortu ahal izateko ezagutza, metodoak eta teknologia egon badaude. Horren erakusgarri da, adibidez, liburu honen lehenengo kapituluan azaltzen den Parisko garraio-sarearen kontrolerako softwarea. Beste froga bat, azken 10-15 urteetan software-akatsen ondorioz sortutako istripu larririk ia-ia ez egon izana da. Hori dela-eta, liburu honen bidez gure ekarpena egin nahi dugu nazioarteko komunitateak dagoeneko bere gain hartu duen erronka batean: software-industriak zeharo fidagarriak diren aplikazioak garatzera jo behar du. Horretarako, software-garatzaileek aplikazio erabat fidagarriak garatu ahal izateko erreminta eta teknikak erabiltzeko eta sortzeko gaitasuna emango dien prestakuntza zientifiko-teknikoa izatea beharrezkoa da. Liburu honek software fidagarria eraikitzeko erabiltzen diren metodoen atzean dauden programen espezifikazio-, transformazio- eta egiaztapen-tekniken hastapenak ikasteko aukera eskaintzea du helburu, hemen agertzen den materiala oinarrizko prestakuntza-ikastaro baterako egokia delarik.
Zehazki, UPV/EHU Euskal Herriko Unibertsitatean ezarrita dauden Informatika Ingeniaritza Gradu desberdinetan irakasten den Programazioaren Metodologia irakasgaiaren testuliburua den honako hau programazio-arloan hasi berria den edonorentzat baliagarria da.
IRUDIEN ZERRENDA
HITZAURREA
1. SARRERA
1.1. Softwarearen garapenerako metodo formalak
1.2. Liburuaren deskribapena
1.3. Esker onak
2. PROGRAMEN ESPEZIFIKAZIO FORMALA
2.1. Espezifikazioaren kontzeptua
2.2. Lehen mailako asertzioak: egoerak adierazteko formulak
2.2.1. Lehen mailako asertzioen sintaxia
2.2.2. Lehen mailako asertzioen semantika
2.3. Ariketak: Lehen mailako asertzioak
2.4. Aldibereko ordezkapena
2.5. Baliozko inplikazioak
2.6. Programen aurre-ondoetako espezifikazio formala
2.7. Ariketak: Programen aurre-ondoetako espezifikazio formala
2.8. Bibliografia-oharrak
2.9. Ariketak: Programen espezifikazio formala
3. PROGRAMA ITERATIBOEN EGIAZTAPENA
3.1. Programen zuzentasuna
3.2. Hoare-ren sistema formala
3.3. Esleipena
3.4. Ariketak: Esleipena
3.5. Konposaketa sekuentziala
3.6. Ariketak: Konposaketa sekuentziala
3.7. Baldintzazko aginduak
3.8. Ariketak: Baldintzazko aginduak
3.9. Inbarianteak eta iterazioen zuzentasun partziala
3.10. Ariketak: Inbarianteak eta iterazioen zuzentasun partziala
3.11. Asertzioak eta programen dokumentazioa
3.12. Ariketak: Asertzioak eta programen dokumentazioa
3.13. Borne-adierazpenak eta iterazioen bukaera
3.14. Ariketak: Borne-adierazpenak eta iterazioen bukaera
3.15. Bibliografia-oharrak
3.16. Ariketak: Programa iteratiboen egiaztapena
4. PROGRAMA ERREKURTSIBOEN EGIAZTAPENA
4.1. Definizio errekurtsiboak
4.2. Programa errekurtsiboak
4.3. Ariketak: Programa errekurtsiboen azterketa
4.4. Programa errekurtsiboen egiaztapena
4.4.1. Errekurtsio anizkoitza eta konjuntzioaren erregela .
4.5. Bibliografia-oharrak
4.6. Ariketak: Programa errekurtsiboen egiaztapena
5. DATU-MOTEN ESPEZIFIKAZIO EKUAZIONALA
5.1. Datu-mota abstraktuak (DMA-ak)
5.2. Espezifikazio ekuazionalaren teknika
5.3. Oinarrizko DMAen espezifikazio ekuazionala
5.4. Ariketak: Sekuentziak
5.5. Ariketak: Pilak
5.6. Ariketak: Zuhaitz bitarrak
5.7. Propietateen frogapena
5.8. Bibliografia-oharrak
5.9. Ariketak: Datu-moten espezifikazio ekuazionala
6. ERREKURTSIBOTIK ITERATIBORAKO TRANSFORMAZIOA
6.1. Errekurtsibotik iteratibora transformatzeko metodoak
6.2. Destolesketa/tolesketa metodoa — Oinarrizko eskema
6.3. Ariketak: Destolesketa/tolesketa metodoa — Oinarrizko eskema
6.4. Destolesketa/tolesketa metodoa — Eskema orokorra
6.5. Bibliografia-oharrak
6.6. Ariketak: Errekurtsibotik iteratiborako transformazioa
7. PROGRAMA ITERATIBOEN ERATORPENA
7.1. Programen eratorpen formalerako metodoa
7.2. Iterazioen eratorpen formala
7.3. Ariketak: Zenbakiei buruzko iterazioen eratorpena
7.4. Inbarianteak sortzeko jarraibideak 234
7.5. Bektoreekin kalkuluak egiten dituzten iterazioen eratorpena
7.6. Fibonacci-ren segida
7.7. Ariketa: Fibonacciren terminoak kalkulatzeko beste era bat
7.8. Bektoreak aldatzen dituzten programen eratorpena
7.9. Zenbaki lagunak
7.10. Bibliografia-oharrak
7.11. Ariketak: programa iteratiboen eratorpena
8. PROGRAMA ERREKURTSIBOEN ERATORPENA
8.1. Programa errekurtsiboen eratorpen formala
8.2. Murgilketaren teknika
8.3. Ariketak: Eratorpena eta murgilketa
8.4. Murgilketa eraginkortasuna lortzeko
8.5. Bibliografia-oharrak
8.6. Ariketak: Programa errekurtsiboen eratorpena
BIBLIOGRAFIA
GLOSARIOA
Liburu honen doako edizioa deskargatzeko webgunean login egin behar da:
Sartu