IRAKASGAIAREN AZALPENA: Programa bat zuzena al den erabakitzeko bide bat, programari datuak ematea eta lortzen diren emaitzak zuzenak al diren aztertzea da. Bestalde, programa bat eraikitzeko bide bat, programatzailearen ezagutza ez-formalean oinarritzea da; era horretan programa eraiki ondoren, programari datuak eman eta emaitzak egokiak al diren erabaki beharko da; eta, beharrezkoa baldin bada, zuzenketak egin beharko dira. Bide horretatik joanez, zaila da programa bat benetan zuzena dela ziurtatzea. Irakasgai honetan programen zuzentasuna aztertzeko eta programa zuzenak eraikitzeko balio duten metodo matematikoak aurkeztuko dira. Metodo horien bidez, programa bat zuzena al den ala ez froga daiteke matematikoki eta, era berean, zuzenak diren programak eraiki daitezke.

TESTUINGURUA: Irakasgai hau lehenengo mailako bigarren lauhilekoan kokatuta dago eta irakasgai honetara iritsi aurretik programazio agintzailearen oinarriak aurkeztu dira baina era ez-formalean. Beraz, orain une egokia da programazioa metodo matematikoen bidez lantzeko eta programazio-ohitura onak hartzeko. Irakasgai honetan lortutako ezagutza, programazioan sakontzeaz arduratuko diren beste irakasgaietan oso lagungarria izan daiteke.

IRAKASGAIARI DAGOZKION BEREZKO GAITASUNAK:



M02CM06: Teknologia informatikoen oinarrizko prozedura algoritmikoak jakitea eta aplikatzea arazoentzat soluzioak diseinatzeko, proposatutako algoritmoen egokitasuna eta konplexutasuna analizatuta.



M02CM08: Aplikazioak modu sendo, seguru eta eraginkorrean analizatzeko, diseinatzeko eta mantentzeko gaitasuna, paradigma eta programazio-lengoaia egokienak aukeratuta.

1. Gaia. Sarrera: Espezifikazioa, zuzentasuna eta kontratu bidezko diseinua.

2. Gaia. Programak espezifikatzeko eta dokumentatzeko metodo formala: Aurre-ondoetako espezifikazioa.

3. Gaia. Programak egiaztatzeko metodo formala: Hoare-ren sistema formala.

4. Gaia. Programak eratortzeko metodo formala: Hoare-ren sistema formalean oinarritutako metodoa.

5. Gaia. Datu-mota abstraktuen espezifikazio aljebraikoa (edo ekuazio bidezko espezifikazioa).

6. Gaia. Programa errekurtsiboen eraldaketa: Errekurtsibotik iteratiborako eraldaketa.

Ikastaroaren garapenean, ikaslearen parte-hartze zuzena eta ikasteko era kooperatiboa eta dinamikoa bultzatzeko eta ikaslearen motibazioa indartzeko, talde-lana, eztabaida eta ariketen emaitzen aurkezpena hartuko dira klaseak antolatzeko oinarri gisa.

• Ebaluazio Jarraituaren Sistema
• Azken Ebaluazioaren Sistema
• Kalifikazioko tresnak eta ehunekoak:
  • Garatu beharreko proba idatzia (%): 60
  • Praktikak egitea (ariketak, kasuak edo buruketak) (%): 40

EBALUAZIO JARRAITUA:

Edukien zerrendako atal bakoitzean landutako gaitasunak ebaluatzeko, bost azterketa partzial egingo dira lauhilekoan zehar. Azterketa partzial bakoitza hainbat ariketez osatuta egongo da. Azterketa partzial horiei dagokien puntuazioa honako hau da: 2. gaiari dagokion azterketak 2 puntuko balioa izango du; 3. gaiari dagokion azterketak 2 puntuko balioa izango du; 4. gaiari dagokion azterketak 1,5 puntuko balioa izango du; 5. gaiari dagokion azterketak 2,5 puntuko balioa izango du; azkenik, 6. gaiari dagokion azterketak 2 puntuko balioa izango du. Ariketa bat gainditzeak, ariketari dagokion atala liberatzea eta bere nota gordetzea dakar ikasturte osorako. Ariketa bat gainditzeko, ariketari dagokion puntuazioaren erdira iritsi nahikoa izango da. Bukaerako notarako, gainditutako ariketei dagozkien puntuazioak bakarrik hartuko dira kontuan. Irakasgaia gainditzeko 5 puntura iritsi beharko da (guztira 10 puntu lortu daitezkeelarik).



Ohiko eta ezohiko deialdietako probetan, lauhilekoan zehar gainditu gabe edo ebaluatu gabe gelditu diren atalak ebaluatuko dira.



BUKAERAKO EBALUAZIOA:

Ebaluazio jarraitua ez aukeratuz gero, lauhilekoaren bukaeran 10 puntuko balioa izango duen azterketa baten bidezko ebaluazioa egingo da. Hor, 5 puntu lortzea nahikoa izango da irakasgaia gainditzeko. Hemen ere, gainditutako ariketak bakarrik hartuko dira kontuan (hau da, ariketa batean lortutako puntuazioa, bakarrik ariketari dagokion puntuazioaren erdira iritsi bada hartuko da kontuan).



EZ AURKEZTUA:

"Ez aurkeztua" kalifikazioa ipintzeko honako irizpide hau hartuko da kontuan:

Ebaluazio jarraitua aukeratu duten ikasleen kasuan, lauhilekoan zehar egindako proben bidez irakasgaia gainditzea ez bada lortu, ohiko deialdiari dagokion probara ez aurkeztea nahikoa izango da "Ez aurkeztua" ipintzeko. Bukaerako ebaluazioa aukeratu duten ikasleen kasuan, ohiko deialdiari dagokion probara ez aurkeztea nahikoa izango da "Ez aurkeztua" ipintzeko. Ezohiko deialdian ere era berean jokatuko da.



EBALUAZIO ERAREN ALDAKETA: EBALUAZIO JARRAITUTIK BUKAERAKO EBALUAZIORA

Hasieran "ebaluazio jarraitua" aukeratu duten ikasleek "bukaerako ebaluazioa" erara bukaerako azterketa baino lehenagoko edozein unetan aldatzeko aukera izango dute (bai ohiko deialdian eta bai ezohiko deialdian ere).



Goian zehaztutako ebaluazio-metodoa "Ikasleen Ebaluaziorako Arautegia" kontuan hartuta planteatu da:

https://www.ehu.eus/eu/web/estudiosdegrado-gradukoikasketak/ebaluaziorako-arautegia

Ohiko deialdirako zehaztutako irizpide eta baldintzei eutsiko zaie.

eGela-n ikasleen esku dagoen materiala. Batez ere gai bakoitzeko apunteak eta ariketen enuntziatuak.

Oinarrizko bibliografia

Programen Espezifikazio, Egiaztapen eta Eratorpen Formala. Javier Álvez, Xabier Arregi, Jose Gaintzarain, Paqui Lucio, Montse Maritxalar. Udako Euskal Unibertsitatea (UEU), 2016.



Especificación, Verificación y Derivación Formal de Programas. Javier Álvez, Xabier Arregi, Jose Gaintzarain, Paqui Lucio, Montse Maritxalar. Pearson, 2015.



Programen Egiaztapena eta Eratorpena. X. Arregi, A. Díaz de Ilaraza, P. Lucio. Udako euskal Unibersitatea, 1993.



Metodología y Tecnología de la Programación II. M. Díaz Roca,, J. C. Rodríguez del Pino. Univ. Palmas Gran Canaria, 2004.



Verificación de Programas y Metodología de la Programación. A. Díaz de Ilarraza, P. Lucio. Servicio Editorial Universidad del País Vasco, 1990.



Program Derivation. The Development of Programs from Specifications. G. Dromey. Addison-Wesley, 1989.

Gehiago sakontzeko bibliografia

Program Construction and Verification. R. C. Backhouse. Prentice-Hall, 1986.

Programación metódica. J.L. Balcázar. MacGraw-Hill, 1993.

Diseño de Programas.- Formalismo y Abstracción. Ricardo Peña. Prentice Hall, 1998.

Aldizkariak

Acta Informatica
Programming and Computer Software
Science of Computer Programming
Software Quality Journal
Transactions on Software Engineering and Methodology

Web helbideak

http://www.sc.ehu.es/jiwlucap/metodologia.html

http://en.wikipedia.org/wiki/Formal_verification

http://en.wikipedia.org/wiki/Design_by_contract