2D1454 Semantik för Programspråk

Kursanalys HT06

Kursdata

Mål

Vad är och hur beter sig en program ur en formell matematiskt synpunkt? Svaret på denna fråga är nödvändigt för att kunna analysera program på ett formellt sätt. De tre viktigaste semantikstilarna betraktas: operationell, denotationell och axiomatisk semantik. Stilarna jämföras och relateras till varandra: på vad fokuserar varenda stil, till vilken slags programanalys är de lämpliga? Olika programegenskaper betraktas och diskuteras hur de formaliseras och bevisas.

Förändringar inför denna kursomgång

Inga större förändringar: efter flera omgånger har kursen stabiliserats.

Sammanfattning

Enligt min uppfattning gick kursen mycket bra. Studenternas aktiva deltagande under lektionerna var en klar indikation på detta. Tyvärr har antalet studenter minskat, vilket å andra sidan har effekten av en mera direkt och intensiv interaktion.

Undervisningen

Jag brukar blanda föreläsningar med övningar och studenterna verkar uppskatta detta. Jag stimulerar aktivt deltagande för att få direkt feedback och på så sätt hålla koll på hur studenterna följer materialet.

Examination

Examinationen består av en skriftlig tenta med 6 problem. En del av dem handlar om att bygga semantiska verktyg. En annan del handlar om att använda olika semantiska stil för att göra programanalys. En tredje del handlar om att bevisa olika språk- och programegenskap. Själva tentan (med lösningar) finns här.

Kurslitteratur

I kursen används boken The Formal Semantics of Programming Languages av Glynn Winskel, MIT Press, 1993. Boken passar väldigt bra min undervisningsstil. Nackdelar är det relativt komplexa innehållet, och att bara hälften av boken kan genomgås i kursen. Boken komplementeras delvis med material (handouts) om small-step och abstract-machine semantik.

Elevenkät

Studenterna gav höga betyg på nästan alla frågor, särskild angående min insats. Ett konkret förbättringsföreslag är att ge mera praktiska exempel. Hela kursutvärderingen finns här.

Kursens belastning för eleverna

Enligt min uppfattning är studenterna inte särskilt belastade under kursen. De gör tre hemuppgift som självutvärdering under kursen.

Förkunskaper

Förkunskaper som är väsentliga för kursen är Diskret Matematik och Logik. Det svåraste i kursen är att genomföra induktiva bevis. De flesta studenter verkade ha tillräckliga förkunskaper.

Verkligt kursinnehåll

Verkliga kursinnehållet kan ses på följande länk.

Övrigt

Kursen är en viktig moment i varje teoretisk-datalogisk curriculum. Tyvärr är den inte obligatorisk i vår skola, och antalet studenter har minskat farligt.

Planerade förändringar

Inga större förändringar planeras: efter flera omgånger har kursen stabiliserats.