inf450 - Correctness of Graph Programs (Complete module description)
Module label | Correctness of Graph Programs |
Modulkürzel | inf450 |
Credit points | 6.0 KP |
Workload | 180 h |
Institute directory | Department of Computing Science |
Verwendbarkeit des Moduls |
|
Zuständige Personen |
|
Prerequisites | - inf400 Theoretical Computer Science I - inf401 Theoretical Computer Science II |
Skills to be acquired in this module | The objectives of this module are modelling of systems, system changes and system properties. Introduction to graph programs. Introduction into system correctness. Methods for proving system correctness. Professional competence The students:
The students:
The students:
The students:
|
Module contents | The module is an introduction to the modelling of systems, system changes and system properties by means of graphs, graph programs and graph conditions and presents a method for proving correctness of systems with respect to a pre- and a postcondition. The basic structures used in this lecture are graphs; they are used in practically all domains of computing science for the representation of complex structures. Graph programs are constructed from the core constructs of nondeterministic rule application, sequential composition and iteration and they can effect programmatic changes of a graph structure. One well-known method for determining the correctness of programs with respect to a pre- and a postcondition is based on the construction of a weakest precondition of the postcondition with respect to the program and the attempt to decide whether the given precondition implies the computed weakest precondition. |
Literaturempfehlungen |
|
Links | |
Language of instruction | German |
Duration (semesters) | 1 Semester |
Module frequency | in 2-year cycle |
Module capacity | unlimited |
Reference text | Often offered as a block course |
Teaching/Learning method | 1VL + 1Ü |
Previous knowledge | - inf400 Theoretical Computer Science I - inf401 Theoretical Computer Science II |
Lehrveranstaltungsform | Comment | SWS | Frequency | Workload of compulsory attendance |
---|---|---|---|---|
Lecture | 3 | WiSe | 42 | |
Exercises | 1 | WiSe | 14 | |
Präsenzzeit Modul insgesamt | 56 h |
Examination | Prüfungszeiten | Type of examination |
---|---|---|
Final exam of module | Will be announced during the course |
presentation or oral exam |