Program Correctness
Faculteit  Science and Engineering 
Jaar  2020/21 
Vakcode  WBCS02405 
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)
(Homework 40% and Exam 60%  The final grade must be equal or above 5.75 for students to pass the course.  If the exam is digital, it will be a pass/fail instead of a numerical grade  In case of a reexamination the final grade is the grade obtained during the reexamination. That is, the homework grade does not count at the reexamination.) 

Vaksoort  propedeuse  
Coördinator  prof. dr. J.A. Perez Parra  
Docent(en)  prof. dr. J.A. Perez Parra  
Verplichte literatuur 


Entreevoorwaarden  Advisable: Logic  
Opmerkingen  In the academic year 20202021, all CS bachelor courses have limited enrollment:  CS students can always enter each course, regardless of whether the course is mandatory for them or not.  A maximum of only 20 places per course is available for nonCS students. These places are filled on a firstcomefirstserved basis, with priority given to students with a strong CSrelated background (e.g., CS exchange students, AI students, etc.). These students need to meet the course prerequisite requirements as mentioned on Ocasys. For more info about the enrollment procedure, see https://student.portal.rug.nl/infonet/studenten/fse/programmes/bsccs/general/vakintekeningprocedure#cap This course was registered last year with course code INBPC08 

Opgenomen in 
