Semantics and Correctness
Course infoSchedule
Course moduleNWI-IBC026
Credits (ECTS)3
CategoryBA (Bachelor)
Language of instructionEnglish
Offered byRadboud University; Faculty of Science; Informatica en Informatiekunde;
dr. E.G.M. Hubbers
Other course modules lecturer
dr. E.G.M. Hubbers
Other course modules lecturer
Contactperson for the course
dr. E.G.M. Hubbers
Other course modules lecturer
dr. E.G.M. Hubbers
Other course modules lecturer
N.M. van der Weide
Other course modules lecturer
Academic year2020
KW3  (25/01/2021 to 04/04/2021)
Starting block
Course mode
RemarksThis course has been moved to Q3. Students for whom the course is compulsory in their programme have first access.
Registration using OSIRISYes
Course open to students from other facultiesYes
Waiting listNo
Placement procedureIn order of Study programme
ExplanationIn order of Study programme
After this course participants are able to:
  • Define the semantics of imperative language constructs using inductive methods.
  • Explain the consequences of design choices.
  • Analyze computations in imperative languages like termination behavior and semantic equivalence.
  • Prove properties of programs using inference systems for correctness.
  • Determine whether inference systems are sound and/or complete.
In this course, you will learn formalisms to define the operational semantics of imperative programming languages. These methods are important for designing new languages and extending existing languages. In addition, these formalisms are used for analyzing the behavior of programs. In the field of computing science, you will not only have to apply these formalisms, but you will also have to evaluate, expand or design these formalisms as well.

Instructional Modes
This course will flip the class room a bit: for each plenary lecture, the relatively simple concepts are already published before the lecture and you will have to study these topics.  Typically the first 20-25 minutes are spent on your questions about these topics, and the rest of the plenary lecture will be used for introducing the more complex topics. In addition, there will be parallel tutorial sessions where you can work on and ask questions about the weekly learning task. The weekly learning cycle ends with discussing some of the solutions that were handed in at the plenary response lectures.

Presumed foreknowledge
You have programming experience with imperative programming languages. In addition, you are able to:
  • use the language of predicate logic to formulate statements;
  • distinguish the elementary steps within argumentation and present proofs in a suitable inference system;
  • specify (programming) languages and extensions using regular expressions and context-free grammars;
  • formulate clearly, both in motivating solutions as well as in proofs in natural language.
You can obtain these prerequisites by doing the courses in the programming line, and by doing one of the courses Languages and Automata or Introduction to Formal Reasoning,  and by doing the course Logic and Applications. In addition, it helps if you have done the course Computability, but that is not a formal requirement.
Test information
The course is finalized with a written exam.

Required materials
Hanne Riis Nielson and Flemming Nielson: Semantics with applications, 1999. The book is available for free as PDF via Brightspace.
Title:Semantics with applications
Author:Hanne Riis Nielson and Flemming Nielson
Engelbert Hubbers: Annotated Programs, an alternative notation for correctness proofs. These notes are available as PDF via Brightspace.
Title:Annotated Programs
Author:Engelbert Hubbers

Instructional modes
Attendance MandatoryYes

84 hours.

Digital Exam
Test weight1
Test typeDigital exam with CIRRUS
OpportunitiesBlock KW3, Block KW4