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
De meest recente roosters zijn te vinden op de Studenten-website:
In MyTimetable (login) 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 MyTimetable 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, na login.
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: twee tot maximaal drie deeltentamens.
De behandelde stof wordt schriftelijk of mondeling geexamineerd tijdens het eindtentamen. Mondelinge examinering vindt alleen plaats bij een kleine groep studenten.
Voor het eindcijfer telt het eindtentamen voor 50% en het gemiddelde van de deeltentamens voor 50%.
Schriftelijke tentamens worden gemaakt met behulp van een eigen laptop. 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
Met ingang van het collegejaar 2022-2023 ben je als student zelf verantwoordelijk om je tijdig, dat wil zeggen 14 of 28 dagen voor aanvang van het vak, in te schrijven. Dat kan via MyStudymap. Dit doe je twee keer per jaar: één keer voor de vakken die je wilt volgen in semester 1 en één keer voor de vakken die je wilt volgen in semester 2.
Inschrijven voor vakken in het eerste semester is mogelijk vanaf juli; inschrijven voor vakken in het tweede semester is mogelijk vanaf december. Zie voor meer informatie deze pagina (tab Wiskunde en Natuurwetenschappen)
Daarnaast is het voor alle studenten, inclusief eerstejaars bachelorstudenten, verplicht om zich in te schrijven voor tentamens én de inschrijving voor elk tentamen in My Studymap te bevestigen. Dit kan tot en met uiterlijk 10 kalenderdagen voorafgaand aan het tentamen. Zonder geldige voorinschrijving én bevestiging in My Studymap kun je niet deelnemen aan het tentamen.
Uitgebreide informatie over de werking van MyStudymap vind je hier.
Contact
Onderwijscoördinator Informatica, Onderwijscoördinator LIACS bachelors
Opmerkingen
Websites: Programmeren & Correctheid, agenda Programmeren & Correctheid, slides