|
\section{The HeadMeetBeaconEvent Test Class}
The HeadMeetBeaconEvent class implements a test event where the head
of a train meets a beacon. It provides a setBeacon and an execute
operation. The execute operation returns the current announcements and
speed restrictions.
\begin{vdm_al}
class HeadMeetBeaconEvent is subclass of Event
instance variables
beacon : Beacon;
operations
public
HeadMeetBeaconEvent: Beacon ==> HeadMeetBeaconEvent
HeadMeetBeaconEvent(b) ==
beacon := b;
public
execute : KLV ==> Test`TestResult
execute (klv) ==
( klv.headMeetsBeacon(beacon);
let anns = klv.getAnnouncements(),
restr = klv.getSpeedRestrictions() in
return mk_Test`BeaconsMet(
[ mk_Test`TIVD(a.getTargetSpeed()) | a in seq anns ],
[ mk_Test`TIVE(r.getSpeedRestriction()) | r in seq restr ]) );
pure public getBeacon: () ==> Beacon
getBeacon() ==
return beacon;
end HeadMeetBeaconEvent
\end{vdm_al}
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.20Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
|
Lebenszyklus
Die hierunter aufgelisteten Ziele sind für diese Firma wichtig
Ziele
Entwicklung einer Software für die statische Quellcodeanalyse
|
