|
\section{The CheckSpeedEvent Test Class}
The CheckSpeedEvent class implements a test event that checks the
speed of a train (i.e.\ of a KLV instance). It provides a setSpeed and
an execute operation. The execute operation returns the status of the
Cab Display and of the Emergency Break.
\begin{vdm_al}
class CheckSpeedEvent is subclass of Event
instance variables
speed : real;
operations
public
CheckSpeedEvent: real ==> CheckSpeedEvent
CheckSpeedEvent (s) ==
speed := s;
public
execute : KLV ==> Test`TestResult
execute (klv) ==
( klv.checkSpeed(speed);
let mk_(a,e,g) = klv.getCabDisplay().getDisplay(),
e' = klv.getEmergencyBreak().getEmergencyBreak() in
return mk_Test`KLVstate(mk_Test`CabDisp(a,e,g),
mk_Test`EmerBreak(e')) );
end CheckSpeedEvent
\end{vdm_al}
¤ Dauer der Verarbeitung: 0.2 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
