Studiegids

nl en

Program Correctness

Vak
2024-2025

Toegangseisen

Niet van toepassing.

Beschrijving

In dit college behandelen we een van de fundementele vragen van de informatica: Hoe specificeren we wat een programma geschreven in een imperatieve programmeertaal (zoals Java) eigenlijk doet en hoe kunnen we met behulp van een logica bewijzen dat ons programma correct is, d.w.z. inderdaad doet wat het geacht wordt te doen. In dit college zullen we leren hoe we de predikaatlogica, zoals geintroduceerd in het college Logica, kunnen gebruiken voor de specifiatie en verificatie van de correctheid van imperatieve programma's.

Aanbevolen voorkennis: de vakken Foundations of Computer Science (4031FDCS6), Introduction to Logic (4031ILOGI), en Concepts of Programming Languages (4032CNPRE).

Leerdoelen

Het hoofddoel van dit vak is het opdoen van kennis en het leren toepassen van de semantiek en bewijstheorie van basis imperatieve programmeerconcepten.

Aan het einde van dit vak heeft de student:

  • leren toepassen van de predikaatlogica in het formuleren van rekenkundige relaties tussen (programma)variabelen

  • basiskennis over de bewijstheorie van correctheid van simpele imperative programma's

  • basiskennis over de bewijstheorie van correctheid van recursieve imperative programma's

  • leren toepassen van bewijstheorie in de beschrijving van correcte formele bewijzen

  • leren geven van concrete tegenvoorbeelden in het geval van incorrecte programma's

  • basiskennis over meta-theoretische aspecten zoals correctheid, volledigheid en beslisbaarheid

  • ervaring met computer-ondersteund bewijzen

Rooster

In MyTimetable kun je alle vak- en opleidingsroosters vinden, waarmee jij je persoonlijke rooster kunt samenstellen. Onderwijsactiviteiten waarvoor je je via MyStudyMap hebt ingeschreven, worden automatisch in je rooster getoond.

Daarnaast kun je My Timetable gemakkelijk koppelen aan een agenda-app op je telefoon en worden roosterwijzigingen automatisch in je agenda doorgevoerd; bovendien ontvang je desgewenst per e-mail een notificatie van de wijziging. Je kunt notificaties aanzetten bij Instellingen, nadat je bent ingelogd.

Vragen? Bekijk de video, lees de instructie of neem contact op met de ISSC helpdesk.

Let op: Joint Degree studenten Leiden/Delft dienen de informatie uit de Leidse en Delftse MyTimetables samen te voegen om een volledig rooster te zien. Deze video legt uit hoe dat werkt.

Onderwijsvorm

Hoorcolleges zijn digitaal vooraf opgenomen, voor 2 uur per week. Werkcolleges en practica worden gehouden op locatie, voor 4 uur per week. Soms worden practica ingevuld met oefeningen zoals tijdens de werkcolleges. Als de groep studenten klein is, dan is tevens individuele begeleiding door de docent mogelijk.

Toetsing en weging

  • Er wordt tussentijds schriftelijk geexamineerd met twee deeltentamens

  • Voor het eindcijfer telt het eindtentamen voor 60% en de deeltentamen voor samen 40%.

Er is een mogelijkheid tot herkansing van het eindtentamen.

De docent maakt duidelijk hoe studenten hun nagekeken schriftelijke tentamens kunnen inzien.

Literatuurlijst

Verification of Sequential and Concurrent Programs, Apt, Krzysztof R., de Boer, Frank S., Olderog, Ernst-Rüdiger, Series: Texts in Computer Science. Springer, 3rd edition, ISBN: 978-1-84882-744-8

Het boek is noodzakelijk voor het volgen van het vak. Een selectie van (optionele) additionale literatuur wordt aangeboden.

Inschrijven

Als student ben je zelf verantwoordelijk voor het tijdig inschrijven via MyStudyMap.

In deze korte video zie je stap voor stap hoe je je kunt inschrijven voor cursussen in MyStudyMap.
Uitgebreide informatie over de werking van MyStudyMap vind je hier.

Er zijn twee inschrijfperiodes per jaar:

  • de inschrijving voor het najaar opent in juli

  • de inschrijving voor het voorjaar opent in december

Zie deze pagina voor meer informatie over deadlines en inschrijven voor vakken en tentamens.

Let op:

  • Het is verplicht om je in te schrijven voor alle activiteiten die je gaat volgen van een vak.

  • Je inschrijving is pas voltooid wanneer je je cursusplanning indient in het tabblad ‘Klaar voor inschrijving’ door op ‘indienen’ te klikken.

  • Niet ingeschreven zijn voor een (her)tentamen betekent dat je niet mag deelnemen aan het (her)tentamen.

Contact

Onderwijscoördinator Informatica, Onderwijscoördinator LIACS bachelors

Opmerkingen

Websites: Programmeren & Correctheid, agenda Programmeren & Correctheid, slides

Software
Vanaf collegejaar 2024/2025 werkt de faculteit Wiskunde en Natuurwetenschappen met het software distributieplatform Academic Software. Via het platform kun je toegang krijgen tot de software die je nodig hebt voor bepaalde vakken in je studie. Voor sommige software moet je laptop aan bepaalde systeemeisen voldoen. Dit staat aangegeven bij de software. Belangrijk is dat je de software installeert voor de start van het vak. Meer informatie over het laptopprofiel vind je op de studentenwebsite.