Download Skript - Fachgebiet Echtzeitsysteme

SE II - Dynamische Programmanalysen und Testen
Fachgebiet
Echtzeitsysteme
Implementierung der Spezialisierung in C++:
class FlashingTrafficLight : public TrafficLight {
// bietet neue Operation „blinkendes gelbes Licht“ an
// verbietet direkten Übergang von rotem Licht zu grünem Licht
// bei der Gelbphase nach der Rotphase ist auch das rote Licht an
public:
// erlaubte Verschärfung der geerbten Invarianten:
// invariant: (! ( (isOff() || isFlashing()) && (isGreen() || isYellow() || isRed()) ) );
// invariant: (! isGreen() && (isRed() || isYellow()) );
// invariant: (! (isOff() && isFlashing());
// verbotene Lockerung der geerbten Invarianten:
// invariant: (isOff() || isFlashing() || isGreen() || isYellow() || isRed())
// neue Observer-Operation
bool isFlashing();
// neue Modifier-Operation
virtual void flashingOn();
// precondition: (isRed() || isYellow() || isGreen());
// postcondition: isFlashing();
© Prof. Dr. Andy Schürr (TU Darmstadt, FB 18, Institut für Datentechnik)
Seite 331