DD2454 Semantik för Programspråk

Kursanalys HT07

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: vad fokuserar varenda stil på, vilken slags programanalys är de lämpliga för? Olika programegenskap betraktas och diskuteras hur de formaliseras och bevisas.

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

Jag införde 3 hemuppgifter, en för varje kursdel.

Sammanfattning

Enligt min uppfattning gick kursen mycket bra. Studenternas aktiva deltagande under lektionerna var en klar indikation på detta.

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 bestod av en skriftlig tenta med 7 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.

Ny betygsskala A-F

Jag har inte lyckats än att formulera en tabell som definerar vad exakt man bor kunna för att få ett visst betyg. Jag anser att detta inte är så lätt för den här kursen, därför använde jag mig av en finare, fast fortfarande lineär skala baserad på poäng. Nästa omgång ska jag försöka införa en betygstabell.

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. Jag funderar på att byta till en annan bok.

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 flera exempel på problemlösning, och kanske införa en programeringsuppgift och en ny kursbok. 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 och förberedning 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

På grund av dålig budget kommer föreläsningslängden att halveras. Ny kursbok kommer kanske att införas.