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.

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.

- 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