TTKK Opinto-opas
81240 Ohjelmien todistaminen, 3,0 ov
Program Verification, 3,0 cu
Professori ANTTI VALMARI
Luentoja 42 h. Harjoituksia 28 h.
| Viikottainen Opetus / Periodi |
S1 | S2 | K1 | K2 | Kesä |
|---|
| Luennot (h) | 3+ | 3 |
- | - | - |
|---|
| Harjoitukset (h) | 2+ | 2 |
- | - | - |
|---|
Luentoaika ja -paikka
Maanantai 14-17 salissa TB207.
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.
Vaadittavat esitiedot
73116 Algoritmimatematiikka.
Suositeltavat esitiedot
81260 Johdatus tietojenkäsittelyteoriaan.
Huomautuksia
Voidaan sisäöllyttää myös jatko-opintoihin. Luennoidaan parillisina vuosina.
Vuorottelee kurssin 81270 kanssa.
Linkkejä
Kurssin kotisivu.