Metodo formalek softwarearen garapena zientifikoagoa eta beste ingeniaritza-diziplina batzuen antzekoagoa izatea eragiten dute, eta oinarri matematiko sendoak dituzten tresnen erabilera sustatzen dute, ondo finkatutako diziplinetan gertatzen den bezala. Metodo horiei formalak deitzen zaie matematikan oinarritzen direlako, batez ere logika matematikoan. Duela urte gutxi arte, teknika horiek erabiliz sistemen garapen industriala benetako arazoetan ariketa teoriko konplexu eta bideraezintzat jotzen zen. Baina sistema informatikoen konplexutasun eta garrantzi gero eta handiagoak agerian utzi zuen sistema horiek fidagarriak eta seguruak izatearen garrantzia, hau da, akatsik edo akatsik ez izatearena. Ez bakarrik akats horiek segurtasuna kritikoa den arloetan izan ditzaketen ondorio izugarriengatik, baita enpresei eragiten dieten ondorio ekonomikoengatik eta kalitateagatik ere. Horrekin guztiarekin batera, sistema informatikoek gero eta zeregin funtsezkoagoa dute gizartean (bereziki, gero eta presentzia handiagoa dute gizakiok egunero erabiltzen ditugun aparatuetan), eta industria-munduak jarrera aldatu zuen. Horrela, azken hamarkadetan metodo formalek aurrerapen nabarmena lortu dute, eta industria arloan duten erabilera ez da izan haien aurkariek ziurtatzen zuten utopia. Gaur egun, enpresa handiak daude, hala nola Intel, IBM, Sony, Siemens, Amazon edo Microsoft, oso modu aktiboan lan egiten dutela softwarearen garapen formalerako laguntza-tresnak sortzen eta aplikatzen, industria-aplikazio fidagarriak lortzeko. Izan ere, irakasgai honetan Microsoft-ek sortutako softwarea garatzeko tresna bat erabiltzen da: Dafny. Metodo formalen erabilgarritasuna eta garapen industrialetan duten eraginkortasuna gaur egun frogatuta dauden arren, oraindik lan gehiago falta da ingeniari gehienek ezagutu eta aplika ditzaten. Zeregin hori unibertsitateek (eduki akademikoetan sartu behar dituzte), irakasleek (jakintza-arlo horretan trebatu eta ikertu behar dute) eta ikasleek (matematikan eta logikan prestakuntza sendoagoa izan behar dute) egin behar dute. Irakasgai honek softwarearen ingeniariaren lana benetako ingeniaritza izatea lortzen laguntzen du, azken erabiltzaileak produktu fidagarriak eta seguruak jaso ditzan.

Irakasgai honen helburu zehatzak hauek dira:

- Programazioa artisau-jarduera baino jarduera zientifikoagoa izatearen garrantzia ulertzea.

- Softwarea garatzeko metodo formalen historia eta motibazioa ezagutzea.

- Softwarearen garapen formalaren arloko artearen egoera ezagutzea.

- Softwarea formalki garatzeko lengoaiak, metodoak eta tresnak ezagutzea.

- Softwarea formalki garatzeko lengoaiak eta tresna zehatzak erabiltzeko gaitasuna.

1. gaia.- Sarrera

2. gaia.- Indukzio matematikoa

3. gaia.- Dafny-ko lengoaia eta egiaztatzailerako sarrera

4. gaia.- Egiaztatzeko baldintzak sortzea

5. gaia.- Datu-motak

6. gaia.- Egiturazko indukzioa eta datatype-ak

7. gaia.- Array-ak eta Framing-a

Irakasgai honetan hainbat irakaskuntza-metodologia erabiltzen dira. Irakasgaiaren kontzeptuzko edukiak azaltzeko eskolak eta problema praktikoak ebazteko laborategiak emango dira. Bi kasuetan Dafny tresna erabiliko damodu interaktiboan: ikasleek tresna erabiltzen dute irakaslearekin batera. Ikasleek banaka garatu beharko dituzten problemak eta ariketak emango dira. Ikasleen ikaskuntza errazteko eta bermatzeko, ikasgelako eta ordenagailuko praktiken jarraipena egingo da. Planteatu diren ariketa guztien atzera-elikadura zehatza emango da, batez ere etengabeko ebaluaziorako balio dutenena, ikasleak lauhilekoan zehar beren ikaskuntza-mailaz jabetu daitezen.

• Ebaluazio Jarraituaren Sistema
• Azken Ebaluazioaren Sistema
• Kalifikazioko tresnak eta ehunekoak:
  • Banakako lanak (%): 100

Etengabeko ebaluazioko irakasgaia gainditzeko, ikasleek laborategian banakako hainbat lan praktiko egin beharko dituzte, ikasgelan lantzen diren tresna eta teknikei buruz duten ezagutza frogatzeko. Ikasleek lan horiei buruzko atzera-elikadura jasoko dute irakasleak zuzendu ahala, ikasteko baliagarriak izan daitezen.

Ebaluazio orokorra laborategian bakarkako lan praktiko bat egitean datza, ikasturtean zehar etengabeko ebaluaziorako egindako lanen baliokidea dena.

- Gelako gardenkiak.

- Tutoriala eta Web orriaren dokumentazioa: https://dafny.org/

Oinarrizko bibliografia

- Gelako gardenkiak.



- Tutoriala eta Web orriaren dokumentazioa: https://dafny.org/



- K. Rustan M. Leino. Program Proofs. MIT Press, March 2023. ISBN 9780262546232

Gehiago sakontzeko bibliografia

- Jim Woodcock, Peter Gorm Larsen, Juan Bicarregui, and John Fitzgerald.
Formal methods: Practice and Experience.
ACM Computing Surveys, 41(4):19:1–19:36, October 2009.

- Jason Koenig and K. Rustan M. Leino. Getting started with Dafny: a guide. In Marktoberdorf 2011 lecture notes. (http://research.microsoft.com/en-us/um/people/leino/papers/krml220.pdf)

- K. Rustan M. Leino. Dafny: An Automatic Program Verifier for Functional Correctness. In LPAR-16, volume 6355 of LNCS, pages 348-370. Springer, 2010. (http://research.microsoft.com/en-us/um/people/leino/papers/krml203.pdf)

- Edsger W. Dijkstra. A Discipline of Programming. Prentice-Hall, Incorporated, 1976, ISBN 0-613-92411-8

Aldizkariak

- ACM Transactions on Computational Logic
- ACM Transactions on Software Engineering and Methodology
- Applicable Algebra in Engineering, Communication and Computing.
- Formal Aspects of Computing
- Formal Methods in System Design
- Journal of Automated Reasoning
- Software Testing Verification & Reliability

Web helbideak

- Dafny: a language and program verifier for functional correctness
https://dafny.org/

- Formal Methods and Software Technology - Interesting Conferences
http://user.it.uu.se/~bengt/Info/conferences.shtml