XSLaren edukia
Softwarea Garatzeko Metodo Formalak
- Ikastegia
- Informatika Fakultatea
- Titulazioa
- Informatikaren Ingeniaritzako Gradua
- Ikasturtea
- 2024/25
- Maila
- 4
- Kreditu kopurua
- 6
- Hizkuntzak
- Gaztelania
IrakaskuntzaToggle Navigation
Irakaskuntza mota | Ikasgelako eskola-orduak | Ikaslearen ikasgelaz kanpoko jardueren orduak |
---|---|---|
Magistrala | 40 | 60 |
Laborategiko p. | 20 | 30 |
Irakaskuntza-gidaToggle Navigation
HelburuakToggle Navigation
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.
Irakasgai-zerrendaToggle Navigation
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
MetodologiaToggle Navigation
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.
Ebaluazio-sistemakToggle Navigation
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.
Nahitaez erabili beharreko materialaToggle Navigation
- Gelako gardenkiak.
- Tutoriala eta Web orriaren dokumentazioa: https://dafny.org/
BibliografiaToggle Navigation
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
TaldeakToggle Navigation
16 Teoriakoa (Gaztelania - Arratsaldez)Erakutsi/izkutatu azpiorriak
Asteak | Astelehena | Asteartea | Asteazkena | Osteguna | Ostirala |
---|---|---|---|---|---|
16-30 | 14:00-15:30 | 15:30-17:00 |
Irakasleak
16 Laborategiko p.-1 (Gaztelania - Arratsaldez)Erakutsi/izkutatu azpiorriak
Asteak | Astelehena | Asteartea | Asteazkena | Osteguna | Ostirala |
---|---|---|---|---|---|
16-30 | 17:00-18:30 |