Info
Täiendavaid ja huvitavamaid teemasid automaatide, keelte ja translaatorite kohta nendele, kellel on sügavam huvi programmeerimiskeelte vastu.
- Maht: 3 EAP.
- Hindamine: Mitte-eristav.
- Toimumine: R 14:15–15:45, Δ - 1008 (ei salvestata/kanta üle Zoom-is).
- Õppejõud: Simmo Saan.
- Registreerumine:
- Enne semestri algust: ise ÕIS-is.
- Pärast semestri algust: kirjuta Zulip-is/email.
- Hinde kujunemine:
- OCaml-is programmeerimise kodutööd.
- Kõik esitatud ja arvestatud (vähemalt pooled koduseks jäetud testidest lähevad läbi).
- Maha registreerumine:
- Kuni kaks nädalat esimesest toimumisest: ise ÕIS-is.
- Kuni "Programmide mudelkontroll" kodutöö tähtajani: kirjuta Zulip-is/email.
Sisu lühikirjeldus
Kursus sisaldab täiendavaid teemasid automaatide, keelte ja translaatorite kohta.
- OCaml-i keele kiirkursus, milles kõike hakatakse implementeerima.
- Automaadid tarkvaravigade tuvastamiseks: juhtimisvoo automaadid, olekute otseesitusega mudelikontroll.
- Automaatne verifitseerimine: korrektne staatiline analüüs, abstraktne interpretatsioon, mitmelõimeliste programmide analüüs.
- Deduktiivsed meetodid: automaatsed teoreemitõestajad.
Järgmises imekaunis diagrammis on kursusel käsitletavad meetodid paigutatud vastavalt omadustele, mida nad kõige paremini rahuldavad. Ükski meetod siin ei ole parem kui teine: kui tahta kõiki neid omadusi rahuldada, siis peab ikkagi ohverdusi tegema, näiteks täpsuses või kiiruses.
- Automaatika tähendab, et meetod vajab vähe juhtimist inimese poolt.
- Väljendusrikkuse ehk väljendusvõime (expressivity) all mõeldakse seda, kui keerulisi omadusi on võimalik antud meetodis väljendada ja kontrollida.
- Olekuruumi suurus eristab meetodeid, mis töötavad hästi lõplikel süsteemidel (näiteks riistvara või UML mudelid), nendest meetoditest, mis analüüsivad programme, kus masina kõiki võimalikke olekuid (nt. muutujate sisu, kutsepinu ja lõimede ajastamine) on piiramatult palju ehk on lõpmatu olekuruum.