Program Correctness
Faculteit  Science and Engineering 
Jaar  2019/20 
Vakcode  INBPC08 
Vaknaam  Program Correctness 
Niveau(s)  propedeuse 
Voertaal  Engels 
Periode  semester II a 
ECTS  5 
Rooster  rooster.rug.nl 
Uitgebreide vaknaam  Program Correctness  
Leerdoelen  At the end of the course, the student is able to: 1) derive (small) correct program fragments for problems that are given by a formal specification 2) formally prove the correctness of given program fragments 

Omschrijving  An errorfree program is hardly ever obtained by simply trying to code it directly. Although it is possible to extensively test a program, it is not the case that a program that passes all tests is correct. A failed test can only show that a program is incorrect, but a passed test does not prove the correctness of a program. To show that a program is correct, we need a much more rigorous tool. In this course we will use (Floyd)Hoare logic to formally demonstrate the correctness of (small) imperative program fragments. The necessary proofrules for assignments, conditional statements (ifthenelse statement) and (while)loops will be introduced. Those rules are used to prove that a program fragment that satisfies a given specification. The first half of the course introduces FloayHoare logic, and applies it to small problems. The first half of the course is assessed with a written midterm exam. Special attention is paid to the derivation of efficient search algorithms (like saddleback search) in the second half of the course. In the final written exam, the focus is on the second half of the course. 

Uren per week  
Onderwijsvorm  Hoorcollege (LC), Werkcollege (T)  
Toetsvorm 
Opdracht (AST), Schriftelijk tentamen (WE), Tussentoets (IT)
(Let H = Homework, M = Midexam and E = Exam. The final grade F is obtained according to the following rule: F=If E < 5 then E else (H + M + 2*E)/4. In case of a reexamination the final grade is the grade obtained during the reexamination.) 

Vaksoort  propedeuse  
Coördinator  dr. A. Meijster  
Docent(en)  dr. A. Meijster  
Verplichte literatuur 


Entreevoorwaarden  Advisable: Logic  
Opmerkingen  
Opgenomen in 
