Quelle HeadMeetBeaconEvent.vdmpp Sprache: VDM

\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}

quality88%

¤ Dauer der Verarbeitung: 0.23 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.