8101160
OHJELMIEN TODISTAMINEN,
PROGRAM VERIFICATION, 3 ov
Tietoa luennoitsijoista
Professori ANTTI VALMARI
Luentoja ja harjoituksia
Luentoja yhteensä 42 h. Harjoituksia yhteensä 26 h.
Viikottainen opetus/periodi |
|
|
|
|
|
Luennot (h): |
3+ |
3 |
- |
- |
- |
Harjoitukset (h): |
2+ |
2 |
- |
- |
- |
Tavoitteet
Luoda opiskelijalle valmiuksia ymmärtää ja käyttää matemaattisia menetelmiä ohjelmistotyön, erityisesti algoritmien määrittelyn ja suunnittelun sekä vaikeiden ohjelman osien ja vaikeiden algoritmien toteuttamisen apuna.
Sisältö
Algoritmien ja pienten ohjelmien spesifiointi ja oikeaksi osoittaminen logiikan ja joukko-opin avulla. Formaalien menetelmien periaatteelliset ja käytännölliset rajoitukset.
Tutkintovaatimukset
Pakolliset laskuharjoitukset ja tentti.
Kirjallisuus
Luentomonisteet. Tukena voi käyttää kirjaa Backhouse, R.: Program Construction and Verification.
Tietoa esitietovaatimuksista
Esitietovaatimuksiin merkityistä 81-kursseista riittää toinen.
Esitiedot
Numero |
Nimi |
|
|
8101100 |
4 |
Pakollinen |
|
73116 |
3 |
Pakollinen |
|
8100500 |
3 |
Pakollinen |
Huomautuksia
Voidaan sisällyttää myös jatko-opintoihin. Luennoidaan parillisina vuosina. Vuorottelee kurssin 8101150 kanssa.