The MaxSpeedEvent class implements a test event that does not perform
any action, but returns the status of the maximal allowed speed of the
train.
\begin{vdm_al} class MaxSpeedEvent issubclassof Event
operations
public
execute : KLV ==> Test`TestResult
execute (klv) ==
( let ms = klv.getMaxSpeed() in return mk_Test`MaxSpeed(ms) );
end MaxSpeedEvent
\end{vdm_al}
¤ 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.0.22Bemerkung:
(vorverarbeitet)
¤
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.
