Introduction to Informatics 2
Module IN0003
This module handbook serves to describe contents, learning outcome, methods and examination type as well as linking to current dates for courses and module examination in the respective sections.
Module version of SS 2012
There are historic module descriptions of this module. A module description is valid until replaced by a newer one.
| available module versions | |
|---|---|
| WS 2012/3 | SS 2012 |
Basic Information
IN0003 is a semester module in German language at Bachelor’s level which is offered in winter semester.
This Module is included in the following catalogues within the study programs in physics.
- Further Modules from Other Disciplines
| Total workload | Contact hours | Credits (ECTS) |
|---|---|---|
| 150 h | 60 h | 5 CP |
Content, Learning Outcome and Preconditions
Content
Among others, the module IN0003 is concerned with the following topics:
- Correctness of imperative programs
++ Verification according to Floyd or Hoare
++ Termination
++ Procedures
- Basic concepts of functional programming
++ Values, variables, functions
++ Data++structures, pattern matching
++ Higher order functions
++ Polymorphic types
++ Programming in the large: Structures and Functors
++ Correctness of functional programs
+++ Semantics of functional programs
+++ Verification of functional programs
- Correctness of imperative programs
++ Verification according to Floyd or Hoare
++ Termination
++ Procedures
- Basic concepts of functional programming
++ Values, variables, functions
++ Data++structures, pattern matching
++ Higher order functions
++ Polymorphic types
++ Programming in the large: Structures and Functors
++ Correctness of functional programs
+++ Semantics of functional programs
+++ Verification of functional programs
Learning Outcome
After successful completion of the module, participants understand the key concepts of functional programming languages. They are able to solve well presented tasks in a functional programming language. Therefore, they are able to acquire programming skills on their own also in further functional programming languages. They also are familiar with the most important techniques for the verification of imperative and functional programming language and can apply them to simple programs.
Preconditions
IN0001 Introduction to Informatics 1
Courses, Learning and Teaching Methods and Literature
Courses and Schedule
| Type | SWS | Title | Lecturer(s) | Dates |
|---|---|---|---|---|
| VO | 2 | Functional Programming and Verification (IN0003) | Nipkow, T. Rädle, J. |
Fri, 08:15–09:45, MW 2001 |
Learning and Teaching Methods
By means of a presentation, either by slides or whiteboard, the lecture transports the concepts of verification and the programming language and illustrates them by examples.
Accompanying assignments for individual study deepen the understanding of the concepts explained in the lecture, and train students to apply these to the verification of small programs and to master programming in the given programming language.
Accompanying assignments for individual study deepen the understanding of the concepts explained in the lecture, and train students to apply these to the verification of small programs and to master programming in the given programming language.
Media
Slide show, blackboard, possibly online programming and/or animations
Literature
Guy Cousineau und Michel Mauny, The Functional Approach to Programming, Cambridge University Press, Cambridge, 1998
Apt, Olderog: Programm-Verifikation. Springer 1991
Gerd Smolka: Programmierung - eine Einführung in die Informatik mit Standard ML. Oldenburg, 2007
Simon Tompson: Haskell: the Craft of Functional Programming. Addison-Wesley, 2011
Apt, Olderog: Programm-Verifikation. Springer 1991
Gerd Smolka: Programmierung - eine Einführung in die Informatik mit Standard ML. Oldenburg, 2007
Simon Tompson: Haskell: the Craft of Functional Programming. Addison-Wesley, 2011
Module Exam
Description of exams and course work
The exam takes the form of a 120 minutes written test. Small programming tasks allow to assess whether the students master a functional programming language and are able to realize small implementation problems. By inferring simple invariants they demonstrate that they have understood the principles of program verification and are able to apply these.
The successful completion of homework asignments may contribute to the grade as a bonus. The exact details for this are announced timely at the begin of the lecture.
The successful completion of homework asignments may contribute to the grade as a bonus. The exact details for this are announced timely at the begin of the lecture.
Exam Repetition
The exam may be repeated at the end of the semester.