2D1454/2G1117 Semantik för Programspråk

Kursanalys VT06

Kursdata

Mål

Vad är och hur beter sig en program ur en 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 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 hyfsat bra. Studenternas aktiva deltagande under lektionerna var en bra indikation. Ett problem var dock att IT-studenterna visade betydligt sämre förkunskaper och träning på diskretmatematisk och logisk resonemang än D-studenterna.

Undervisningen

Jag brukar blanda föreläsningar med övningar och studenterna verkar uppskatta detta.

Examination

Examinationen består av en skriftlig tenta med 5 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.

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. Som konkreta förbättringsföreslag vill studenterna ha fler hemuppgifter. 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 en hemuppgift som självutvärdering under andra hälften av 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, men det visade sig att D studenterna har betydligt bättre färdigheter i detta än IT studenterna.

Verkligt kursinnehåll

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

Övrigt

Om jag får mera tid enligt budget, skulle jag gärna vilja utveckla flera hemuppgifter som kunde ge bonuspoäng till tentan, och förbereda lecture notes som handouts.

Planerade förändringar

Kursen flyttas till period 2. Inga andra större förändringar planeras: efter flera omgånger har kursen stabiliserats.