Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/VDM/VDMPP/KLVPP/   (Wiener Entwicklungsmethode ©)  Datei vom 13.4.2020 mit Größe 1 kB image not shown  

Quelle  Test.vdmpp   Sprache: VDM

 
\section{The Test Class}

The Test class defines an environment for executing test cases. The
class maintains a reference to a KLV instanceand it provides two
operations, runOneTest for execution of one test event, and runTests
for execution of a sequence of test events. Different kinds of test
events can be executed. These are defined by the Event class hierarchy
defined below.

The data types represent different kinds of categories of results.

\begin{vdm_al}
class Test

types

  public
  TestResult = KLVstate | BeaconsMet | MaxSpeed;

  public
  KLVstate :: cd : CabDisp
              eb : EmerBreak;

  public
  CabDisp :: alarm   : bool
             emerbr  : bool
             grfault : bool;

  public
  EmerBreak :: break : bool;

  public
  BeaconsMet :: ann : seq of TIVD
                res : seq of TIVE;

  public
  TIVD :: ts : real;

  public
  TIVE :: sp : real;

  public
  MaxSpeed :: ms: real;

instance variables

  klv : KLV := new KLV();

operations

  public
  runTests : seq of Event ==> seq of TestResult
  runTests (events) ==
    return [e.execute(klv) | e in seq events ];

  public
  runOneTest : Event ==> TestResult
  runOneTest (event) ==
    return event.execute(klv)
pre ((isofclass(HeadMeetBeaconEvent,event) => 
      let e1: HeadMeetBeaconEvent = event
      in isofclass(TIV_E, e1.getBeacon())) => klv.getAnnouncements() <> []) and
    ((isofclass(TailMeetBeaconEvent,event) =>
      let e2: TailMeetBeaconEvent = event
      in isofclass(TIV_E,e2.getBeacon())) => (klv.getFirstSpeedRestriction() or
                                             klv.getSpeedRestrictions() <> []));

end Test
\end{vdm_al}

98%


¤ Dauer der Verarbeitung: 0.14 Sekunden  (vorverarbeitet)  ¤

*© Formatika GbR, Deutschland






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.