2D1454 Semantik för
Programspråk
Kursanalys HT06
Kursdata
- Kurs: Semantik för programspråk, 4p.
- Omgång: HT06, Period 2
- Kursledare: Dilian Gurov
- Kursformat: 30t. lektioner (föreläsningar blandade
med övningar)
- Antal registrerade elever: 8
- Antal direkt avhoppade elever: 0
- Kurslitteratur: Glynn Winskel: The
Formal
Semantics of Programming Languages, MIT Press, 1993
- Moment: TEN1, 4p.
- Elever som klarat kursen: 6
- Prestationsgrad efter första examinationstillfället:
5: 4, 4: 1, 3: 1, U: 2
- Examinationsgrad efter första examinationstillfället:
75%
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.