|Module label||Correctness of Graph Programs|
|Credit points||6.0 KP|
|Faculty/Institute||Department of Computing Science|
|Used in course of study||
|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.
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.
|Language of instruction||German|
|Duration (semesters)||1 Semester|
|Module frequency||im 2-Jahres-Zyklus|
|Modullevel||AC (Aufbaucurriculum / Composition)|
|Modulart||je nach Studiengang Pflicht oder Wahlpflicht|
|Lern-/Lehrform / Type of program|
|Vorkenntnisse / Previous knowledge||- inf400 Theoretische Informatik I
- inf401 Theoretische Informatik II
|Course type||Comment||SWS||Frequency||Workload attendance|
|Total time of attendance for the module||56 h|
|Examination||Time of examination||Type of examination|
|Final exam of module||
Will be announced during the course
presentation or oral exam