Download Skript - Fachgebiet Echtzeitsysteme
Transcript
SE II - Dynamische Programmanalysen und Testen
Fachgebiet
Echtzeitsysteme
Überprüfung von Invarianten, ... in C++:
class TrafficLight {
public:
// Konstruktoren und Destruktoren
TrafficLight() {
... ; INVARIANT;
};
~TrafficLight() {
INVARIANT; ...
};
// öffentliche verändernde Operationen (Modifier)
void lightOn() {
PRE(isOff());
... ;
POST(isRed());
};
...
protected:
inline bool invariant() const { return ( ... ); };
// Übersetzer ruft inline-Methode nicht auf, sondern kopiert Rumpf an Aufrufstelle ein
};
© Prof. Dr. Andy Schürr (TU Darmstadt, FB 18, Institut für Datentechnik)
Seite 337