NWI-IBC026
Semantics and Correctness
Course infoSchedule
Course moduleNWI-IBC026
Credits (ECTS)3
CategoryBA (Bachelor)
Language of instructionDutch, English
Offered byRadboud University; Faculty of Science; Informatica en Informatiekunde;
Lecturer(s)
Lecturer
J.J.J. Doesburg
Other course modules lecturer
Examiner
dr. E.G.M. Hubbers
Other course modules lecturer
Lecturer
dr. E.G.M. Hubbers
Other course modules lecturer
Coordinator
dr. E.G.M. Hubbers
Other course modules lecturer
Contactperson for the course
dr. E.G.M. Hubbers
Other course modules lecturer
Academic year2018
Period
KW2  (05/11/2018 to 27/01/2019)
Starting block
KW2
Course mode
full-time
RemarksStudents for whom the course is compulsory in their programme have first access.
Registration using OSIRISYes
Course open to students from other facultiesYes
Pre-registrationNo
Waiting listNo
Placement procedureIn order of Study programme
ExplanationIn order of Study programme
Aims
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.
Content
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.
Additional comments
Because students who do not put effort into the weekly assignments, typically fail the exam, there will be some kind of obligation to work on the assignments. At the time of writing the information for the study guide, it is not clear yet how this will be implemented.

Topics
Topics that will be addressed:
- Expression evaluation
- Natural semantics
- Structural operational semantics
- Semantical equivalence
- Semantics for blocks and procedures
- Axiomatic semantics
- Soundness
- Completeness

Test information
The course is finalized with a written exam.

Prerequisites
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, Languages and Automata, Computability and Logics and Applications.

Contact information
http://www.cs.ru.nl/~hubbers/courses/sc

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

Instructional modes
Course
Attendance MandatoryYes

Remark
84 hours.

Lecture

Remark
14 hours.

Response lecture

Preparation of meetings
The corresponding task must have been studied seriously.

Remark
14 hours.

Self study

Remark
49 hours.

Tutorial

Remark
7 hours

Tests
Exam
Test weight1
Test typeExam
OpportunitiesBlock KW2, Block KW3