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 als 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 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 Fundamentele Informatica, Logica, en Programmeermethoden.
Leerdoelen
Kennis en toepassing van de semantiek en bewijstheorie van basis imperatieve programmeerconcepten.
Rooster
De meest recente roosters zijn te vinden op de Studenten-website:
Onderwijsvorm
hoor- en werkcollege
Toetsing
De behandelde stof wordt schriftelijk geexamineerd .
Daarnaast worden er twee tot maximaal drie nog aan te kondigen deeltentamens gegeven.
Voor het eindcijfer telt het schriftelijk tentamen voor 75%. Het gemiddelde van de deeltentamens telt voor 25%.
Literatuur
Verification of Sequential and Concurrent Programs, Apt, Krzysztof R., de Boer, Frank S., Olderog, Ernst-Rüdiger, Series: Texts in Computer Science. Springer, 3rd ed. 2nd Printing., ISBN: 978-1-84882-744-8. Lecture slides
Aanmelden
Aanmelding voor vakken verloopt via uSis. Hiervoor is de uSis-code van het vak nodig, die te vinden zijn in de Studiegids. Meer info over het inschrijven voor vakken of tentamens is hier te vinden.
MyTimetable
In MyTimetable kun je alle vak- en opleidingsroosters vinden, waarmee jij je persoonlijke rooster kunt samenstellen. Onderwijsactiviteiten waarvoor je in uSis staat 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.
Vragen? Bekijk de video-instructie, lees de instructie of neem contact op met de ISSC helpdesk.
Brightspace
Inschrijving voor vakken verloopt via uSis. Wanneer je je hier inschrijft voor een bepaald vak krijg je automatisch ook toegang tot de omgeving van dit vak via Brightspace.
Voor meer informatie over Brightspace kun je op deze link klikken om de handleidingen van de universiteit te bekijken. Bij overige vragen of problemen kan contact opgenomen worden met de helpdesk van de universiteit Leiden.
Contact
Onderwijscoördinator Informatica, Riet Derogee
Website
Programmeren & Correctheid, agenda Programmeren & Correctheid, slides