Objektorientierte Programmierung und Modellierung (Fach) / Vor- und Nachbedingungen (Lektion)
In dieser Lektion befinden sich 4 Karteikarten
WS 15/16
Diese Lektion wurde von RouHim erstellt.
- Worum geht es bei dem Thema "Vor- und Nachbedingungen"? Es geht darum das die Korrektheit eines Programms mithilfe von Vor- und Nachbedingungen sichergestellt wird. Das tut man indem man eine Formel als Vorbedingung und eine als Nachbedingung aufstellt.
- Was ist das Hoare-Kalkül? Beim Hoare-Kalkül geht es darum, dass die Korrektheit nicht nur vor und nach dem Programm gegeben ist, sondern auch nach jeder Anweisung. Somit hat man für jede Anweisung eine Vor- und Nachbedinung:{P} S {Q}P = VorbedingungS = AnweisungQ = Nachbedingung
- Wie funktioniert das Hoare-Kalkül in der Praxis? Es wird zunächst eine allgemeine Bedingung festgelegt die immer gilt.Diese Bedingung heißt Invariante {I}. Anschließend wird eine Nachbedingung / Vorbedingung erfasst, diese Bedingungen halten den Zustand vor und nach dem Programm fest.(Diese Bedingungen sind meistens vorgegeben) Jetzt wird jede Anweisung zwischen Anfang und Ende von hinten nach vorne einzeln Bewiesen. Bsp.:I = {i >= 1}VB = {n >= 0} {n + 5 >= 0} {1 + n + 5 >= 1}i = 1; {i + n + 5 >= 1}n += 5; {i + n >= 1}i += n;{i >= 1}NB = {i > n && i >= 5}
- Besonderheit Hoare-Kalkül für Schleifen, wie funktioniert es? Der Aufbau ist folgendermaßen:{B} = Schleifenbedingung{I} = Schleifeninvariante {I}while(x > y){ {I && B} ...Schleifen Körper {I}}{I && !B}Vorgehensweise:- Schleifeninvariante und Schleifenbedingung finden- Schleifenkörper von hinten nach vorne beweisen