Rökfræði í hugbúnaðargerð
TÖL402G Vor 2012
Almennar upplýsingar
Kennari í námskeiðinu er Páll Melsted lektor í tölvunarfræði. Bókin sem við notum í námskeiðinu heitir Logic in Computer Science: Modelling and Reasoning about Systems eftir Michael Huth og Mark Ryan og fæst í Bóksölunni.
Lögð verða fyrir vikuleg heimadæmi, bæði verkefni úr bókinni og af vikublöðum.
Yfirlit yfir námsefni
Tímar
- Fyrirlestrar eru á miðvikudögum kl. 8:20-9:50 og á föstudögum kl. 10:00-10:40 í Naustinu í kjallara Endurmenntunar (merkt Et á stundatöflu).
- Dæmatímar eru á miðvikudögum kl. 10:50-12:20 strax að loknum fyrirlestri í sömu stofu.
Námsmat
- Lokaeinkunn er 70% prófseinkunn og 30% meðaltal 10 af 12 bestu heimadæmum
Vikublöð og verkefni.
Vikublöð
- Vikublað 1
- Vikublað 2
- Vikublað 3
- Vikublað 4
- Vikublað 5
- Leiðrétt Figure 2.6 bls. 145 í bók fyrir Alloy 4. Ath. að Alloy 4 breytti um rithátt fyrir fun.
- Vikublað 6
- Dæmi í Alloy - FileSystem - einfalt
- Vikublað 7
- Vikublað 8
- Vikublað 9
- simple.smv lagað frá dæminu í bókinni til að virka með nýrri útgáfum af NuSMV
- Vikublað 10
- Vikublað 11
- Vikublað 12
- Sönnun á log2 dæmi – fastayrðingin sem við notuðum í tíma virkar ekki.
- Vikublað 13 – skil þriðjudaginn 17. apríl kl. 16:00 í hólf kennara.
Ýmislegt efni tengt námskeiðinu
- Natural deduction – grein á Wikipedia
- List of logic symbols – yfirlit á Wikipedia, með LaTeX nöfnum fyrir tákn
- Sönnunarbox í LaTeX – frá Paul Taylor, þetta er pakkinn sem höfundar bókarinnar notuðu.
- Alloy Alloy líkanagerðarmálið
- Inngangur að Alloy eftir Kristján Jónasson Blað 1, Blað 2
- NuSMV líkanaprófun.