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.- Datu-motak

5. gaia.- Egiturazko indukzioa eta datatype-ak

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

7. gaia.- Moduluak eta objektu orientzioa

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 eta lauhileko ikaskuntza-maila neurtuko duten arazoak eta ariketak erraztuko dira.

Etengabeko ebaluazioaren irakasgaia gainditzeko, ikasleek banakako hiru lan praktiko egin beharko dituzte laborategian, ikasgelan lantzen diren tresnak eta teknikak ezagutzen dituztela erakusteko. Lan praktiko bakoitzaren nota % 30ekoa da lehenengoarentzat, % 40koa bigarrenarentzat eta % 30ekoa hirugarrenarentzat.

- 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