Beschrijving
Hoe beschrijven 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 Java programma’s.
Methode
hoorcollege en werkgroep
Examinering
schriftelijk
Voorkennis
eerstejaarscolleges informatica
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.