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.