Programmacorrectheid
periode 3, 2010-2011

Deze pagina kan tijdens de cursus herhaaldelijk gewijzigd worden.
Last modified: Wed Jul 13 13:49:31 CEST 2011

Nieuw: De toets van 11 maart 2011 en een uitwerking daarvan. De toets is nagekeken; de cijfers staan op Nestor.

Docent voor het hoorcollege Wim H. Hesselink (Bernoulliborg, kamer 374).
Docenten voor het werkcollege: Jan Jongejan (Bernoulliborg, kamer 366) en Sebastian Verschoor.

De cursus is gebaseerd op de syllabus Programmacorrectheid, die verkrijgbaar is bij de Repro in de Bernoulliborg. Deze syllabus wordt zowel bij het hoorcollege als bij het werkcollege intensief gebruikt.
Enige links:
Rooster van dit vak.
Aanvullende syllabus over lineaire bewijzen (19 februari 2007).

Beschikbaar zijn de volgende oude toetsen en tentamens.
De toets van 1 maart 2010 en een uitwerking daarvan. Merk op, dat de toets toen eerder in de cursus viel en daarom minder stof dekte.
De toets van 3 maart 2009.
De toets van 5 maart 2008 en een uitwerking daarvan.
Het tentamen van 9 april 2010 en een uitwerking daarvan.
Het tentamen van 14 april 2009 en een uitwerking daarvan.
Het tentamen van 21 april 2008 en een uitwerking daarvan.

Aantekeningen bij een voordracht voor Orientatie Informatica over programmacorrectheid (27 november 2006).
Een tekst voor het Jongerejaarscolloquium (11 januari 2007).

Doelstelling

Van grote stukken software is eenvoudig vast te stellen dat ze correct zijn. Geregeld echter zijn er situaties waarin het lastig is in te zien dat een programmafragment aan zijn specificatie voldoet of waarin de correctheid zo belangrijk is dat niet vertrouwd kan worden op informele overwegingen. Deze cursus heeft tot doel de student voldoende gereedschap aan te reiken om, op momenten dat dat nodig is, de correctheid van een programmafragment formeel vast te stellen.

Om te komen tot een formeel correctheidsbewijs van een programmafragment is het nodig de specificatie in een formele taal te noteren. In deze cursus is de formele specificatie soms gegeven, maar je zult ook leren om bij een informele beschrijving een formele specificatie op te stellen.

Werkvormen

Hoorcollege. Tijdens het hoorcollege worden uitgaande van aanwezige programmeerkennis, bewijsregels afgeleid. Aan de hand van voorbeelden wordt duidelijk gemaakt hoe deze bewijsregels functioneren bij het ontwikkelen van geannoteerde programmafragmenten.

Werkcollege. Tijdens het werkcollege krijgen de studenten de gelegenheid om onder begeleiding van een docent de leerstof te verwerken aan de hand van oefeningen.

We hebben in de eerste helft van de cursus tamelijk veel tijd nodig voor het uitleggen van het hoe en waarom van het opstellen van specificaties en het afleiden van correcte programma's. Je moet er ook al veel mee oefenen, maar de programma's zijn i.h.a. nog niet moeilijk. Tijdens de tweede helft zijn de programma's moeilijker en kost het oefenen veel meer tijd. Er is daarom in de eerste helft meer tijd voor hoorcollege uitgetrokken en in de tweede helft meer tijd voor werkcollege. Gebruik deze tijd goed.

Syllabus. Zowel het hoorcollege als het werkcollege zijn gebaseerd op de syllabus Programmacorrectheid van W. H. Hesselink en G. R. Renardel de Lavalette, die je kunt kopen bij de Repro in de Bernoulliborg.

Huiswerk. Bij dit vak is het zorgvuldig noteren van een programmafragment met annotatie een dusdanig belangrijk aspect, dat studenten geregeld feedback moeten krijgen op hun manier van presenteren. Daartoe dienen de inleveropgaven: maak elke week het huiswerk dat uit een of meer opgaven bestaat en lever dit op papier op tijd in via het postvakje van Hesselink (4de verdieping noord). Er is 6 keer huiswerk. Het huiswerk telt in het totaal mee voor 25% in de eindbeoordeling. De huiswerksets tellen elk voor 4% mee, behalve de 5de set die voor 5% mee telt. Het huiswerk mag in koppels van 2 gemaakt worden, maar niet in grotere koppels.

Tussentoets. Aan het eind van week 4 is er een tussentoets die voor 25% meetelt in het eindcijfer.

Zelfwerkzaamheid. In de collegeperiode 7 uur per week, met een reserve van 40 uur voor tentamenvoorbereiding.

Wekenschema

Het wekenschema gaat uit van 6 contacturen per week gedurende 7 weken. De eerste drie weken zijn er 4 uur hoorcollege per week en 2 uur werkcollege per week. Aan het eind van week 4 is er een schriftelijke individuele toets. In de resterende weken is er 2 uur hoorcollege per week en 4 uur werkcollege per week. Het onderstaande schema is indicatief en kan nog aangepast en verfijnd worden.

Feitelijke invulling.

Week 1(7) Zorg dat je het dictaat hebt. Dit is verkrijgbaar bij de Repro van de Bernoulliborg. Lees de hoofdstukken 1, 2 en 3 al vast goed door.
Dinsdag 15 februari. Hoorcollege. Behandeling van de hoofdstukken 3 en 5 (en 1, 2, 4 voorzover van toepassing).
Woensdag/donderdag 16/17 februari. Werkcollege: opgaven 3.6, 3.12, 5.1(a,c,e), 5.2, 5.16.
Vrijdag 18 februari. Hoorcollege over hoofdstuk 6.
Vrijdag 18 februari. Huiswerk hw1: opgaven 5.1(b,d) en 5.10 voor 15:00 op papier in postvakje van Hesselink (Bernoulliborg, vierde verdieping noord).

Week 2(8). Bestudeer de hoofdstukken 6 en 7.
NB: Woensdag 23 februari (13:00-14:45). Hoorcollege. Bespreking van het huiswerk en van de annotatie-eisen. Stappenplan, behandeling van 6.4.
Woensdag/donderdag 23/24 februari. Werkcollege: opgaven 3.16 en H 6: 1, 2, 3, 4.
Vrijdag 25 februari. Hoorcollege. Hoofdstuk 7: het vinden van de invariant.
Vrijdag 25 februari. Huiswerk hw2: opgave 6.6 op papier voor 15:00 uur.

Week 3(9). Bestudeer hoofdstuk 8.
Dinsdag 1 maart. Hoorcollege. Bespreking huiswerk, het onderscheid tussen lineaire bewijzen (bij de stappen 1 en 3) en geannoteerde commando's (bij de stappen 2 en 4); behandeling hoofdstuk 8.
Woensdag/donderdag 2/3 maart. Werkcollege: opgaven 5.15(a), H 7: 1, 5, 11(a), H 8: 2.
Vrijdag 4 maart. Hoorcollege. Hoofdstuk 8 vervolg.
Vrijdag 4 maart. Huiswerk hw3: opgave 8.3 op papier voor 15:00 uur.

Week 4(10). Bestudeer het hele dictaat tot en met hoofdstuk 8.
Dinsdag 8 maart. Hoorcollege. Bespreking huiswerk. Gelegenheid tot vragen ter voorbereiding van de toets.
Woensdag/donderdag 9/10 maart. Werkcollege: opgaven H 8: 4, 8, 15.
Vrijdag 11 maart: geen hoorcollege.
Vrijdag 11 maart. Toets in de tentamenhal, tijd 14:00-16:00. Stof: dictaat tot en met hoofdstuk 8, alle opgegeven opgaven.
Geen huiswerk ivm de toets.

Week 5(11). Bestudeer hoofdstuk 9 van het dictaat.
Dinsdag 15 maart. Twee-dimensionale telproblemen: hoofdstuk 9.
Dinsdag/woensdag 15/16 maart. Werkcollege: opgaven H 9: 2, 3, 4.
Donderdag/vrijdag 17/18 maart. Werkcollege: opgaven H 9: 5, 6.
Vrijdag 18 maart. Huiswerk hw4: opgave 9.7 op papier voor 15:00 uur.

Week 6(12). Bestudeer hoofdstuk 9 nogmaals.
Dinsdag 22 maart. Hoorcollege: bespreking huiswerk en opnieuw hoofdstuk 9.
Dinsdag/woensdag 22/23 maart. Werkcollege: opgaven H 9: 8, 9, (10).
Donderdag/vrijdag 24/25 maart. Werkcollege: opgaven H 9: 12, 13, (17).
Vrijdag 25 maart. Huiswerk hw5: opgave 9.18 op papier voor 15:00 uur.

Week 7(13). Bestudeer hoofdstuk 10 van het dictaat.
Dinsdag 29 maart. Hoorcollege. Teruggave huiswerk, en hoofdstuk 10.
Dinsdag/woensdag 29/30 maart. Werkcollege: H 10: 1, 3, (5).
Donderdag/vrijdag 31 maart/1 april. Werkcollege: H 10: 2, 8, (6).
Vrijdag 1 april. Huiswerk hw6: opgave 10.13 op papier voor 15:00 uur.

Week 8(14).
Dinsdag 5 april. Bespreking en teruggave huiswerk. Laatste gelegenheid plenair vragen te stellen. Bereid dus vragen voor.
Geen werkcollege in deze week.

Beoordeling

Het eindcijfer E wordt bepaald uit drie onderdelen: hw = het gemiddelde huiswerkcijfer, tt = het cijfer voor de tussentoets en T = het cijfer voor het afsluitende schriftelijke tentamen. Als T > 4 is, wordt E het gewogen gemiddelde E := (hw + tt + 2*T)/4, waarbij het tentamen dus even veel weegt als huiswerk en toets bij elkaar. Als T <= 4 is, geldt het tentamencijfer, dus E := T. Bij een eventueel hertentamen telt alleen het tentamencijfer.

Tussentijdse toets: vrijdag 11 maart 14-16 uur, tentamenhal.
Tentamen: donderdag 14 april, 9-12 uur, examenhal.

Link naar mijn start pagina.

Ik hoor het graag, als er hier of (bv) in het dictaat fouten of onduidelijkheden staan.